Sixth theorem proved:
${
$( Lemma for mendpadm. Multiplication is surjective. $)
$d x y z a b c B $. $d x y z a b c .o. $. $d x 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 ) $.
$( Lemma for mendpadm. Multiplication by ` x ` from the left is
surjective. $)
mendpadmlem2 $p |- ( ph -> A. z e. B A. x e. B E. y e. B ( x .o. y ) = z
) $=
( va vc co wceq wi wral oveq1 eqeq1d oveq2d vb cv wcel wrex wal wa cmgm
w3a
simp1 mgmcl 3com23 simp3 syl3anc syld3an3 3exp syl imp31 ad2antrr weq
oveq2
oveq12d eqeq12d cbvral3vw sylib com23 simplr rspc3v mpd simpr oveq1d
rspcev
id mpbid syl2anc ex alrimiv df-ral imbi2i albii sylbbr )
ADUBZEUCZBUBZEUCZW
CCUBZGNZWAOZCEUDZPZBUEZPZDUEZWHBEQZDEQZAWKDAWBWJAWBUFZWIBWOWDWHWOWDUFZWCWAG
NZWAWCWQGNZGNZGNZEUCZWCWTGNZWAOZWHAWBWDXAAFUGUCZWBWDXAPPJXDWBWDXAXDWBWDUHZX
DWQEUCZWSEUCZXAXDWBWDUIZXDWDWBXFEFWCWAGHIUJZUKZXDWBWDWREUCZXGXEXDWDXFXKXHXD
WBWDULXJEFWCWQGHIUJUMZEFWAWRGHIUJUNEFWQWSGHIUJUMUOUPUQWPWQWRGNZWTGNZWAOZXCW
PLUBZUAUBZGNZXPMUBZXQGNZGNZGNZXSOZMEQUAEQLEQZXOWPWFWCWAWEGNZGNZGNZWAOZDEQCE
QBEQZYDAYIWBWDKURYHYCXPWEGNZXPYEGNZGNZWAOXRXPWAXQGNZGNZGNZWAOBCDLUAMEEEBLUS
ZYGYLWAYPWFYJYFYKGWCXPWEGRWCXPYEGRVASCUAUSZYLYOWAYQYJXRYKYNGWEXQXPGUTYQYEYM
XPGWEXQWAGUTTVASDMUSZYOYBWAXSYRYNYAXRGYRYMXTXPGWAXSXQGRTTYRVLVBVCVDZWPXFXKW
BYDXOPAWBWDXFAXDWBWDXFPPJXDWDWBXFXDWDWBXFXIUOVEUPUQAWBWDXKAXDWBWDXKPPJXDWBW
DXKXLUOUPUQAWBWDVFZYCXOWQXQGNZWQXTGNZGNZXSOXMWQXSWRGNZGNZGNZXSOLUAMWQWRWAEE
EXPWQOZYBUUCXSUUGXRUUAYAUUBGXPWQXQGRXPWQXTGRVASXQWROZUUCUUFXSUUHUUAXMUUBUUE
GXQWRWQGUTUUHXTUUDWQGXQWRXSGUTTVASMDUSZUUFXNXSWAUUIUUEWTXMGUUIUUDWSWQGXSWAW
RGRTTUUIVLVBVGUMVHWPXNXBWAWPXMWCWTGWPYDXMWCOZYSWPWDWBWDYDUUJPWOWDVIZYTUUKYC
UUJWCXQGNZWCXTGNZGNZXSOWQWCXSWAGNZGNZGNZXSOLUAMWCWAWCEEELBUSZYBUUNXSUURXRUU
LYAUUMGXPWCXQGRXPWCXTGRVASUADUSZUUNUUQXSUUSUULWQUUMUUPGXQWAWCGUTUUSXTUUOWCG
XQWAXSGUTTVASMBUSZUUQXMXSWCUUTUUPWRWQGUUTUUOWQWCGXSWCWAGRTTUUTVLVBVGUMVHVJS
VMWGXCCWTEWEWTOWFXBWAWEWTWCGUTSVKVNVOVPVOVPWNWBWMPZDUEWLWMDEVQUVAWKDWMWJWBW
HBEVQVRVSVTUP $.
$}
As a side note, Tirix is now close to completing the proof of the
Eckmann-Hilton argument, and although his version is better organized than
mine, it still looks pretty long. I guess now we can say that the short
proof on Wikipedia doesn't convey a good idea about the amount of work
needed to accomplish that task.
Il giorno sabato 7 dicembre 2024 alle 11:44:15 UTC+1 [email protected] ha
scritto:
> > *Thank you, Igor, it is a really interesting video.*
>
>
> Thanks, Glauco! Yamma’s feature of proposing a list of theorems is also
> very useful. I want to add such a feature to mm-lamp in the future.
>
>
> > *there's potential for improving the search maybe by adding special
> tactics for set.mm <http://set.mm> which narrow down the search with
> specific theorems banned/allowed.*
>
>
> Thanks for the feedback! Current implementation of the bottom-up prover
> allows to provide a list of theorems to use. Also it is possible to narrow
> down usage of some theorems to some specific scenarios. For example, to
> allow usage of syl only when the first hypothesis is of the form of |- ( ph
> -> X e. A ) and the conclusion is |- ( ph -> Y = ( X ^ N ) ). With
> appropriately collected list of theorems to use and such rules for
> narrowing down usage of some theorems, the bottom-up prover becomes very
> fast, so I don’t even need to specify statement length restriction. But
> all of these are available in macros only. I also have a few more ideas
> to try, for example, making bottom-up prover parameters dynamic, so they
> depend on what is needed to prove. Currently I am working on a few other
> improvements which will affect macros API. After that I will start
> documenting the macros feature.
>
>
> On Saturday, December 7, 2024 at 8:09:48 AM UTC+1 savask wrote:
>
>> > Here is my video ...
>>
>> It was very interesting, thanks. For me the highlight of the video was
>> the "proving bottom-up" dialog, which can search for proofs of large depth
>> automatically. Metamath.exe also has one (the "improve" command), and mmj2
>> doesn't, as far as I'm aware, so in a sense metamath-lamp has partly
>> surpassed mmj2 in functionality.
>>
>> There was an interesting part near the end where the proof search
>> couldn't figure out that A e. CC is implied by A e. RR, since the latter
>> statement has the same length and hence isn't picked up by the "Less"
>> search heuristic. I think mmj2's transformation script
>> <https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js>
>>
>> can circumvent such issues in special cases, so there's potential for
>> improving the search maybe by adding special tactics for set.mm which
>> narrow down the search with specific theorems banned/allowed.
>>
>> > I proved the fifth theorem. Again, apparently one hypothesis is not
>> needed, the set B is not required to be not empty.
>>
>> Nice! You shouldn't require nonemptyness until lemma 7, which postulates
>> the existence of unity. I think it's a bit unfortunate that we allow empty
>> magmas, since algebraic structures are usually assumed to be based on
>> nonempty sets; this makes the theory more uniform.
>>
>
--
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/9f1b8989-4ca0-40af-83a0-cb5523bd6cdfn%40googlegroups.com.
