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/8fb3b928-75b7-4ff7-bebc-d05336ce8d6cn%40googlegroups.com.
