Twelfth theorem proved. Nonemptiness is not used.
I used mendpadmlem5a (proved above) instead of mendpadmlem5 to make the
proof a little shorter.
${
$d x y z a b c u v B $. $d x y z a b c u v .o. $. $d u v 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 ) $.
$( First part of ~ mendpadmlem8 $)
mendpadmlem8a $p |- ( ph -> A. x e. B A. y e. B ( x .o. ( x .o. y ) ) = y
) $=
( vu va co wceq wral weq id oveq12d oveq2d vv vb wcel mendpadmlem5a
eqeq12d
vc cv wa eqcom bitrdi rspcv mpan9 cbvralvw sylib simpr rspcdva
mendpadmlem6
adantr adantlr ad2antrr eqeq1d eqeq2d eqidd simpl rspc2vd adantll mpd
eqtrd
oveq1 oveq2 cbvral3vw simplr cmgm mgmcl syl3anc rspc3v ralrimiva
cbvral2vw
wi )
ALUGZVTUAUGZGNZGNZWAOZUAEPZLEPBUGZWFCUGZGNZGNZWGOZCEPBEPAWELEAVTEUCZUH
ZWDUAEWLWAEUCZUHZWCVTVTVTGNZGNZVTWAWOGNZGNZGNZWAWNVTWPWBWRGWLVTWPOZWMAWFWFW
FGNZGNZWFOZBEPZWKWTABCDEFGHIJKUDZXCWTBVTEBLQZXCWPVTOWTXFXBWPWFVTXFWFVTXAWOG
XFRZXFWFVTWFVTGXGXGSSXGUEWPVTUIUJUKULURWNWAWQVTGWNWAWAWAWAGNZGNZWQAWMWAXIOZ
WKAWMUHMUGZXKXKGNZGNZXKOZXJMEWAMUAQZXNXIWAOXJXOXMXIXKWAXOXKWAXLXHGXORZXOXKW
AXKWAGXPXPSSXPUEXIWAUIUJAXNMEPZWMAXDXQXEXCXNBMEBMQZXBXMWFXKXRWFXKXAXLGXRRZX
RWFXKWFXKGXSXSSSXSUEUMUNURAWMUOUPUSWNXHWOWAGWNXAWGWGGNZOZCEPBEPZXHWOOZAYBWK
WMABCDEFGHIJKUQUTWKWMYBYCVSAWKWMUHZYCXHXTOYABCWAVTEEEBUAQZXAXHXTYEWFWAWFWAG
YERZYFSVACLQZXTWOXHYGWGVTWGVTGYGRZYHSVBWKWMUOYDYEUHEVCWKWMVDVEVFVGTVHTSWNXK
UBUGZGNZXKUFUGZYIGNZGNZGNZYKOZUFEPUBEPMEPZWSWAOZWNWHWFDUGZWGGNZGNZGNZYROZDE
PCEPBEPZYPAUUCWKWMKUTUUBYOXKWGGNZXKYSGNZGNZYROYJXKYRYIGNZGNZGNZYROBCDMUBUFE
EEXRUUAUUFYRXRWHUUDYTUUEGWFXKWGGVIWFXKYSGVISVACUBQZUUFUUIYRUUJUUDYJUUEUUHGW
GYIXKGVJUUJYSUUGXKGWGYIYRGVJTSVADUFQZUUIYNYRYKUUKUUHYMYJGUUKUUGYLXKGYRYKYIG
VITTUUKRUEVKUNWNWKWOEUCZWMYPYQVSAWKWMVLZWNFVMUCZWKWKUULAUUNWKWMJUTUUMUUMEFV
TVTGHIVNVOWLWMUOYOYQVTYIGNZVTYLGNZGNZYKOWPVTYKWOGNZGNZGNZYKOMUBUFVTWOWAEEEM
LQZYNUUQYKUVAYJUUOYMUUPGXKVTYIGVIXKVTYLGVISVAYIWOOZUUQUUTYKUVBUUOWPUUPUUSGY
IWOVTGVJUVBYLUURVTGYIWOYKGVJTSVAUFUAQZUUTWSYKWAUVCUUSWRWPGUVCUURWQVTGYKWAWO
GVITTUVCRUEVPVOVGVHVQVQWDWJWFWFWAGNZGNZWAOLUABCEELBQZWCUVEWAUVFVTWFWBUVDGUV
FRVTWFWAGVISVAUACQZUVEWIWAWGUVGUVDWHWFGWAWGWFGVJTUVGRUEVRUN $.
$( Second part of ~ mendpadmlem8 $)
mendpadmlem8b $p |- ( ph -> A. x e. B A. y e. B ( ( x .o. y ) .o. y ) = x
) $=
( vu vv cv co wceq wral wcel weq id wa mendpadmlem8a ad2antrr oveq1
oveq12d
wi eqeq1d oveq2 oveq2d eqeq12d rspc2v eqcom syl6ib adantll mpd
mendpadmlem4
simplr simpr mgmcl syl3anc syl2anc eqtrd ralrimiva oveq1d cbvral2vw
sylib
cmgm )
ALNZMNZGOZVIGOZVHPZMEQZLEQBNZCNZGOZVOGOZVNPZCEQBEQAVMLEAVHERZUAZVLME
VTVIERZUAZVKVJVHVJGOZGOZVHWBVIWCVJGWBVNVPGOZVOPZCEQBEQZVIWCPZAWGVSWAABCDEFG
HIJKUBUCVSWAWGWHUFAVSWAUAWGWCVIPZWHWFWIVHVHVOGOZGOZVOPBCVHVIEEBLSZWEWKVOWLV
NVHVPWJGWLTVNVHVOGUDUEUGCMSZWKWCVOVIWMWJVJVHGVOVIVHGUHUIWMTUJUKWCVIULUMUNUO
UIWBVNVOVNGOZGOZVOPZCEQBEQZWDVHPZAWQVSWAABCDEFGHIJKUPUCWBVJERZVSWQWRUFWBFVG
RZVSWAWSAWTVSWAJUCAVSWAUQZVTWAUREFVHVIGHIUSUTXAWPWRVJVOVJGOZGOZVOPBCVJVHEEV
NVJPZWOXCVOXDVNVJWNXBGXDTVNVJVOGUHUEUGCLSZXCWDVOVHXEXBWCVJGVOVHVJGUDUIXETUJ
UKVAUOVBVCVCVLVRVNVIGOZVIGOZVNPLMBCEELBSZVKXGVHVNXHVJXFVIGVHVNVIGUDVDXHTUJM
CSZXGVQVNXIXFVPVIVOGVIVOVNGUHXITUEUGVEVF $.
$( Lemma for mendpadm. Multiplying two times from the left or right by
the same element gives the original element. $)
mendpadmlem8 $p |- ( ph -> A. x e. B A. y e. B ( ( x .o. ( x .o. y ) ) =
y /\ ( ( x .o. y ) .o. y ) = x ) ) $=
( cv co wceq wral wa mendpadmlem8a mendpadmlem8b r19.26-2 sylanbrc )
ABLZUA
CLZGMZGMUBNZCEOBEOUCUBGMUANZCEOBEOUDUEPCEOBEOABCDEFGHIJKQABCDEFGHIJKRUDUEBC
EEST $.
$}
--
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/d665456f-9d8d-4c0d-9d86-1f8d872551f6n%40googlegroups.com.
