I removed some DV conditions from my previous proof of aabbaa to use it in
mendpadmlem9. Proofs for mendpadmlem10 and mendpadmlem11 are also
provided.
${
$( If multiplying two times from the left (and the right) is an identity
mapping, then the operation is commutative. $)
$d a b u B $. $d b u X $. $d b u Y $. $d a b u .o. $. $d u ph $.
aabbaa.a $e |- ( ph -> A. a e. B A. b e. B ( a .o. b ) e. B ) $.
aabbaa.b $e |- ( ph -> A. a e. B A. b e. B ( a .o. ( a .o. b ) ) = b ) $.
aabbaa.c $e |- ( ph -> A. a e. B A. b e. B ( ( b .o. a ) .o. a ) = b ) $.
aabbaa.d $e |- ( ph -> X e. B ) $.
aabbaa.e $e |- ( ph -> Y e. B ) $.
aabbaa $p |- ( ph -> ( X .o. Y ) = ( Y .o. X ) ) $=
( vu co wceq wral oveq2 id oveq12d eqeq1d weq ralbidv cbvralvw sylib
bitrdi
cv eqcom oveq1 oveq1d eqeq12d wa eqidd wcel eleq1d rspc2vd mpd oveq2d
eqtrd
)
ACDENZUSCENZCENZDCENAGUFZMUFZENZVCENZVBOZGBPZMBPZUSVAOZAVBFUFZENZVJENZVBO
ZGBPZFBPVHJVNVGFMBFMUAZVMVFGBVOVLVEVBVOVKVDVJVCEVJVCVBEQVORZSTUBUCUDZAVIVBV
BCENZCENZOZVFMGCUSBBBVCCOZVFVSVBOVTWAVEVSVBWAVDVRVCCEVCCVBEQWARSTVSVBUGUEVB
USOZVBUSVSVAWBRWBVRUTCEVBUSCEUHUIUJKAWAUKBULZAVCVBENZBUMZGBPZMBPZUSBUMZAVJV
BENZBUMZGBPZFBPWGHWKWFFMBVOWJWEGBVOWIWDBVJVCVBEUHZUNUBUCUDAWHCVBENZBUMWEMGC
DBBBWAWDWMBVCCVBEUHUNVBDOZWMUSBVBDCEQUNKWCLUOUPZUOUPAUTDCEAUTUSUSDENZENZDAC
WPUSEAVHCWPOZVQAWRVBVBDENZDENZOZVFMGDCBBBVCDOZVFWTVBOXAXBVEWTVBXBVDWSVCDEVC
DVBEQXBRSTWTVBUGUEVBCOZVBCWTWPXCRXCWSUSDEVBCDEUHUIUJLAXBUKBULKUOUPUQAVCWDEN
ZVBOZGBPZMBPZWQDOZAVJWIENZVBOZGBPZFBPXGIXKXFFMBVOXJXEGBVOXIXDVBVOVJVCWIWDEV
PWLSTUBUCUDAXHUSUSVBENZENZVBOXEMGUSDBBBVCUSOZXDXMVBXNVCUSWDXLEXNRVCUSVBEUHS
TWNXMWQVBDWNXLWPUSEVBDUSEQUQWNRUJWOAXNUKBULLUOUPURUIUR $.
$}
${
$d x y z a b c u v w B $. $d x y z a b c u v w .o. $. $d a b c u v w 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. Multiplication is commutative. $)
mendpadmlem9 $p |- ( ph -> A. x e. B A. y e. B ( x .o. y ) = ( y .o. x )
) $=
( vu vb va cv co wceq wral wcel weq vv wa cmgm ad2antrr simpr mgmcl
syl3anc
simplr ralrimiva oveq1 eleq1d oveq2 cbvral2vw sylib mendpadmlem8a id
eqeq1d
oveq12d oveq2d eqeq12d mendpadmlem8b ralcom aabbaa )
ALOZUAOZGPZVEVDGPZQZU
AERZLERBOZCOZGPZVKVJGPZQZCERBERAVILEAVDESZUBZVHUAEVPVEESZUBZEVDVEGCBAVMESZB
ERCERZVOVQAMOZNOZGPZESZNERZMERVTAWEMEAWAESZUBZWDNEWGWBESZUBFUCSZWFWHWDAWIWF
WHJUDAWFWHUHWGWHUEEFWAWBGHIUFUGUIUIWDVSVKWBGPZESMNCBEEMCTZWCWJEWAVKWBGUJZUK
NBTZWJVMEWBVJVKGULZUKUMUNUDAVKVMGPZVJQZBERCERZVOVQAWAWCGPZWBQZNERMERZWQAVJV
LGPZVKQZCERBERWTABCDEFGHIJKUOXBWSWAWAVKGPZGPZVKQBCMNEEBMTZXAXDVKXEVJWAVLXCG
XEUPVJWAVKGUJURUQCNTZXDWRVKWBXFXCWCWAGVKWBWAGULUSXFUPUTUMUNWSWPVKWJGPZWBQMN
CBEEWKWRXGWBWKWAVKWCWJGWKUPWLURUQWMXGWOWBVJWMWJVMVKGWNUSWMUPUTUMUNUDVRVLVKG
PVJQZCERBERZXHBERCERAXIVOVQABCDEFGHIJKVAUDXHBCEEVBUNAVOVQUHVPVQUEVCUIUIVHVN
VJVEGPZVEVJGPZQLUABCEELBTVFXJVGXKVDVJVEGUJVDVJVEGULUTUACTXJVLXKVMVEVKVJGULV
EVKVJGUJUTUMUN $.
$( Lemma for mendpadm. Multiplication is associative. $)
mendpadmlem10 $p |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .o. y )
.o. z ) = ( x .o. ( y .o. z ) ) ) $=
( va vb co wceq wral weq oveq2 oveq1 oveq2d vu vv wcel mendpadmlem4
oveq12d
vw vc cv wa eqeq1d eqeq12d cbvral2vw sylib ad3antrrr simpllr eqidd
ad2antrr
id cmgm simplr simpr syl3anc adantr rspc2vd mpd mendpadmlem8b oveq1d
rspc2v
mgmcl wi adantll cbvral3vw rspc3v 3eqtr3rd eqtr3d ralrimiva )
AUAUHZUBUHZGN
ZUFUHZGNZVQVRVTGNZGNZOZUFEPZUBEPZUAEPBUHZCUHZGNZDUHZGNZWGWHWJGNZGNZOZDEPCEP
BEPAWFUAEAVQEUCZUIZWEUBEWPVREUCZUIZWDUFEWRVTEUCZUIZVQWAVQGNZGNZWAWCWTLUHZMU
HZXCGNZGNZXDOZMEPLEPZXBWAOZAXHWOWQWSAWGWHWGGNZGNZWHOZCEPBEPXHABCDEFGHIJKUDX
LXGXCWHXCGNZGNZWHOBCLMEEBLQZXKXNWHXOWGXCXJXMGXOURZWGXCWHGRUEUJCMQZXNXFWHXDX
QXMXEXCGWHXDXCGSTXQURZUKULUMUNWTXIVQXDVQGNZGNZXDOXGLMVQWAEEELUAQZXFXTXDYAXC
VQXEXSGYAURZXCVQXDGRUEUJXDWAOZXTXBXDWAYCXSXAVQGXDWAVQGSTYCURUKAWOWQWSUOWTYA
UIEUPWTFUSUCZVSEUCZWSWAEUCAYDWOWQWSJUNZWRYEWSWRYDWOWQYEAYDWOWQJUQAWOWQUTWPW
QVAEFVQVRGHIVIVBVCZWRWSVAZEFVSVTGHIVIVBVDVEWTXAWBVQGWTWAVSWBVTGNZGNZGNZWAVS
VRGNZGNWBXAWTYJYLWAGWTYIVRVSGWTXCXDGNZXDGNZXCOZMEPLEPZYIVROZAYPWOWQWSAWIWHG
NZWGOZCEPBEPYPABCDEFGHIJKVFYSYOXCWHGNZWHGNZXCOBCLMEEXOYRUUAWGXCXOWIYTWHGWGX
CWHGSZVGXPUKXQUUAYNXCXQYTYMWHXDGWHXDXCGRZXRUEUJULUMUNZWQWSYPYQVJWPYOYQVRXDG
NZXDGNZVROLMVRVTEELUBQZYNUUFXCVRUUGYMUUEXDGXCVRXDGSVGUUGURUKMUFQZUUFYIVRUUH
UUEWBXDVTGXDVTVRGRUUHURUEUJVHVKVETTWTYMXCUGUHZXDGNZGNZGNZUUIOZUGEPMEPLEPZYK
WBOZAUUNWOWQWSAWIWGWJWHGNZGNZGNZWJOZDEPCEPBEPUUNKUUSUUMYTXCUUPGNZGNZWJOYMXC
WJXDGNZGNZGNZWJOBCDLMUGEEEXOUURUVAWJXOWIYTUUQUUTGUUBWGXCUUPGSUEUJXQUVAUVDWJ
XQYTYMUUTUVCGUUCXQUUPUVBXCGWHXDWJGRTUEUJDUGQZUVDUULWJUUIUVEUVCUUKYMGUVEUVBU
UJXCGWJUUIXDGSTTUVEURUKVLUMUNWTYEWSWBEUCZUUNUUOVJYGYHWTYDWQWSUVFYFWPWQWSUTY
HEFVRVTGHIVIVBUUMUUOVSXDGNZVSUUJGNZGNZUUIOWAVSUUIVTGNZGNZGNZUUIOLMUGVSVTWBE
EEXCVSOZUULUVIUUIUVMYMUVGUUKUVHGXCVSXDGSXCVSUUJGSUEUJUUHUVIUVLUUIUUHUVGWAUV
HUVKGXDVTVSGRUUHUUJUVJVSGXDVTUUIGRTUEUJUUIWBOZUVLYKUUIWBUVNUVKYJWAGUVNUVJYI
VSGUUIWBVTGSTTUVNURUKVMVBVEWTYLVQWAGWTYPYLVQOZUUDWRYPUVOVJZWSWOWQUVPAYOUVOV
QXDGNZXDGNZVQOLMVQVREEYAYNUVRXCVQYAYMUVQXDGXCVQXDGSVGYBUKMUBQZUVRYLVQUVSUVQ
VSXDVRGXDVRVQGRUVSURUEUJVHVKVCVETVNTVOVPVPVPWDWNWGVRGNZVTGNZWGWBGNZOWIVTGNZ
WGWHVTGNZGNZOUAUBUFBCDEEEUABQZWAUWAWCUWBUWFVSUVTVTGVQWGVRGSVGVQWGWBGSUKUBCQ
ZUWAUWCUWBUWEUWGUVTWIVTGVRWHWGGRVGUWGWBUWDWGGVRWHVTGSTUKUFDQZUWCWKUWEWMVTWJ
WIGRUWHUWDWLWGGVTWJWHGRTUKVLUM $.
$d a b c M $.
mendpadm.c $e |- ( ph -> B =/= (/) ) $.
$( Lemma for mendpadm. ` M ` is a group. $)
mendpadmlem11 $p |- ( ph -> M e. Grp ) $=
( vb vu wceq wcel co wral eqeq12d oveq12d va vc c0g cfv cbs a1i cplusg
cmgm
mgmcl syl3an1 w3a mendpadmlem10 weq oveq1 oveq1d oveq2d rspc3v
mendpadmlem7
cv oveq2 mpan9 mendpadmlem5b id cbvralvw sylib wi simpr ax-1 eleq1a
anabsi5
wa im2anan9 3anim1i 3anidm23 syl mendpadmlem6 ad2antrr eqeq1d eqeq2d
rspc2v
ancoms adantll mpd rspccv eqtr3d mendpadmlem5a adantr grpidd rspcdv ex
mpid
imp simplll simpllr adantl 3jca 3ad2ant1 3adant1 rspcdv2 pm3.22 sylc
isgrpd
)
AUAMUBEGFUAUSZFUCUDZEFUEUDOZAHUFGFUGUDOZAIUFAFUHPZXCEPZMUSZEPZXCXIGQZEPJE
FXCXIGHIUIUJABUSZCUSZGQZDUSZGQZXLXMXOGQZGQZOZDERCERBERXHXJUBUSZEPUKXKXTGQZX
CXIXTGQZGQZOZABCDEFGHIJKULXSYDXCXMGQZXOGQZXCXQGQZOXKXOGQZXCXIXOGQZGQZOBCDXC
XIXTEEEBUAUMZXPYFXRYGYKXNYEXOGXLXCXMGUNUOXLXCXQGUNSCMUMZYFYHYGYJYLYEXKXOGXM
XIXCGUTUOYLXQYIXCGXMXIXOGUNUPSDUBUMZYHYAYJYCXOXTXKGUTYMYIYBXCGXOXTXIGUTUPSU
QVAABCDEFGHILJKURAXHXDXCGQZXCOZAXHXIXIGQZXIGQZXIOZMERZYOAXLXLGQZXLGQZXLOZBE
RZYSABCDEFGHIJKVBZUUBYRBMEBMUMZUUAYQXLXIUUEYTYPXLXIGUUEXLXIXLXIGUUEVCZUUFTU
UFTUUFSVDVEAXHYSYOVFAXHVKZYRYOMXCEAXHVGZUUGMUAUMZVKZYQYNXIXCUUJYPXDXIXCGUUJ
AXJVKZYPXDOUUGUUIUUKAUUGAXHUUIXJAUUGVHXCEXIVIVLVJUUKUAEGFYPXEUUKHUFXFUUKIUF
UUKXGXJXJUKZYPEPAXJUULAXGXJXJJVMVNEFXIXIGHIUIVOUUKXHVKZXCXCGQZXCGQZYPXCGQXC
UUMUUNYPXCGUUMYTXMXMGQZOZCERBERZUUNYPOZAUURXJXHABCDEFGHIJKVPZVQXJXHUURUUSVF
ZAXHXJUVAUUQUUSUUNUUPOBCXCXIEEYKYTUUNUUPYKXLXCXLXCGYKVCZUVBTZVRYLUUPYPUUNYL
XMXIXMXIGYLVCZUVDTVSVTWAWBWCZUOUUKXHUUOXCOZAUUCXJXHUVFVFZUUDUUCUVGVFXJUUBUV
FBXCEYKUUAUUOXLXCYKYTUUNXLXCGUVCUVBTUVBSWDUFVAWLWEUUMXCUUNGQZXCYPGQXCUUMUUN
YPXCGUVEUPUUKXHUVHXCOZAXHUVIVFZXJAXLYTGQZXLOZBERZUVJABCDEFGHIJKWFZUVLUVIBXC
EYKUVKUVHXLXCYKXLXCYTUUNGUVBUVCTUVBSWDVOWGWLWEWHVOUUGUUIVGZTUVOSWIWJWKWLUUH
UUGMEGFUUNXEUUGHUFXFUUGIUFUUGXGXHXHUKZUUNEPAXHUVPAXGXHXHJVMVNEFXCXCGHIUIVOU
UGXJVKZNUSZUVRGQZUVRGQZUVROZUUNXIGQZXIONXIEUVQNMUMZVKZUVTUWBUVRXIUWDUVSUUNU
VRXIGUWDAXHUVREPZUKZUVSUUNOZUWDAXHUWEAXHXJUWCWMAXHXJUWCWNUVQUWCUWEXJUWCUWEV
FUUGXIEUVRVIWOWLWPZUWFUURUWGAXHUURUWEUUTWQZXHUWEUURUWGVFZAUWEXHUWJUUQUWGUVS
UUPOBCUVRXCEEBNUMZYTUVSUUPUWKXLUVRXLUVRGUWKVCZUWLTZVRCUAUMZUUPUUNUVSUWNXMXC
XMXCGUWNVCZUWOTVSVTZWAWRWCVOUVQUWCVGZTUWQSUUGXJVGZAUWANERZXHXJAUUCUWSUUDUUB
UWABNEUWKUUAUVTXLUVRUWKYTUVSXLUVRGUWMUWLTUWLSVDVEVQWSUVQUVRUVSGQZUVROZXIUUN
GQZXIONXIEUWDUWTUXBUVRXIUWDUVRXIUVSUUNGUWQUWDUWFUWGUWHUWFUWEXHVKZUURUWGXHUW
EUXCAXHUWEWTWRUWIUWPXAVOTUWQSUWRAUXANERZXHXJAUVMUXDUVNUVLUXABNEUWKUVKUWTXLU
VRUWKXLUVRYTUVSGUWLUWMTUWLSVDVEVQWSWHXB $.
$}
There is a bit of a conflict between proof length and amount of DV
conditions. So far, I've been inclined to prefer fewer DV conditions at the
cost of longer proofs, because theorems can be used more easily later, as
in the example above. What version do people usually prefer?
--
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/2210a3b4-d2dc-4d20-9745-1d561faf3862n%40googlegroups.com.
