I proved the eleventh theorem. As anticipated by Savask, this is the first
one using nonemptyness.
${
$d x y z a b u v B $. $d x y z a b u v .o. $. $d M u v $. $d u v a b
ph $.
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 ) $.
$( Lemma for mendpadm. ` M ` has an identity element. $)
mendpadmlem7 $p |- ( ph -> ( 0g ` M ) e. B ) $=
( vv vu vb co wceq wa wral oveq12d va c0g cfv eqid wrex wne wcel weq
eleq1a
cv c0 simpr anim1ci mendpadmlem6 id eqeq1d eqeq2d cbvral2vw ad2antrr
rspc2v
sylib sylc syl9r imp31 eqeq12d anbi12d mendpadmlem5 cbvralvw ralbii
rspcdv2
ex ancom ralrimiva wi r19.2zb biimpi cmgm w3a 3anim1i 3anidm23 mgmcl
syl wb
simpl eqcomd ad4ant24 rspcdv ralrimdva rspcimedv rexlimdva mpd mgmidcl
) AM
EGNFFUBUCZHWMUDIAUAUJZWNGPZOUJZGPZWPQZWPWOGPZWPQZRZOESZUAEUEZNUJZMUJZGPZXEQ
ZXEXDGPZXEQZRZMESZNEUEZAEUKUFZXBUAESZXCJAXBUAEAWNEUGZRZXAOEXPWPEUGZRZXEXEGP
ZXEGPZXEQZXEXSGPZXEQZRZXAMWPEXRMOUHZRZYAWRYCWTYFXTWQXEWPYFXSWOXEWPGXPXQYEXS
WOQZXQYEXEEUGZXPYGWPEXEUIXPYHYGXPYHRYHXORXDXDGPZWPWPGPZQZOESNESZYGXPXOYHAXO
ULUMAYLXOYHABUJZYMGPZCUJZYOGPZQZCESBESYLABCDEFGHIKLUNYQYKYIYPQBCNOEEBNUHZYN
YIYPYRYMXDYMXDGYRUOZYSTUPCOUHZYPYJYIYTYOWPYOWPGYTUOZUUATUQURVAUSYKYGXSYJQNO
XEWNEENMUHZYIXSYJUUBXDXEXDXEGUUBUOZUUCTUPOUAUHZYJWOXSUUDWPWNWPWNGUUDUOZUUET
UQUTVBVKVCVDZXRYEULZTUUGVEYFYBWSXEWPYFXEWPXSWOGUUGUUFTUUGVEVFXPXQULAYDMESZX
OXQAYCYARZMESZUUHAYMYNGPZYMQZYNYMGPZYMQZRZBESUUJABCDEFGHIKLVGUUOUUIBMEBMUHZ
UULYCUUNYAUUPUUKYBYMXEUUPYMXEYNXSGUUPUOZUUPYMXEYMXEGUUQUUQTZTUUQVEUUPUUMXTY
MXEUUPYNXSYMXEGUURUUQTUUQVEVFVHVAUUIYDMEYCYAVLVIVAUSVJVMVMXMXNXCVNXBUAEVOVP
VBAXBXLUAEXPXKXBNWOEXPFVQUGZXOXOVRZWOEUGAXOUUTAUUSXOXOKVSVTEFWNWNGHIWAWBXPX
DWOQZRZXBXJMEUVBYHRXAXJOXEEUVBYHULUVAOMUHZXAXJWCXPYHUVAUVCRZWRXGWTXIUVDWQXF
WPXEUVDWOXDWPXEGUVDXDWOUVAUVCWDWEZUVAUVCULZTUVFVEUVDWSXHWPXEUVDWPXEWOXDGUVF
UVETUVFVEVFWFWGWHWIWJWKWL $.
$}
I found this one to be more challenging than the previous ones, not because
of its length, but rather because there were a few steps that, when taken
in the wrong direction, lead me to dead ends. Finding a strategy that
worked all the way from the beginning to the end required some nontrivial
consideration (it might very well be that you won't feel the same, this is
my experience).
--
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/46145ae9-27ee-4aca-a0c8-47323e87dcbcn%40googlegroups.com.
