I proved the third theorem.
${
$( If multiplying two times from the left (and the right) is an identity
mapping, then the operation is commutative. $)
$d a b B $. $d a b X $. $d a b Y $. $d a b .o. $. $d a ph $.
aabbaa.a $e |- ( ph -> A. a e. B A. b e. B ( a .o. b ) e. B ) $.
aabbaa.b $e |- ( ph -> A. a e. B A. b e. B ( a .o. ( a .o. b ) ) = b ) $.
aabbaa.c $e |- ( ph -> A. a e. B A. b e. B ( ( b .o. a ) .o. a ) = b ) $.
aabbaa.d $e |- ( ph -> X e. B ) $.
aabbaa.e $e |- ( ph -> Y e. B ) $.
aabbaa $p |- ( ph -> ( X .o. Y ) = ( Y .o. X ) ) $=
( co wceq wral oveq2 id oveq1 rspc2vd mpd cv oveq12d eqeq1d eqcom
bitrdi wa
oveq1d eqeq12d eqidd wcel eleq1d oveq2d eqtrd )
ACDEMZUNCEMZCEMZDCEMAGUAZFU
AZEMZUREMZUQNZGBOFBOZUNUPNZJAVCUQUQCEMZCEMZNZVAFGCUNBBBURCNZVAVEUQNVFVGUTVE
UQVGUSVDURCEURCUQEPVGQUBUCVEUQUDUEUQUNNZUQUNVEUPVHQVHVDUOCEUQUNCERUGUHKAVGU
FBUIZAURUQEMZBUJZGBOFBOUNBUJZHAVLCUQEMZBUJVKFGCDBBBVGVJVMBURCUQERUKUQDNZVMU
NBUQDCEPUKKVILSTZSTAUODCEAUOUNUNDEMZEMZDACVPUNEAVBCVPNZJAVRUQUQDEMZDEMZNZVA
FGDCBBBURDNZVAVTUQNWAWBUTVTUQWBUSVSURDEURDUQEPWBQUBUCVTUQUDUEUQCNZUQCVTVPWC
QWCVSUNDEUQCDERUGUHLAWBUFBUIKSTULAURVJEMZUQNZGBOFBOVQDNZIAWFUNUNUQEMZEMZUQN
WEFGUNDBBBURUNNZWDWHUQWIURUNVJWGEWIQURUNUQERUBUCVNWHVQUQDVNWGVPUNEUQDUNEPUL
VNQUHVOAWIUFBUILSTUMUGUM $.
$}
Il giorno lunedì 2 dicembre 2024 alle 23:07:40 UTC+1 Glauco ha scritto:
> I'll post my progress here:
>
> https://github.com/tirix/christmas24.mm
>
>
> cool repo! :-)
>
> If you ever have the chance to record a screencast of some proof
> development (audio isn’t necessary), I’d love to check it out. It would
> help me identify features I could add to Yamma. I’m currently working on
> some improvements, and seeing your workflow from a different perspective
> would be incredibly helpful.
>
>
--
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/85532acc-8913-41be-bb57-cf0337862b72n%40googlegroups.com.
