One theorem left:
${
$d x y a b B $. $d x y a b .o. $. $d M a b $.
mendpadmbi.a $e |- B = ( Base ` M ) $.
mendpadmbi.b $e |- .o. = ( +g ` M ) $.
$( Lemma for mendpadmbi. In a group of exponent dividing 2 we have ` x
.o. x .o. y = y ` for all ` x ` and ` y ` . $)
mendpadmbilem5a $p |- ( ( M e. Grp /\ ( gEx ` M ) || 2 ) -> A. x e. B A.
y e. B ( x .o. ( x .o. y ) ) = y ) $=
( va vb wcel cfv c2 wa cv co wceq wral eqid 3ad2ant2 3eqtr3rd cgrp cgex
wbr
cdvds c0g cmg gexid adantl w3a 3anan32 gexdvdsi eqcomd sylbir eqtr3d
adantr
mulg2 oveq1d grplid ad4ant14 simplll simplr simpr grpass syl13anc
ralrimiva
weq id oveq1 oveq12d eqeq1d oveq2 oveq2d eqeq12d cbvral2vw sylib )
DUAJZDUB
KZLUDUCZMZHNZVTINZEOZEOZWAPZICQZHCQANZWFBNZEOZEOZWGPZBCQACQVSWEHCVSVTCJZMZW
DICWLWACJZMZDUEKZWAEOZVTVTEOZWAEOZWAWCWNWOWQWAEWLWOWQPWMWLVQVTDUFKZOZWOWQWK
WTWOPVSVTWSVQDCWOFVQRZWSRZWORZUGZUHWLVPWKVRUIZWTWQPVPWKVRUJXELVTWSOZWOWQWTV
TWSVQDLCWOFXAXBXCUKWKVPXFWQPVRCEWSDVTFXBGUPSWKVPWOWTPVRWKWTWOXDULSTUMUNUOUQ
VPWMWPWAPVRWKCEDWAWOFGXCURUSWNVPWKWKWMWRWCPVPVRWKWMUTVSWKWMVAZXGWLWMVBCEDVT
VTWAFGVCVDTVEVEWDWJWFWFWAEOZEOZWAPHIABCCHAVFZWCXIWAXJVTWFWBXHEXJVGVTWFWAEVH
VIVJIBVFZXIWIWAWGXKXHWHWFEWAWGWFEVKVLXKVGVMVNVO $.
$( Lemma for mendpadmbi. In an abelian group of exponent dividing 2 we
have ` x .o. x .o. y = y ` for all ` x ` and ` y ` . $)
mendpadmbilem5 $p |- ( ( M e. Abel /\ ( gEx ` M ) || 2 ) -> A. x e. B A.
y e. B ( x .o. ( x .o. y ) ) = y ) $=
( cabl wcel cgrp cgex cfv c2 cdvds wbr cv co wceq wral ablgrp sylan
mendpadmbilem5a ) DHIDJIDKLMNOAPZUCBPZEQEQUDRBCSACSDTABCDEFGUBUA $.
$}
--
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/d47c53d5-29f8-4159-8a59-e9eb9f7f1418n%40googlegroups.com.
