Hi Mario, I'm sure you're right, and in fact I would use a class A and something like ph -> A e. V as an additional hyp.
But I cannot reproduce the contradiction off the top of my head; it would be interesting to see it, to gain a deeper understanding. Can you please show a short proof? (do you proof something like +oo e. RR ? ) Thank you Glauco Il giorno lunedì 14 ottobre 2024 alle 14:28:43 UTC+2 [email protected] ha scritto: > It's not safe to make an assumption of the form |- { x e. RR | ( F ` x ) = > 4 } = { a , b } because the variables a,b are implicitly universally > quantified in the hypothesis, which means you can prove a contradiction > from it. (Consider what happens if you use vtocl on the hypothesis to > replace a by +oo.) You should either use class variables A,B as I > indicated, or add a context ph -> before every assumption (which is *not* > assumed to be disjoint from a,b). > > On Mon, Oct 14, 2024 at 2:12 PM Glauco <[email protected]> wrote: > >> I take it back, you can get away with { x | ( F ` x ) = 4 } , here's >> the proof (but for your larger goal, I doubt it's enough) >> >> h1::temp3.1 |- F = ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) ) - ( ( >> 2 x. k ) x. x ) ) + l ) ) >> h2::temp3.2 |- { x | ( F ` x ) = 4 } = { a , b } >> 3::fveq2 |- ( x = a -> ( F ` x ) = ( F ` a ) ) >> 4:3:eqeq1d |- ( x = a -> ( ( F ` x ) = 4 <-> ( F ` a ) = 4 ) ) >> 5::vex |- a e. _V >> 6::nfmpt1 |- F/_ x ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) ) - ( >> ( 2 x. k ) x. x ) ) + l ) ) >> 7:1,6:nfcxfr |- F/_ x F >> 8::nfcv |- F/_ x a >> 9:7,8:nffv |- F/_ x ( F ` a ) >> 10:9:nfeq1 |- F/ x ( F ` a ) = 4 >> 11:10,5,4:elabf |- ( a e. { x | ( F ` x ) = 4 } <-> ( F ` a ) = 4 ) >> 12::vex |- a e. _V >> 13:12:prid1 |- a e. { a , b } >> 14:13,2:eleqtrri |- a e. { x | ( F ` x ) = 4 } >> qed:14,11:mpbi |- ( F ` a ) = 4 >> >> $= ( cv cfv c4 wceq cab wcel cpr vex cr c2 co cmul prid1 cexp cmin caddc >> nfmpt1 >> eleqtrri cmpt nfcxfr nfcv nffv nfeq1 fveq2 eqeq1d elabf mpbi ) >> DIZAIZCJZKLZA >> >> MZNUPCJZKLZUPUPEIZOUTUPVCDPZUAHUFUSVBAUPAVAKAUPCACAQBIZUQRUBSTSRVETSUQTSUCSF >> IUDSZUGGAQVFUEUHAUPUIUJUKVDUQUPLURVAKUQUPCULUMUNUO $. >> >> $d a x >> >> Il giorno lunedì 14 ottobre 2024 alle 13:53:35 UTC+2 Glauco ha scritto: >> >>> Since the >>> >>> $d F x >>> >>> constraint would conflict with your F definition, here is an alternative >>> version >>> >>> >>> h1::temp3.1 |- F = ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) ) - ( >>> ( 2 x. k ) x. x ) ) + l ) ) >>> h2::temp3.2 |- { x e. RR | ( F ` x ) = 4 } = { a , b } >>> 3::fveq2 |- ( x = a -> ( F ` x ) = ( F ` a ) ) >>> 4:3:eqeq1d |- ( x = a -> ( ( F ` x ) = 4 <-> ( F ` a ) = 4 ) ) >>> 5::nfcv |- F/_ x a >>> 6::nfcv |- F/_ x RR >>> 7::nfmpt1 |- F/_ x ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) ) - >>> ( ( 2 x. k ) x. x ) ) + l ) ) >>> 8:1,7:nfcxfr |- F/_ x F >>> 9:8,5:nffv |- F/_ x ( F ` a ) >>> 10:9:nfeq1 |- F/ x ( F ` a ) = 4 >>> 11:5,6,10,4:elrabf |- ( a e. { x e. RR | ( F ` x ) = 4 } <-> ( a e. RR >>> /\ ( F ` a ) = 4 ) ) >>> 12::vex |- a e. _V >>> 13:12:prid1 |- a e. { a , b } >>> 14:13,2:eleqtrri |- a e. { x e. RR | ( F ` x ) = 4 } >>> 15:14,11:mpbi |- ( a e. RR /\ ( F ` a ) = 4 ) >>> qed:15:simpri |- ( F ` a ) = 4 >>> >>> $= ( cv cr wcel cfv c4 wceq crab wa nfcv c2 co cmul cpr vex prid1 >>> eleqtrri cexp >>> cmin caddc cmpt nfmpt1 nfcxfr nffv nfeq1 fveq2 eqeq1d elrabf mpbi >>> simpri ) D >>> >>> >>> IZJKZURCLZMNZURAIZCLZMNZAJOZKUSVAPURUREIZUAVEURVFDUBUCHUDVDVAAURJAURQZAJQAUT >>> >>> >>> MAURCACAJBIZVBRUESTSRVHTSVBTSUFSFIUGSZUHGAJVIUIUJVGUKULVBURNVCUTMVBURCUMUNUO >>> UPUQ $. >>> >>> $d a x >>> >>> Il giorno lunedì 14 ottobre 2024 alle 13:42:45 UTC+2 Glauco ha scritto: >>> >>>> Hi Jorge, >>>> >>>> with Yamma you get something like this (I doubt you can get away with { >>>> x | ( F ` x ) = 4 }, for instance ( F ` +oo ) is not "well-defined" ) >>>> >>>> ``` >>>> $theorem temp3 >>>> >>>> * comments >>>> >>>> h1::temp3.1 |- { x e. RR | ( F ` x ) = 4 } = { a , b } >>>> 2::fveq2 |- ( x = a -> ( F ` x ) = ( F ` a ) ) >>>> 3:2:eqeq1d |- ( x = a -> ( ( F ` x ) = 4 <-> ( F ` a ) = 4 ) >>>> ) >>>> 4:3:elrab |- ( a e. { x e. RR | ( F ` x ) = 4 } <-> ( a e. >>>> RR /\ ( F ` a ) = 4 ) ) >>>> 5::vex |- a e. _V >>>> 6:5:prid1 |- a e. { a , b } >>>> 7:6,1:eleqtrri |- a e. { x e. RR | ( F ` x ) = 4 } >>>> 8:7,4:mpbi |- ( a e. RR /\ ( F ` a ) = 4 ) >>>> qed:8:simpri |- ( F ` a ) = 4 >>>> >>>> $= ( cv cr wcel cfv c4 wceq crab wa cpr vex prid1 eleqtrri fveq2 eqeq1d >>>> elrab >>>> mpbi simpri ) >>>> CFZGHZUCBIZJKZUCAFZBIZJKZAGLZHUDUFMUCUCDFZNUJUCUKCOPEQUIUFAUCG >>>> UGUCKUHUEJUGUCBRSTUAUB $. >>>> >>>> $d F x >>>> $d a x >>>> ``` >>>> >>>> >>>> >>>> >>>> Il giorno lunedì 14 ottobre 2024 alle 12:40:47 UTC+2 [email protected] >>>> ha scritto: >>>> >>>>> I wanted to check how far I can get in formalizing this problem and >>>>> its solution. But I stuck in the very beginning. >>>>> >>>>> >>>>> Firstly, I formalized the initial conditions as Mario suggested: >>>>> >>>>> >>>>> hyp1: |- 0 < k >>>>> >>>>> hyp2: |- 0 < l >>>>> >>>>> hyp3: |- F = ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) ) - ( ( 2 x. k ) x. x >>>>> ) ) + l ) ) >>>>> >>>>> hyp4: |- { x | ( F ` x ) = 4 } = { a , b } >>>>> >>>>> hyp5: |- ( ( ( a - b ) ^ 2 ) + ( ( ( F ` a ) - ( F ` b ) ) ^ 2 ) ) = ( >>>>> 6 ^ 2 ) >>>>> >>>>> hyp6: |- ( ( ( a ^ 2 ) + ( ( F ` a ) ^ 2 ) ) + ( ( b ^ 2 ) + ( ( F ` b >>>>> ) ^ 2 ) ) ) = c >>>>> >>>>> >>>>> I used { a , b } instead of { A , B } because then I can easily prove |- >>>>> a e. _V, which is used in the proof below. Also, as I understand, a >>>>> and b represent x-coordinates of the corresponding points. >>>>> >>>>> >>>>> Next, I wanted to simplify hyp5, by proving that F(a) = F(b) = 4, so >>>>> the hyp5 would be |- ( ( a - b ) ^ 2 ) = ( 6 ^ 2 ). But that’s where >>>>> I am stuck. I can prove |- [ a / x ] ( F ` x ) = 4 which looks a >>>>> right direction to move in: >>>>> >>>>> >>>>> 1| | vex | |- a e. _V >>>>> >>>>> 2| 1 | prid1 | |- a e. { a , b } >>>>> >>>>> 3| | hyp4 | |- { x | ( F ` x ) = 4 } = { a , b } >>>>> >>>>> 4| 3 | eleq2i | |- ( a e. { x | ( F ` x ) = 4 } <-> a e. { a , b } ) >>>>> >>>>> 5| 2,4 | mpbir | |- a e. { x | ( F ` x ) = 4 } >>>>> >>>>> 6| | df-clab | |- ( a e. { x | ( F ` x ) = 4 } <-> [ a / x ] ( F ` >>>>> x ) = 4 ) >>>>> >>>>> 7| 5,6 | mpbi | |- [ a / x ] ( F ` x ) = 4 >>>>> >>>>> >>>>> But I still cannot prove |- ( F ` a ) = 4. Any suggestions what >>>>> approaches I can try to prove this? >>>>> >>>>> On Sunday, July 28, 2024 at 11:54:47 PM UTC+2 [email protected] wrote: >>>>> >>>>>> On Sun, Jul 28, 2024 at 11:43 PM Glauco <[email protected]> wrote: >>>>>> >>>>>>> I maybe wrong, but my feeling is that what Jagra calls A , in >>>>>>> Mario's translation is actually < A , 4 > (or < A, F(A) > , if you >>>>>>> prefer). >>>>>> >>>>>> >>>>>> I meant it to be interpreted as <A, F(A)>, and part of the proof >>>>>> would be showing that F(A) = 4 so that the rest of the statement >>>>>> simplifies. (But that would seem to be part of the proof, not the >>>>>> formalization of the statement, if we want to read it literally.) >>>>>> >>>>>> -- >> 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/161f583c-22bf-4699-b663-92652793f9c3n%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/161f583c-22bf-4699-b663-92652793f9c3n%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/69ebb4e9-fb35-4f43-a1d9-ac3ff8fe917bn%40googlegroups.com.
