Last theorem of the original challenge proved:
${
$d x y z a b B $. $d x y z a b .o. $. $d a b ph $. $d M a b x $.
mendpadm.a $e |- B = ( Base ` M ) $.
mendpadm.b $e |- .o. = ( +g ` M ) $.
mendpadm.c $e |- ( ph -> B =/= (/) ) $.
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 ) $.
$( Boolean groups (i.e. abelian groups of exponent 2), can be defined by
one identity.
Here we use a short identity from a 1972 paper of N.S. Mendelsohn and
R. Padmanabhan. $)
mendpadm $p |- ( ph -> ( M e. Abel /\ A. x e. B ( x .o. x ) = ( 0g ` M )
) ) $=
( vb va wcel co wceq wral weq oveq12d cabl cv c0g cfv cbs a1i
mendpadmlem11
cplusg wa wi wal mendpadmlem9 oveq1 oveq2 eqeq12d cbvral2vw r19.21bi
df-ral
sylib 19.21bi 3impia isabld eqid adantr simpr mgmcl syl3anc
mendpadmlem6 id
eqeq1d eqcom bitrdi rspc2v adantll oveq1d mendpadmlem5b rspcv mpan9
adantlr
cmgm mpd eqtr3d oveq2d mendpadmlem5a ismgmid2 ralrimiva cbvralvw jca )
AFUA
OBUBZWIGPZFUCUDZQZBERZAMNEGFEFUEUDQAHUFGFUHUDQAIUFABCDEFGHIKLJUGAMUBZEOZNUB
ZEOZWNWPGPZWPWNGPZQZAWOUIZWQWTUJZNXAWTNERZXBNUKAXCMEAWICUBZGPZXDWIGPZQZCERB
ERXCMERABCDEFGHIKLULXGWTWNXDGPZXDWNGPZQBCMNEEBMSZXEXHXFXIWIWNXDGUMWIWNXDGUN
UOCNSXHWRXIWSXDWPWNGUNXDWPWNGUMUOUPUSUQWTNEURUSUTVAVBAWPWPGPZWKQZNERWMAXLNE
AWQUIZMEGXKFWKHWKVCIXMFVTOZWQWQXKEOAXNWQKVDAWQVEZXOEFWPWPGHIVFVGXMWOUIZWNWN
GPZWNGPZXKWNGPWNXPXQXKWNGXPWJXDXDGPZQZCERBERZXQXKQZXMYAWOAYAWQABCDEFGHIKLVH
VDVDWQWOYAYBUJAXTYBXSXKQZBCWPWNEEBNSZXTXKXSQYCYDWJXKXSYDWIWPWIWPGYDVIZYETVJ
XKXSVKVLCMSZXSXQXKYFXDWNXDWNGYFVIZYGTVJVMVNWAZVOAWOXRWNQZWQAWJWIGPZWIQZBERW
OYIABCDEFGHIKLVPYKYIBWNEXJYJXRWIWNXJWJXQWIWNGXJWIWNWIWNGXJVIZYLTZYLTYLUOVQV
RVSWBXPWNXQGPZWNXKGPWNXPXQXKWNGYHWCAWOYNWNQZWQAWIWJGPZWIQZBERWOYOABCDEFGHIK
LWDYQYOBWNEXJYPYNWIWNXJWIWNWJXQGYLYMTYLUOVQVRVSWBWEWFXLWLNBENBSZXKWJWKYRWPW
IWPWIGYRVIZYSTVJWGUSWH $.
$}
Every theorem of the original challenge now has a proof (either by me or
Thierry).
--
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/da0c754b-a3f2-465e-b4bc-0edad930642cn%40googlegroups.com.
