I proved the fourth theorem. It seems one hypothesis is not needed.
This proof is way too long so probably I used a very inefficient approach.
${
$( The Eckmann-Hilton argument. If for two unital magmas, represented
here by the operation ` .o. ` with unit ` E `
and the operation ` .(x) ` with unit ` I ` , on the same base set ` B
` an identity ` ( ( a .(x) b ) .o. ( c .(x) d ) ) = ( ( a .o. c ) .(x) ( b
.o. d ) ) `
holds, then these magmas coincide and the operation is associative and
commutative. $)
$d a b c d e v B $. $d a b c d e v E $. $d a b c d e v I $.
$d a b c d e v .o. $. $d a b c d e v .(x) $. $d a b c d e v ph $.
eckmannhilton.a $e |- ( ph -> A. a e. B A. b e. B ( a .o. b ) e. B ) $.
eckmannhilton.c $e |- ( ph -> A. a e. B ( ( a .o. E ) = a /\ ( E .o. a )
= a ) ) $.
eckmannhilton.d $e |- ( ph -> A. a e. B ( ( a .(x) I ) = a /\ ( I .(x) a
) = a ) ) $.
eckmannhilton.e $e |- ( ph -> ( E e. B /\ I e. B ) ) $.
eckmannhilton.f $e |- ( ph -> A. a e. B A. b e. B A. c e. B A. d e. B ( (
a .(x) b ) .o. ( c .(x) d ) ) = ( ( a .o. c ) .(x) ( b .o. d ) ) ) $.
iden $p |- ( ph -> E = I ) $=
( co wceq wral oveq2 eqeq12d cv wa r19.26 simpld wb id bitrdi adantl
rspcdv
wcel eqcom adantld syl5bi mpd syl6ib adantrd oveq12d oveq1d 2ralbidv
oveq2d
oveq1 simprd eqidd rspc2vd syld 3eqtrd )
ADDDFPZEECPZEAGUAZDFPZVIQZDVIFPZVI
QZUBGBRZDVGQZLVNVKGBRZVMGBRZUBZAVOVKVMGBUCZAVQVOVPAVMVOGDBADBUJZEBUJZNUDZVI
DQZVMVOUEAWCVMVGDQVOWCVLVGVIDVIDDFSWCUFZTVGDUKUGUHUIULUMUNAVGEDCPZDECPZFPZE
DFPZDEFPZCPZVHADWEDWFFAVIECPZVIQZEVICPZVIQZUBGBRZDWEQZMWOWLGBRZWNGBRZUBZAWP
WLWNGBUCZAWRWPWQAWRWEDQZWPAWNXAGDBWBWCWNXAUEAWCWMWEVIDVIDECSWDTUHUIWEDUKUOU
LUMUNAWODWFQZMWOWSAXBWTAWQXBWRAWQWFDQZXBAWLXCGDBWBWCWLXCUEAWCWKWFVIDVIDECVA
WDTUHUIWFDUKUOUPUMUNUQAVIHUAZCPZIUAZJUAZCPZFPZVIXFFPZXDXGFPZCPZQZJBRIBRZHBR
GBRZWGWJQZOAXOWEXHFPZEXFFPZDXGFPZCPZQZJBRIBRZXPAYBEXDCPZXHFPZXRXKCPZQZJBRIB
RXNGHEDBBBVIEQZXMYFIJBBYGXIYDXLYEYGXEYCXHFVIEXDCVAURYGXJXRXKCVIEXFFVAURTUSX
DDQZYFYAIJBBYHYDXQYEXTYHYCWEXHFXDDECSURYHXKXSXRCXDDXGFVAUTTUSAVTWANVBZAYGUB
BVCWBVDAXPWEDXGCPZFPZWHXSCPZQYAIJDEBBBXFDQZXQYKXTYLYMXHYJWEFXFDXGCVAUTYMXRW
HXSCXFDEFSURTXGEQZYKWGYLWJYNYJWFWEFXGEDCSUTYNXSWIWHCXGEDFSUTTWBAYMUBBVCYIVD
VEUNAWHEWIECAVNWHEQZLVNVRAYOVSAVPYOVQAVKYOGEBYIYGVKYOUEAYGVJWHVIEVIEDFVAYGU
FZTUHUIUPUMUNAVNWIEQZLVNVRAYQVSAVQYQVPAVMYQGEBYIYGVMYQUEAYGVLWIVIEVIEDFSYPT
UHUIULUMUNUQVFAWOVHEQZMWOWSAYRWTAWRYRWQAWNYRGEBYIYGWNYRUEAYGWMVHVIEVIEECSYP
TUHUIULUMUNVF $.
mcoinc $p |- ( ph -> A. a e. B A. b e. B ( a .o. b ) = ( a .(x) b ) ) $=
( co wceq wral wa ralimi cv wi syl r19.26 iden oveq2d eqeq1d biimpd
ralimdv
simpl adantrd syl5bi mpd sylanbrc ralrimivw ralcom sylib oveq1d adantld
weq
simpr oveq2 id eqeq12d anbi12d biimpri sylbir syl2anc simpll simprl
oveq12d
cbvralvw simplr simprr ralim 3syl ralbii sylbb anim2i 2ralbidv simprd
eqidd
wcel rspc2vd imp biimpi sylc )
AGUAZECPZEHUAZCPZFPZWHEFPZEWJFPZCPZQZHBRZWHW
JFPZWHWJCPZQZHBRZUBZGBRZWQGBRZXAGBRAWIWHQZWMWHQZSZWKWJQZWNWJQZSZSZHBRZGBRZW
PWTUBZHBRZGBRXCAXGHBRZGBRZXJHBRZGBRZXMAXGGBRZHBRXQAXTHBAXEGBRZXFGBRZXTAXEEW
HCPZWHQZSZGBRZYAMYEXEGBXEYDUJTUCAWHDFPZWHQZDWHFPZWHQZSZGBRZYBLYLYHGBRZYJGBR
ZSAYBYHYJGBUDAYMYBYNAYHXFGBAYHXFAYGWMWHADEWHFABCDEFGHIJKLMNOUEZUFUGUHUIUKUL
UMXEXFGBUDUNUOXGHGBBUPUQAXRGBAYDEWHFPZWHQZSZGBRZXRAYDGBRZYQGBRZYSAYFYTMYEYD
GBXEYDVATUCAYLUUALAYKYQGBAYJYQYHAYJYQAYIYPWHADEWHFYOURUGUHUSUIUMYDYQGBUDUNY
RXJGHBGHUTZYDXHYQXIUUBYCWKWHWJWHWJECVBUUBVCZVDUUBYPWNWHWJWHWJEFVBUUCVDVEVLU
QUOXQXSSXPXRSZGBRXMXPXRGBUDUUDXLGBXLUUDXGXJHBUDVFTVGVHXLXOGBXKXNHBXKWPWTXKW
LWRWOWSXKWIWHWKWJFXEXFXJVIXGXHXIVJVKXKWMWHWNWJCXEXFXJVMXGXHXIVNVKVDUHTTXOXB
GBWPWTHBVOTVPAWIEJUAZCPZFPZWMEUUEFPZCPZQZJBRZGBRZXDAAWSIUAZUUECPZFPZWHUUMFP
ZWJUUEFPZCPZQZJBRZGBRZIBRZHBRZSZUULAAUUTIBRZHBRGBRZUVDAVCOUVFUVCAUVFUVEGBRZ
HBRUVCUVEGHBBUPUVGUVBHBUUTGIBBUPVQVRVSVHAUVCUULAUULWIUUNFPZUUPUUHCPZQZJBRGB
RUVAHIEEBBBWJEQZUUSUVJGJBBUVKUUOUVHUURUVIUVKWSWIUUNFWJEWHCVBURUVKUUQUUHUUPC
UVKWJEUUEFUVKVCURUFVDVTUUMEQZUVJUUJGJBBUVLUVHUUGUVIUUIUVLUUNUUFWIFUVLUUMEUU
ECUVLVCURUFUVLUUPWMUUHCUUMEWHFVBURVDVTADBWCEBWCNWAZAUVKSBWBUVMWDWEUCUUKWQGB
UUKWQUUJWPJHBJHUTZUUGWLUUIWOUVNUUFWKWIFUUEWJECVBUFUVNUUHWNWMCUUEWJEFVBUFVDV
LWFTUCWQXAGBVOWG $.
eckmannhilton $p |- ( ph -> ( E = I /\ A. a e. B A. b e. B ( ( a .o. b )
= ( a .(x) b ) /\ ( a .o. b ) = ( b .o. a ) ) /\
A. a e. B A. b e. B A. c e. B ( ( a .o. b ) .o. c )
= ( a .o. ( b .o. c ) ) ) ) $=
( wceq co wral syl wi vv ve cv wa iden mcoinc id ralcom ralbii bitri biimpi
oveq1 oveq1d eqeq12d ralbidv oveq2 oveq2d wcel simpr eqidd rspc2vd
cbvralvw
mpd weq jca ralimi a1i com12 ralrimiv r19.26 imp bicomi eqeq1d impd
ralimdv
biimpd com13 oveq12 wb eqcom eqeq2 ralim simpll simplr oveq12d rspcdv
bitrd
imim1i idd simpllr eleq12d cbvral2vw rsp imim2i simp2 3exp syld com45
com34
ex com23 eqeq2d mpdd 3jca )
ADEPZGUCZHUCZFQZXFXGCQZPZXHXGXFFQZPZUDHBRZGBRZX
HIUCZFQZXFXGXOFQZFQZPZIBRZHBRZGBRZABCDEFGHIJKLMNOUEZAXJHBRZXLHBRZUDZGBRZXNA
YDGBRZYEGBRZUDZYGAYHYIABCDEFGHIJKLMNOUFZAAEXFCQZXGECQZFQZEXGFQZXFEFQZCQZPZH
BRZGBRZUDYIAAYTAUGAEXGCQZXOECQZFQZEXOFQZXGEFQZCQZPZIBRZHBRZYTAXIXOJUCZCQZFQ
ZXFXOFQZXGUUJFQZCQZPZIBRZHBRZJBRZGBRZUUIAUUPJBRZIBRZHBRZGBRZUUTOUVDUUTUVCUU
SGBUVCUUQJBRZHBRUUSUVBUVEHBUUPIJBBUHUIUUQHJBBUHUJUIUKSAUUIUUAUUKFQZUUDUUNCQ
ZPZIBRZHBRUURGJEEBBBXFEPZUUQUVIHBUVJUUPUVHIBUVJUULUVFUUOUVGUVJXIUUAUUKFXFEX
GCULUMUVJUUMUUDUUNCXFEXOFULUMUNUOUOUUJEPZUVIUUHHBUVKUVHUUGIBUVKUVFUUCUVGUUF
UVKUUKUUBUUAFUUJEXOCUPUQUVKUUNUUEUUDCUUJEXGFUPUQUNUOUOADBURZEBURZUDUVMNUVLU
VMUSSZAUVJUDBUTUVNVAVCUUIYTUUIYLUUBFQZUUDYPCQZPZIBRZGBRYTUUHUVRHGBHGVDZUUGU
VQIBUVSUUCUVOUUFUVPUVSUUAYLUUBFUVSXGXFECUVSUGZUQUMUVSUUEYPUUDCUVSXGXFEFUVTU
MUQUNUOVBUVRYSGBUVQYRIHBIHVDZUVOYNUVPYQUWAUUBYMYLFUWAXOXGECUWAUGZUMUQUWAUUD
YOYPCUWAXOXGEFUWBUQUMUNVBUIUJUKSVEAYTYIAYSYETZGBRZYTYITAYRXLTZHBRZGBRZUWDAY
LXFPZYMXGPZUDZYQXKPZUDZHBRZGBRZUWGAUWJHBRZGBRZUWKHBRZGBRZUDZUWNAUWPUWRAUWHH
BRZGBRZUWIHBRZGBRZUDZUWPAUXAUXCAUWHGBRZHBRZUXAAUXEHBXGBURZAUXEAUXETUXGAXFEC
QZXFPZUWHUDZGBRZUXEMUXJUWHGBUXIUWHUSVFSVGVHVIUXFUXAUWHHGBBUHUKSAUXBGBXFBURZ
AUXBAUXBTUXLAUXKUXBMUXKUXIGBRZUXEUDZUXBUXKUXNUXIUWHGBVJUKUXMUXEUXBUXEUXMUXB
UXMUXBTUXEUXMUXBUXIUWIGHBGHVDZUXHYMXFXGUXOXFXGECUXOUGZUMUXPUNVBUKVGVHVKSSVG
VHVIVEUXDUWPUXDUWTUXBUDZGBRZUWPUXRUXDUWTUXBGBVJVLUXQUWOGBUWOUXQUWHUWIHBVJVL
UIUJUKSAYQXGXFCQZPZHBRZGBRZUWRAYOXGPZYPXFPZUDZHBRZGBRZUYBAUYCHBRZGBRZUYDHBR
ZGBRZUDZUYGAUYIUYKAUYHGBUXLAUYHAUYHTUXLAEXFFQZXFPZGBRZUYHAXFDFQZXFPZDXFFQZX
FPZUDZGBRZUYOLAUYTUYNGBAUYQUYSUYNUYQAUYSUYNTZAVUBTUYQAUYSUYNAUYRUYMXFADEXFF
YCUMVMVPVGVHVNVOVCUYOUYHTAUYOUYHUYNUYCGHBUXOUYMYOXFXGXFXGEFUPUXPUNVBUKVGVCV
GVHVIAUYDGBRZHBRZUYKAVUCHBUXGAVUCAVUCTZUXGAXEVUCYCXEAVUCVUEXEAVUAVUCLAUYTUY
DGBAUYQUYSUYDUYSUYQAUYDUYQAUYDTTUYSAUYQUYDAUYQUYDAUYPYPXFADEXFFYCUQZVMVPVHV
GVQVNVOVCVGVHVCVGVHVIVUDUYKUYDHGBBUHUKSVEUYLUYGUYGUYLUYGUYHUYJUDZGBRUYLUYFV
UGGBUYCUYDHBVJUIUYHUYJGBVJUJVLUKSUYFUYAGBUYEUXTHBYOXGYPXFCVRVFVFSAUYAUWQTZG
BRZUYBUWRTAUXTUWKTZHBRZGBRZVUIAYHVULYKYHUAUCZUBUCZFQZVUMVUNCQZPZUBBRZUABRZV
ULYHVUSYHXFVUNFQZXFVUNCQZPZUBBRZGBRVUSYDVVCGBXJVVBHUBBHUBVDXHVUTXIVVAXGVUNX
FFUPXGVUNXFCUPUNVBUIVVCVURGUABGUAVDZVVBVUQUBBVVDVUTVUOVVAVUPXFVUMVUNFULXFVU
MVUNCULUNUOVBUJUKVUSXGVUNFQZXGVUNCQZPZUBBRZHBRZVULVUSVVIVURVVHUAHBUAHVDZVUQ
VVGUBBVVJVUOVVEVUPVVFVUMXGVUNFULVUMXGVUNCULUNUOVBUKVVIXKUXSPZGBRZHBRZVULVVI
VVMVVHVVLHBVVGVVKUBGBUBGVDZVVEXKVVFUXSVUNXFXGFUPVUNXFXGCUPUNVBUIUKVVMVVKHBR
ZGBRZVULVVMVVPVVKHGBBUHUKVVOVUKGBVVKVUJHBVVKUXTUWKVVKUXSXKPZUXTUWKVSVVKVVQX
KUXSVTUKUXSXKYQWASVPVFVFSSSSSVUKVUHGBUXTUWKHBWBVFSUYAUWQGBWBSVCVEUWSUWNUWNU
WSUWNUWOUWQUDZGBRUWSUWMVVRGBUWJUWKHBVJUIUWOUWQGBVJUJVLUKSUWMUWFGBUWLUWEHBUW
LYRXLUWLYNXHYQXKUWLYLXFYMXGFUWHUWIUWKWCUWHUWIUWKWDWEUWJUWKUSUNVPVFVFSUWFUWC
GBYRXLHBWBVFSYSYEGBWBSVKSVEYJYGYGYJYDYEGBVJVLUKSYFXMGBYFXMXMYFXJXLHBVJVLUKV
FSAUVDYBOAUVDXHUUJFQZXFUUNFQZPZJBRZHBRZGBRZYBAUVDXIEUUJCQZFQZYPUUNCQZPZJBRZ
HBRZGBRZVWDAUVAHBRZGBRZIBRZVWKTUVDVWKTAVWMVWKIEBUVNAXOEPZVWMVWKVSZVWOVWPTAV
WOVWLVWJGBVWOUVAVWIHBVWOUUPVWHJBVWOUULVWFUUOVWGVWOUUKVWEXIFVWOXOEUUJCVWOUGZ
UMUQVWOUUMYPUUNCVWOXOEXFFVWQUQUMUNUOUOUOVGVKWFUVDVWNVWKUVDVWNUVDVWLIBRZGBRV
WNUVCVWRGBUVAHIBBUHUIVWLGIBBUHUJUKWHSUVDAVWKVWDTZAVWSTUVDAVWJVWCTZGBRZVWSAV
WIVWBTZHBRZGBRZVXAAVWHVWATZJBRZHBRZGBRZVXDAXIXHPZVWEUUJPZUDZVWGVVTPZUDZJBRZ
HBRZGBRZVXHAVXKJBRZHBRZGBRZVXLJBRZHBRZGBRZUDZVXPAVXSVYBAVXIJBRZHBRZGBRZVXJJ
BRZHBRZGBRZUDZVXSAVYFVYIAVXIHBRZGBRZJBRZVYFAVYLJBUUJBURZAVYLAVYLTVYNAYHVYLY
KYDVYKGBXJVXIHBXJVXIXHXIVTUKVFVFSVGVHVIVYMVYFVYMVYKJBRZGBRVYFVYKJGBBUHVYOVY
EGBVXIJHBBUHUIUJUKSAVYHGBUXLAVYHAVYHTUXLAVYGHBUXGAVYGAVYGTUXGAUXEVYGAUXKUXE
MAUXJUWHGBUXJAUWHUXIUWHAUWHTZUWHVYPTUXIAUWHUWHAUWHWIVHVGVKVHVOVCUXEVYGUWHVX
JGJBGJVDZYLVWEXFUUJXFUUJECUPVYQUGUNVBUKSVGVHVIVGVHVIVEVYJVXSVYJVYEVYHUDZGBR
ZVXSVYSVYJVYEVYHGBVJVLVYSVYDVYGUDZHBRZGBRVXSVYRWUAGBWUAVYRVYDVYGHBVJVLUIWUA
VXRGBVYTVXQHBVXQVYTVXIVXJJBVJVLUIUIUJUJUKSAXFUUNCQZVVTPZJBRZHBRZGBRZVYBAWUE
GBAUXLWUEAUXLUDZWUDHBWUGUXGWUDWUGUXGUDZWUCJBWUGUXGVYNWUCTZAUXLUXGWUITZAYHUX
LWUJTYKAUXLYHWUJAUXLUXGYHWUIAUXLUXGVYNYHWUCAUXLUXGVYNYHWUCTZTZTWUGUXGWULWUH
VYNWUKWUHVYNUDZVUNVUMFQZVUNVUMCQZPZUABRUBBRZWUCTWUKWUMWUCXFVUMCQZXFVUMFQZPZ
WUPUBUAXFUUNBBBVVNWUPWUOWUNPZWUTWUPWVAVSVVNWUNWUOVTVGVVNWUOWURWUNWUSVUNXFVU
MCULVUNXFVUMFULUNWGVUMUUNPZWURWUBWUSVVTWVBVUMUUNXFCWVBUGZUQWVBVUMUUNXFFWVCU
QUNAUXLUXGVYNWJWUMVVNUDBUTWUHVYNUUNBURZWUGUXGVYNWVDTZAUXLUXGWVETZAWVDJBRZHB
RZUXLWVFTZAXHBURZHBRGBRZWVHKWVKWVHWVKVUMUUJFQZBURZJBRZUABRWVHWVJWVMVUMXGFQZ
BURGHUAJBBVVDXHWVOBBXFVUMXGFULVVDBUTWKHJVDZWVOWVLBBXGUUJVUMFUPWVPBUTWKWLWVN
WVGUAHBVVJWVMWVDJBVVJWVLUUNBBVUMXGUUJFULVVJBUTWKUOVBUJUKSAWVHWVFWVIWVHWVFTA
WVHUXGWVGTWVFWVGHBWMWVGWVEUXGWVDJBWMWNSVGAWVFUXLWVFAWVFUXLWOWPWQVCVKVKVKVAY
HWUQWUCYHWUQXJWUPVUNXGFQZVUNXGCQZPGHUBUABBGUBVDXHWVQXIWVRXFVUNXGFULXFVUNXGC
ULUNHUAVDWVQWUNWVRWUOXGVUMVUNFUPXGVUMVUNCUPUNWLUKWHSWTWTWTWRWSXAVCVKVKVIWTV
IWTVIAWUEVYATZGBRZWUFVYBTAXFYPPZGBRZWVTAVUAWWBLAUYQGBRZUYSGBRZUDZWWBTVUAWWB
TAWWCWWDWWBWWDWWCAWWBWWCAWWBTTWWDAWWCWWBAUYQWWAGBAXFUYPPZWWATUYQWWATAWWFWWA
AUYPYPXFVUFXBVPUYQWWFWWAUYQWWFUYPXFVTUKWHSVOVHVGVQVNVUAWWEWWBVUAWWEUYQUYSGB
VJUKWHSVCWWAWVSGBWWAWUDVXTHBWWAWUCVXLJBWWAWUCVXLWWAWUBVWGVVTWWAXFYPUUNCWWAU
GUMVMVPVOVOVFSWUEVYAGBWBSVCVEVYCVXPVYCVXRVYAUDZGBRZVXPWWHVYCVXRVYAGBVJVLWWH
VXQVXTUDZHBRZGBRVXPWWGWWJGBWWJWWGVXQVXTHBVJVLUIWWJVXOGBWWIVXNHBVXNWWIVXKVXL
JBVJVLUIUIUJUJUKSVXOVXGGBVXNVXFHBVXMVXEJBVXMVWHVWAVXMVWFVVSVWGVVTVXMXIXHVWE
UUJFVXIVXJVXLWCVXIVXJVXLWDWEVXKVXLUSUNVPVFVFVFSVXGVXCGBVXFVXBHBVWHVWAJBWBVF
VFSVXCVWTGBVWIVWBHBWBVFSVWJVWCGBWBSVGVHXCUVDVWDYBTZTAWWKUVDVWDYBVWCYAGBVWBX
THBVWAXSJIBJIVDZVVSXPVVTXRWWLUUJXOXHFWWLUGZUQWWLUUNXQXFFWWLUUJXOXGFWWMUQUQU
NVBUIUIUKVGVGXCVCXD $.
$}
Il giorno martedì 3 dicembre 2024 alle 05:27:20 UTC+1 savask ha scritto:
> > Saveliy, could you please comment on that (is it legal to add a
> disjoint for a and b and what was your intention)?
>
>
> Yes, it is legal to add or remove disjoints if you need it for the proof.
> I don't have a very good intuition behind disjoint conditions, so it seems
> I missed some in the statements.
>
>
> > I used mm-lamp, and it has some automation to prove such steps (no need
> to write any code, it is available out of the box). ... Will it not break
> any rules of this initiative, if I show how to prove abaeqb?
>
>
> Sure, please share the video, it would be very interesting to take a look
> at mm-lamp automation.
>
--
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/399f3f91-e2d9-4ca5-ab5f-30df2e627be7n%40googlegroups.com.
