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.
