Part 2 is, of course, making a version of this which is suitable for set.mm.
On Sun, Dec 15, 2024 at 1:16 AM Gino Giotto <[email protected]> wrote: > Last theorem proved: > > ${ > $d x y z a b c B $. $d x y z a b c .o. $. $d M a b c $. > mendpadmbi.a $e |- B = ( Base ` M ) $. > mendpadmbi.b $e |- .o. = ( +g ` M ) $. > mendpadmbi.c $e |- B =/= (/) $. > mendpadmbi.d $e |- M e. Mgm $. > $( Boolean groups are characterized by an identiy of N.S. Mendelsohn and > R. Padmanabhan. $) > mendpadmbi $p |- ( A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x > .o. ( z .o. y ) ) ) = z <-> ( M e. Abel /\ ( gEx ` M ) || 2 ) ) $= > ( va vb vc cv co wceq wral wcel oveq1 oveq2d cabl cgex cfv c2 cdvds > wbr c0g > wa wne a1i cmgm weq oveq12d eqeq1d 2ralbidv cbvralvw biimpi mendpadm > simpld > c0 mendpadmbilem4 jca cgrp wi simpl ablgrp grpass 3exp2 3syl > mendpadmbilem5 > imp41 ad3antrrr mgmcl mp3an1 oveq2 eqeq12d rspc2v sylan adantlll mpd > ablcom > id ad5ant145 3eqtr3rd ralrimiva cbvral3vw sylib impbii ) > ANZBNZFOZWICNZWJFO > > ZFOZFOZWLPZCDQBDQZADQZEUARZEUBUCUDUEUFZUHZWRWSWTWRWSKNZXBFOEUGUCPKDQWRKBCDE > > FGHDUTUIWRIUJEUKRZWRJUJWRXBWJFOZXBWMFOZFOZWLPZCDQBDQZKDQWQXHAKDAKULZWPXGBCD > > DXIWOXFWLXIWKXDWNXEFWIXBWJFSWIXBWMFSUMUNUOUPUQURUSABCDEFGHIJVAVBXAXBLNZFOZX > > BMNZXJFOZFOZFOZXLPZMDQZLDQZKDQWRXAXRKDXAXBDRZUHZXQLDXTXJDRZUHZXPMDYBXLDRZUH > > ZXKXKXLFOZFOZXKXBXJXLFOZFOZFOXLXOYDYEYHXKFXAXSYAYCYEYHPZXAWSEVCRZXSYAYCYIVD > > VDVDWSWTVEEVFYJXSYAYCYIDFEXBXJXLGHVGVHVIVKTYDWIWKFOZWJPZBDQADQZYFXLPZXAYMXS > > YAYCABDEFGHVJVLXSYAYCYMYNVDZXAXSYAUHXKDRZYCYOXCXSYAYPJDEXBXJFGHVMVNYLYNXKXK > > WJFOZFOZWJPABXKXLDDWIXKPZYKYRWJYSWIXKWKYQFYSWBWIXKWJFSUMUNBMULZYRYFWJXLYTYQ > > YEXKFWJXLXKFVOTYTWBVPVQVRVSVTYDYHXNXKFYDYGXMXBFWSYAYCYGXMPWTXSDFEXJXLGHWAWC > > TTWDWEWEWEXPWPWIXJFOZWIXMFOZFOZXLPWKWIXLWJFOZFOZFOZXLPKLMABCDDDKAULZXOUUCXL > > UUGXKUUAXNUUBFXBWIXJFSXBWIXMFSUMUNLBULZUUCUUFXLUUHUUAWKUUBUUEFXJWJWIFVOUUHX > > MUUDWIFXJWJXLFVOTUMUNMCULZUUFWOXLWLUUIUUEWNWKFUUIUUDWMWIFXLWLWJFSTTUUIWBVPW > FWGWH $. > $} > > I guess this is the end. Nice challenge, I enjoyed it. > > -- > 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/27f7b052-78a8-4b02-b269-0e817bb9bb65n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/27f7b052-78a8-4b02-b269-0e817bb9bb65n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSuxea7otER-7QSqtqU-arnLcyjFfrheR12CVe91YtAtgw%40mail.gmail.com.
