I proved the fift theorem. Again, apparently one hypothesis is not needed,
the set B is not required to be not empty.
${
$( Lemma for mendpadm. Multiplication is surjective. $)
$d x y B $. $d x y .o. $. $d x y z 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 ) $.
mendpadmlem1 $p |- ( ph -> A. z e. B E. x e. B E. y e. B ( x .o. y ) = z
) $=
( cv co wceq wrex wcel wa wral wi mpd adantr simpr weq simplr rsp wn
pm2.21
com24 oveq12 simpl oveq2d oveq12d eqeq1d biimpd ex a1i com14 imp41
rspcimdv
syl5 cmgm pm3.22 anidms mgmcl 3expb syl2an 3expia biimprd adantll
rspcimedv
ja sylan ralrimiva )
ABLZCLZGMZDLZNZCEOZBEOZDEAVQEPZQZVQVQGMZVQWCGMZGMZVQNZ
VTWBVPVNVQVOGMZGMZGMZVQNZDERZCERZBERZWFAWMWAKUAWBWLWFBVQEAWAUBWBBDUCZQZWKWF
CVQEAWAWNUDWKWAWJSZWOCDUCZQWFWJDEUEAWAWNWQWPWFSZWAWNWQWRSSSAWPWNWQWAWFWAWJW
NWQWAWFSSSWAUFWAWQWNWFWAWQWNWFSSUGUHWAWNWQWJWFWNWQWJWFSZSSWAWNWQWSWNWQQZWJW
FWTWIWEVQWTVPWCWHWDGVNVQVOVQGUIWTVNVQWGWCGWNWQUJWTVOVQVQGWNWQUBUKULULUMUNUO
UPUQVKUQUPURUTUSUSTWBVSWFBWCEAFVAPZWAWAQZWCEPZWAJWAXBWAWAVBVCXAWAWAXCEFVQVQ
GHIVDVEVFZWBVNWCNZQVRWFCWDEWBWDEPZXEWBXCXFXDAXAWAXCXFSJXAWAXCXFEFVQWCGHIVDV
GVLTUAXEVOWDNZWFVRSWBXEXGQZVRWFXHVPWEVQVNWCVOWDGUIUMVHVIVJVJTVM $.
$}
Il giorno venerdì 6 dicembre 2024 alle 01:07:45 UTC+1 Glauco ha scritto:
> Here is my video
> https://drive.google.com/file/d/1B_hiEfuP8KE3L_6uTnfdD7wkiLP15IIp/view?usp=sharing
>
>
> Thank you, Igor, it is a really interesting video.
>
> Glauco
>
--
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/52896c9d-2b06-4f69-a965-0ccb44ca2f69n%40googlegroups.com.
