First four bonus theorems proved. Proofs are quite short.
${
$d x y z a B $. $d x y z a .o. $. $d M a $.
mendpadmbi.a $e |- B = ( Base ` M ) $.
mendpadmbi.b $e |- .o. = ( +g ` M ) $.
mendpadmbi.c $e |- B =/= (/) $.
mendpadmbi.d $e |- M e. Mgm $.
${
$d E x a $.
$( Lemma for mendpadmbi. Mendelsohn-Padmanabhan identity implies that `
x .o. x ` is the group identity for all ` x ` . $)
mendpadmbilem1.a $e |- E = ( 0g ` M ) $.
mendpadmbilem1 $p |- ( A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o.
( x .o. ( z .o. y ) ) ) = z -> A. x e. B ( x .o. x ) = E ) $=
( va cv co wceq wral wcel a1i weq cabl c0g cfv c0 wne cmgm oveq12d
eqeq1d
oveq1 2ralbidv cbvralvw biimpi mendpadm id eqtr4di ralimi simpl2im
sylib
)
ANZBNZGOZUSCNZUTGOZGOZGOZVBPZCDQBDQZADQZMNZVIGOZEPZMDQZUSUSGOZEPZADQVHF
UARVJFUBUCZPZMDQVLVHMBCDFGHIDUDUEVHJSFUFRVHKSVHVIUTGOZVIVCGOZGOZVBPZCDQBD
QZMDQVGWAAMDAMTZVFVTBCDDWBVEVSVBWBVAVQVDVRGUSVIUTGUIUSVIVCGUIUGUHUJUKULUM
VPVKMDVPVJVOEVPUNLUOUPUQVKVNMADMATZVJVMEWCVIUSVIUSGWCUNZWDUGUHUKUR $.
$( Lemma for mendpadmbi. Mendelsohn-Padmanabhan identity implies that `
x ` to the power of ` 2 ` is the group identity for all ` x ` . $)
mendpadmbilem2.a $e |- .x. = ( .g ` M ) $.
mendpadmbilem2 $p |- ( A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o.
( x .o. ( z .o. y ) ) ) = z -> A. x e. B ( 2 .x. x ) = E ) $=
( cv co wceq wral c2 mendpadmbilem1 wcel mulg2 eqeq2 syl5ibcom ralimia
syl )
AOZBOZHPUGCOZUHHPHPHPUIQCDRBDRADRUGUGHPZFQZADRSUGEPZFQZADRABCDFGHIJ
KLMTUKUMADUGDUAULUJQUKUMDHEGUGINJUBUJFULUCUDUEUF $.
$}
$( Lemma for mendpadmbi. Mendelsohn-Padmanabhan identity implies that the
group exponent is at most 2. $)
mendpadmbilem3 $p |- ( A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. (
x .o. ( z .o. y ) ) ) = z -> ( gEx ` M ) e. ( 1 ... 2 ) ) $=
( va cmgm wcel c2 cv co wceq wral cfv eqid cn cmg c0g cgex c1 cfz 2nn
oveq1
weq oveq12d eqeq1d 2ralbidv cbvralvw mendpadmbilem2 sylbi gexlem2
mp3an12i
)
ELMNUAMAOZBOZFPZURCOZUSFPZFPZFPZVAQZCDRBDRZADRZNKOZEUBSZPEUCSZQKDRZEUDSZU
ENUFPMJUGVGVHUSFPZVHVBFPZFPZVAQZCDRBDRZKDRVKVFVQAKDAKUIZVEVPBCDDVRVDVOVAVRU
TVMVCVNFURVHUSFUHURVHVBFUHUJUKULUMKBCDVIVJEFGHIJVJTZVITZUNUOKVIVLENLDVJGVLT
VTVSUPUQ $.
$( Lemma for mendpadmbi. Mendelsohn-Padmanabhan identity implies that the
group exponent divides 2. $)
mendpadmbilem4 $p |- ( A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. (
x .o. ( z .o. y ) ) ) = z -> ( gEx ` M ) || 2 ) $=
( cv co wceq wral c1 c2 wcel cdvds wbr id cgex cfv cfz mendpadmbilem3
elpri
wo cpr fz12pr eleq2s cz 2z 1dvds ax-mp eqbrtrdi z2even jaoi 3syl )
AKZBKZFL
URCKZUSFLFLFLUTMCDNBDNADNEUAUBZOPUCLZQVAOMZVAPMZUFZVAPRSZABCDEFGHIJUDVEVAOP
UGVBVAOPUEUHUIVCVFVDVCVAOPRVCTPUJQOPRSUKPULUMUNVDVAPPRVDTUOUNUPUQ $.
$}
--
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/55fd913f-e0f0-4342-941c-a154d03f7e44n%40googlegroups.com.
