Tenth theorem proved:
${
$d x y z a b c u v B $. $d x y z a b c u v .o. $. $d a u v ph $.
mendpadm.a $e |- B = ( Base ` M ) $.
mendpadm.b $e |- .o. = ( +g ` M ) $.
mendpadm.d $e |- ( ph -> M e. Mgm ) $.
mendpadm.e $e |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o.
( x .o. ( z .o. y ) ) ) = z ) $.
$( Lemma for mendpadm. Squares of all elements are equal to each other. $)
mendpadmlem6 $p |- ( ph -> A. x e. B A. y e. B ( x .o. x ) = ( y .o. y )
) $=
( vu vv va vb co wceq wral weq oveq2d vc cv wi wal wa mendpadmlem4 id
oveq2
wcel oveq12d eqeq1d oveq1 eqeq12d cbvral2vw sylib ad2antrr simpr eqidd
cmgm
simplr syl3anc rspc2vd mpd cbvral3vw rspc3v eqtr3d ex alrimiv df-ral
imbi2i
mgmcl albii sylbbr syl eqeq2d )
ALUBZVPGPZMUBZVRGPZQZMERZLERZBUBZWCGPZCUBZW
EGPZQZCERBERAVPEUIZVREUIZVTUCZMUDZUCZLUDZWBAWLLAWHWKAWHUEZWJMWNWIVTWNWIUEZV
RVQVRGPZGPZVQVSWONUBZOUBZWRGPZGPZWSQZOERNERZWQVQQZAXCWHWIAWCWEWCGPZGPZWEQZC
ERBERXCABCDEFGHIJKUFXGXBWRWEWRGPZGPZWEQBCNOEEBNSZXFXIWEXJWCWRXEXHGXJUGWCWRW
EGUHUJUKCOSZXIXAWEWSXKXHWTWRGWEWSWRGULTXKUGUMUNUOUPZWOXDVRWSVRGPZGPZWSQXBNO
VRVQEEENMSZXAXNWSXOWRVRWTXMGXOUGWRVRWSGUHUJUKWSVQQZXNWQWSVQXPXMWPVRGWSVQVRG
ULTXPUGUMWNWIUQZWOXOUEEURWOFUSUIZWHWHVQEUIAXRWHWIJUPAWHWIUTZXSEFVPVPGHIVKVA
VBVCWOWPVRVRGWOVQVPVRVPGPZGPZGPZWPVRWOYAVRVQGWOXCYAVRQZXLWOYCVPWSVPGPZGPZWS
QXBNOVPVREEENLSZXAYEWSYFWRVPWTYDGYFUGWRVPWSGUHUJUKOMSZYEYAWSVRYGYDXTVPGWSVR
VPGULTYGUGUMXSWOYFUEEURXQVBVCTWOWRWSGPZWRUAUBZWSGPZGPZGPZYIQZUAEROERNERZYBV
RQZAYNWHWIAWCWEGPZWCDUBZWEGPZGPZGPZYQQZDERCERBERYNKUUAYMWRWEGPZWRYRGPZGPZYQ
QYHWRYQWSGPZGPZGPZYQQBCDNOUAEEEXJYTUUDYQXJYPUUBYSUUCGWCWRWEGULWCWRYRGULUJUK
XKUUDUUGYQXKUUBYHUUCUUFGWEWSWRGUHXKYRUUEWRGWEWSYQGUHTUJUKDUASZUUGYLYQYIUUHU
UFYKYHGUUHUUEYJWRGYQYIWSGULTTUUHUGUMVDUOUPWOWHWHWIYNYOUCXSXSXQYMYOVPWSGPZVP
YJGPZGPZYIQVQVPYIVPGPZGPZGPZYIQNOUAVPVPVREEEYFYLUUKYIYFYHUUIYKUUJGWRVPWSGUL
WRVPYJGULUJUKOLSZUUKUUNYIUUOUUIVQUUJUUMGWSVPVPGUHUUOYJUULVPGWSVPYIGUHTUJUKU
AMSZUUNYBYIVRUUPUUMYAVQGUUPUULXTVPGYIVRVPGULTTUUPUGUMVEVAVCVFTVFVGVHVGVHWBW
HWAUCZLUDWMWALEVIUUQWLLWAWKWHVTMEVIVJVLVMVNVTWGWDVSQLMBCEELBSZVQWDVSUURVPWC
VPWCGUURUGZUUSUJUKMCSZVSWFWDUUTVRWEVRWEGUUTUGZUVAUJVOUNUO $.
$}
> Yes, I'm surprised that this is the case, probably shows the lack of
intuition on my side. When I showed the problem set to Mario, he suggested
rewriting some statements with class variables, i.e. instead of* "A. a e. B
A. b e. B ( a .o. b ) = ( b .o. a)" *one can introduce *"X e. B"* and *"Y
e. B"* as hypotheses and write *"( X .o. Y ) = ( Y .o. X )"*. In the end I
did that only for a couple of first problems, since I wasn't sure how these
additional hypotheses work with scoping etc. Thierry is using that
technique in his repository, yet it seems the overall proof length is also
large.
I wonder how it looks on the other proof assistants. It seems an
interesting example related to the topic of de Bruijn factors and the
difficulty of proving theorems formally vs. informally.
Il giorno domenica 8 dicembre 2024 alle 22:10:02 UTC+1 Gino Giotto ha
scritto:
> Ninth theorem proved:
>
> ${
> $d x y z a b v B $. $d x y z a b v .o. $. $d v ph $.
> mendpadm.a $e |- B = ( Base ` M ) $.
> mendpadm.b $e |- .o. = ( +g ` M ) $.
> mendpadm.d $e |- ( ph -> M e. Mgm ) $.
> mendpadm.e $e |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o.
> ( x .o. ( z .o. y ) ) ) = z ) $.
> $( First part of ~ mendpadmlem5 $)
> mendpadmlem5a $p |- ( ph -> A. x e. B ( x .o. ( x .o. x ) ) = x ) $=
> ( vv va vb cv co wceq wral weq id wcel wa impac mendpadmlem4 adantr
> oveq12d
> idd oveq2 eqeq1d oveq1 oveq2d eqeq12d cbvral2vw sylib rspc2v sylc
> ralrimiva
> cbvralvw )
> ALOZUSUSGPZGPZUSQZLERBOZVCVCGPZGPZVCQZBERAVBLEAUSEUAZUBZVGVGUBMO
>
> ZNOZVIGPZGPZVJQZNERMERZVBAVGVGAVGUGUCVHVCCOZVCGPZGPZVOQZCERBERZVNAVSVGABCDE
>
> FGHIJKUDUEVRVMVIVOVIGPZGPZVOQBCMNEEBMSZVQWAVOWBVCVIVPVTGWBTVCVIVOGUHUFUICNS
>
> ZWAVLVOVJWCVTVKVIGVOVJVIGUJUKWCTULUMUNVMVBUSVJUSGPZGPZVJQMNUSUSEEMLSZVLWEVJ
>
> WFVIUSVKWDGWFTVIUSVJGUHUFUINLSZWEVAVJUSWGWDUTUSGVJUSUSGUJUKWGTULUOUPUQVBVFL
> BELBSZVAVEUSVCWHUSVCUTVDGWHTZWHUSVCUSVCGWIWIUFUFWIULURUN $.
>
> $d a b ph $.
> $( Second part of ~ mendpadmlem5 $)
> mendpadmlem5b $p |- ( ph -> A. x e. B ( ( x .o. x ) .o. x ) = x ) $=
> ( vv va vb cv co wceq wral weq oveq12d wcel wa mendpadmlem4 adantr id
> oveq2
> eqeq1d oveq1 oveq2d eqeq12d cbvral2vw sylib cmgm w3a 3anim1i 3anidm23
> mgmcl
> simplr simpr eqcomd mendpadmlem5a cbvralvw rspcdva ad2antrr eqtr3d
> rspcimdv
> syl rspcdv mpd ralrimiva sylibr )
> ALOZVLGPZVLGPZVLQZLERBOZVPGPZVPGPZVPQZBER
>
> AVOLEAVLEUAZUBZMOZNOZWBGPZGPZWCQZNERZMERZVOWAVPCOZVPGPZGPZWIQZCERBERZWHAWMV
>
> TABCDEFGHIJKUCUDWLWFWBWIWBGPZGPZWIQBCMNEEBMSZWKWOWIWPVPWBWJWNGWPUEZVPWBWIGU
>
> FTUGCNSZWOWEWIWCWRWNWDWBGWIWCWBGUHUIWRUEUJUKULWAWGVOMVMEWAFUMUAZVTVTUNZVMEU
>
> AAVTWTAWSVTVTJUOUPEFVLVLGHIUQVGWAWBVMQZUBZWFVONVLEAVTXAURXBNLSZUBZWEVNWCVLX
>
> DWBVMWDVLGWAXAXCURZXDVLVMGPZWDVLXDVLWCVMWBGXDWCVLXBXCUSZUTXDWBVMXEUTTWAXFVL
>
> QZXAXCWAWBWBWBGPZGPZWBQZXHMEVLMLSZXJXFWBVLXLWBVLXIVMGXLUEZXLWBVLWBVLGXMXMTT
>
> XMUJWAVPVQGPZVPQZBERZXKMERAXPVTABCDEFGHIJKVAUDXOXKBMEWPXNXJVPWBWPVPWBVQXIGW
>
> QWPVPWBVPWBGWQWQTTWQUJVBULAVTUSVCVDVETXGUJVHVFVIVJVSVOBLEBLSZVRVNVPVLXQVQVM
> VPVLGXQVPVLVPVLGXQUEZXRTXRTXRUJVBVK $.
>
> $( Lemma for mendpadm. Multiplication of ` x ` by ` x .o. x ` gives ` x
> ` . $)
> mendpadmlem5 $p |- ( ph -> A. x e. B ( ( x .o. ( x .o. x ) ) = x /\ ( (
> x .o. x ) .o. x ) = x ) ) $=
> ( cv co wceq wral wa mendpadmlem5a mendpadmlem5b r19.26 sylanbrc )
> ABLZUAUA
> GMZGMUANZBEOUBUAGMUANZBEOUCUDPBEOABCDEFGHIJKQABCDEFGHIJKRUCUDBEST $.
> $}
>
> Il giorno domenica 8 dicembre 2024 alle 13:54:02 UTC+1 savask ha scritto:
>
>> > As a side note, Tirix is now close to completing the proof of the
>> Eckmann-Hilton argument, and although his version is better organized than
>> mine, it still looks pretty long. I guess now we can say that the short
>> proof on Wikipedia doesn't convey a good idea about the amount of work
>> needed to accomplish that task.
>>
>> Yes, I'm surprised that this is the case, probably shows the lack of
>> intuition on my side. When I showed the problem set to Mario, he suggested
>> rewriting some statements with class variables, i.e. instead of* "A. a
>> e. B A. b e. B ( a .o. b ) = ( b .o. a)" *one can introduce *"X e. B"*
>> and *"Y e. B"* as hypotheses and write *"( X .o. Y ) = ( Y .o. X )"*. In
>> the end I did that only for a couple of first problems, since I wasn't sure
>> how these additional hypotheses work with scoping etc. Thierry is using
>> that technique in his repository, yet it seems the overall proof length is
>> also large.
>>
>> I plan to add another 3 "bonus" tasks near the end of next week, asking
>> to prove the Mendelsohn-Padmanabhan identity in a boolean group (so we get
>> a full characterization). Again, this is trivial mathematically but I'm not
>> quite sure it will be trivial in metamath, although we have all the
>> required definitions like group exponent (gEx) ready.
>>
>
--
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 visit
https://groups.google.com/d/msgid/metamath/41cbff26-2400-46e4-862f-88bcb35fa0d8n%40googlegroups.com.
