Thanks! Makes perfect sense. I will adapt the proof accordingly! -stan
On Sat, Mar 7, 2020 at 10:47 AM Mario Carneiro <[email protected]> wrote: > Yep, you correctly identified eliman0 as the bad lemma here. I hadn't > heard of it but it's using a trick to avoid having to prove that the input > is in the domain of the function. Using metamath.exe, I searched for this > pattern and got a few results: > > MM> sea * '( ? ` ? ) e. ( ? " ? )'/j > 19563 eliman0 $p |- ( ( A e. B /\ -. ( F ` A ) = (/) ) -> ( F ` A ) e. ( F > " B > ) ) > 20603 funfvima $p |- ( ( Fun F /\ B e. dom F ) -> ( B e. A -> ( F ` B ) e. > ( F > " A ) ) ) > 20604 funfvima2 $p |- ( ( Fun F /\ A C_ dom F ) -> ( B e. A -> ( F ` B ) > e. ( F > " A ) ) ) > 20611 fnfvima $p |- ( ( F Fn A /\ S C_ A /\ X e. S ) -> ( F ` X ) e. ( F " > S ) > ) > 20740 f1elima $p |- ( ( F : A -1-1-> B /\ X e. A /\ Y C_ A ) -> ( ( F ` X > ) e. > ( F " Y ) <-> X e. Y ) ) > 79323 kqfvima $e |- F = ( x e. X |-> { y e. J | x e. y } ) $p |- ( ( J e. ( > TopOn ` X ) /\ U e. J /\ A e. X ) -> ( A e. U <-> ( F ` A ) e. ( F " U > ) ) > ) > > and the actual theorems you want to reference are either funfvima, > funfvima2, or fnfvima depending on how the function is presented. (Arguably > eliman0 should be moved to after fnfvima and given a more similar name, > e.g. fviman0.) In this case, the function has known domain and range so I > would go for fnfvima, using fnco to prove that ( abs o. F ) Fn RR. > > > On Fri, Mar 6, 2020 at 11:59 PM 'Stanislas Polu' via Metamath < > [email protected]> wrote: > >> (fvco3d is a natural deduction form of fvco3 proved here: >> https://github.com/metamath/set.mm/commit/454132a35254c17c4e54353b5c2c772eeb2ebb65#diff-12dc1484b058d1ee6cb68a74194d66c7R641421-R641429 >> ) >> >> -stan >> >> On Sat, Mar 7, 2020 at 8:54 AM Stanislas Polu <[email protected]> wrote: >> >>> Interesting! >>> >>> It basically comes from an attempt at satisfying the conditions >>> for eliman0. Here's the full proof draft: >>> >>> ``` >>> $( <MM> <PROOF_ASST> THEOREM=imo72b2lem1 LOC_AFTER=? >>> >>> h1::imo72b2lem1.1 |- ( ph -> F : RR --> RR ) >>> h2::imo72b2lem1.7 |- ( ph -> E. x e. RR ( F ` x ) =/= 0 ) >>> h3::imo72b2lem0.6 |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 ) >>> >>> !d84:: |- ( ( ph /\ x e. RR ) -> ( ( abs o. F ) ` x ) =/= (/) ) >>> d83:d84:adantrr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>> ( ( abs o. F ) ` x ) =/= (/) ) >>> d81:d83:neneqd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> -. >>> ( ( abs o. F ) ` x ) = (/) ) >>> >>> d95:1:ffvelrnda |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR ) >>> d94:d95:adantrr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( >>> F ` x ) e. RR ) >>> d92:d94:recnd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>> ( F ` x ) e. CC ) >>> d93::simprr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( >>> F ` x ) =/= 0 ) >>> d91:d92,d93:absrpcld |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>> ( abs ` ( F ` x ) ) e. RR+ ) >>> d9:d91:rpgt0d |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> 0 >>> < ( abs ` ( F ` x ) ) ) >>> >>> d80::simprl |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> x >>> e. RR ) >>> d82::eliman0 |- ( ( x e. RR /\ -. ( ( abs o. F ) ` x ) = (/) ) >>> -> ( ( abs o. F ) ` x ) e. ( ( abs o. F ) " RR ) ) >>> d75:d80,d81,d82:syl2anc |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>> -> ( ( abs o. F ) ` x ) e. ( ( abs o. F ) " RR ) ) >>> oeqaa::imaco |- ( ( abs o. F ) " RR ) = ( abs " ( F " RR ) ) >>> d71:d75,oeqaa:syl6eleq |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>> -> ( ( abs o. F ) ` x ) e. ( abs " ( F " RR ) ) ) >>> d73:1:adantr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> F >>> : RR --> RR ) >>> d74::simprl |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> x >>> e. RR ) >>> d72:d73,d74:fvco3d |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( >>> ( abs o. F ) ` x ) = ( abs ` ( F ` x ) ) ) >>> d7:d72,d71:eqeltrrd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( >>> abs ` ( F ` x ) ) e. ( abs " ( F " RR ) ) ) >>> >>> d10::simpr |- ( ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>> /\ z = ( abs ` ( F ` x ) ) ) -> z = ( abs ` ( F ` x ) ) ) >>> d8:d10:breq2d |- ( ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) /\ >>> z = ( abs ` ( F ` x ) ) ) -> ( 0 < z <-> 0 < ( abs ` ( F ` x ) ) ) ) >>> >>> d6:d7,d8,d9:rspcedvd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>> E. z e. ( abs " ( F " RR ) ) 0 < z ) >>> qed:2,d6:rexlimddv |- ( ph -> E. z e. ( abs " ( F " RR ) ) 0 < z ) >>> >>> $) >>> >>> -stan >>> >>> On Fri, Mar 6, 2020 at 11:58 PM Mario Carneiro <[email protected]> >>> wrote: >>> >>>> The composition function value combination is easy enough to eliminate >>>> using fvco, but the equality to the empty set is a type error, because the >>>> lhs is a real number and the question of whether the empty set is a real >>>> number is deliberately left ambiguous by the real number axioms. So I would >>>> like to know what steps got you to this point. There are some function >>>> value theorems that assume this as a "convenience" but there should be >>>> analogues of them that don't (probably with some other assumption like the >>>> function is a set). >>>> >>>> On Fri, Mar 6, 2020 at 8:02 AM 'Stanislas Polu' via Metamath < >>>> [email protected]> wrote: >>>> >>>>> Thanks again Mario! >>>>> >>>>> I made more progress towards the final demonstration of the full IMO >>>>> problem. Working on the following lemma: >>>>> >>>>> ``` >>>>> h1::imo72b2lem1.1 |- ( ph -> F : RR --> RR ) >>>>> >>>>> h2::imo72b2lem1.7 |- ( ph -> E. x e. RR ( F ` x ) =/= 0 ) >>>>> >>>>> h3::imo72b2lem0.6 |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 >>>>> ) >>>>> ``` >>>>> >>>>> I need to prove the following goal which seems pretty obvious but I'm >>>>> struggling to find a way to discharge it: >>>>> >>>>> ``` >>>>> d84:: |- ( ( ph /\ x e. RR ) -> ( ( abs o. F ) ` x ) =/= (/) ) >>>>> ``` >>>>> >>>>> Any idea on how to proceed with this? >>>>> >>>>> Thanks thanks! >>>>> >>>>> -stan >>>>> >>>>> On Thu, Mar 5, 2020 at 6:27 PM Mario Carneiro <[email protected]> >>>>> wrote: >>>>> >>>>>> 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 >>>>>> <https://groups.google.com/d/msgid/metamath/CAFXXJSs4iVxdk7Uz1_bW-heUVCJy-CMGENLNtzWd8%2B12rFEVBQ%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_0x2N3k16mC%2Byc_%3D6HvNQ3OWpAXtQ3fHkMv%3DPqERwFR60Q%40mail.gmail.com >>>>> <https://groups.google.com/d/msgid/metamath/CACZd_0x2N3k16mC%2Byc_%3D6HvNQ3OWpAXtQ3fHkMv%3DPqERwFR60Q%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/CAFXXJSv0pGnDb%2Bfae5_ZS_mAK_R6MeMQPAL4gsHD-9S5g2XSVQ%40mail.gmail.com >>>> <https://groups.google.com/d/msgid/metamath/CAFXXJSv0pGnDb%2Bfae5_ZS_mAK_R6MeMQPAL4gsHD-9S5g2XSVQ%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_0yzRWT%3DZn6qPpgXPbzSabuOqHVSLW6uG9aF6S6yYht5mA%40mail.gmail.com >> <https://groups.google.com/d/msgid/metamath/CACZd_0yzRWT%3DZn6qPpgXPbzSabuOqHVSLW6uG9aF6S6yYht5mA%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/CAFXXJSutmF6LrPLUHM%3DoBbd5d_4kE8jeM9j-gFsc9tnYVU4Mcg%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAFXXJSutmF6LrPLUHM%3DoBbd5d_4kE8jeM9j-gFsc9tnYVU4Mcg%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_0zvmvxLGSCC4QA2vDLK3HR7qoXZuZsmXR_cyEwKQJaQsQ%40mail.gmail.com.
