There is a theorem specifically for that translation, something like A. x e. ( F " A ) P[x] <-> A. y e. A P[( F ` y )]. It's probably called ralima but you've caught me on the bus again.
Mario On Thu, Mar 5, 2020, 8:07 AM 'Stanislas Polu' via Metamath < [email protected]> wrote: > Thanks Mario! > > I just finished formalizing the following lemma (which is a good chunk of > the proof \o/): > > ``` > $d F c x $. $d c ph x $. > imo72b2lem.1 $e |- ( ph -> F : RR --> RR ) $. > imo72b2lem.2 $e |- ( ph -> G : RR --> RR ) $. > imo72b2lem.3 $e |- ( ph -> A e. RR ) $. > imo72b2lem.4 $e |- ( ph -> B e. RR ) $. > imo72b2lem.5 $e |- ( ph -> ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) = > ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) $. > imo72b2lem.6 $e |- ( ph -> A. x e. ( abs " ( F " RR ) ) x <_ 1 ) $. > imo72b2lem.7 $e |- ( ph -> E. x e. RR ( F ` x ) =/= 0 ) $. > > imo72b2lem $p |- ( ph -> ( ( abs ` ( F ` A ) ) x. ( abs ` ( G ` B ) ) > ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) ) $= > ``` > > Proof here: > https://github.com/spolu/set.mm/commit/454132a35254c17c4e54353b5c2c772eeb2ebb65 > > One thing I'm quite dissatisfied with is the shape of `imo72b2lem.6`. I'd > much rather have the more natural/intuitive expression `|- ( ph -> A. x e. > RR ( abs ` ( F `x ) ) <_ 1 )` but I completely failed to prove imo72b2lem.6 > from it. Any help on this would be greatly appreciated! > > -stan > > On Wed, Mar 4, 2020 at 8:45 PM Mario Carneiro <[email protected]> wrote: > >> Can't look right now, but you should search for a theorem of the form A = >> (/) <-> ( F " A ) = (/) . >> >> On Wed, Mar 4, 2020, 11:30 AM 'Stanislas Polu' via Metamath < >> [email protected]> wrote: >> >>> I'm now looking to prove that `( abs " ( F " RR ) ) =/= (/)` given `F : >>> RR --> RR`. From my exploration of the definition of --> I believe this >>> should be enough but I don't see an easy path towards that? Would anybody >>> have an example in mind that could give me a little bit of inspiration? >>> >>> Thanks for the continued support! >>> >>> -stan >>> >>> On Wed, Mar 4, 2020 at 6:29 PM Benoit <[email protected]> wrote: >>> >>>> Stan: you're right about the need to prove this (if using explicit >>>> substitution): look for the utility theorems exchanging [. / ]. with other >>>> symbols (quantifiers, operations). As said by Jim and Thierry, who are >>>> more experienced in proof building, implicit substitution might be easier >>>> to use. I think it is instructive to compare the details of both proving >>>> styles on a specific example (e.g. ralbidv, suggested by Thierry, would be >>>> analogous to exchanging [. / ]. with A.). >>>> >>>> Still, I think adding what I called rspesbcd could prove useful (if it >>>> is not already in set.mm under another label; I cannot search now, but >>>> it probably is already somewhere). >>>> >>>> Benoît >>>> >>>> -- >>>> You received this message because you are subscribed to the Google >>>> Groups "Metamath" group. >>>> To unsubscribe from this group and stop receiving emails from it, send >>>> an email to [email protected]. >>>> To view this discussion on the web visit >>>> https://groups.google.com/d/msgid/metamath/ebdd296f-6bcd-49e0-88c8-c7fef3628cdd%40googlegroups.com >>>> <https://groups.google.com/d/msgid/metamath/ebdd296f-6bcd-49e0-88c8-c7fef3628cdd%40googlegroups.com?utm_medium=email&utm_source=footer> >>>> . >>>> >>> -- >>> You received this message because you are subscribed to the Google >>> Groups "Metamath" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to [email protected]. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/metamath/CACZd_0zFiVT5n-7%2BYh-YL2mDCLMom6R66gq7gbMT7tgJzTzadQ%40mail.gmail.com >>> <https://groups.google.com/d/msgid/metamath/CACZd_0zFiVT5n-7%2BYh-YL2mDCLMom6R66gq7gbMT7tgJzTzadQ%40mail.gmail.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/CAFXXJStosWZ0BEO7zjpeW90VMNT3pf-Kr6nUaqLefJyA%3Dgwa2Q%40mail.gmail.com >> <https://groups.google.com/d/msgid/metamath/CAFXXJStosWZ0BEO7zjpeW90VMNT3pf-Kr6nUaqLefJyA%3Dgwa2Q%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CACZd_0zgFkBD0kOaAXNGyB3PL18Qt06uSHV%3DEmwOjh6Rk5j3OQ%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CACZd_0zgFkBD0kOaAXNGyB3PL18Qt06uSHV%3DEmwOjh6Rk5j3OQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSs4iVxdk7Uz1_bW-heUVCJy-CMGENLNtzWd8%2B12rFEVBQ%40mail.gmail.com.
