Seventh theorem proved:
${
$d x y z a b c B $. $d x y z a b c .o. $. $d 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 ) $.
$( Lemma for mendpadm. Multiplication by ` y ` from the right is
surjective. $)
mendpadmlem3 $p |- ( ph -> A. z e. B A. y e. B E. x e. B ( x .o. y ) = z
) $=
( va vb vc co wceq wral oveq1 eqeq1d oveq2d cv wcel wrex wi wal weq
oveq12d
wa oveq2 id eqeq12d cbvral3vw sylib ad2antrr cmgm simplr mgmcl simpr
rspc3v
syl3anc mpd biimpd rspcev syl6an ex alrimiv df-ral imbi2i albii sylbbr
syl
)
ADUAZEUBZCUAZEUBZBUAZVNGOZVLPZBEUCZUDZCUEZUDZDUEZVSCEQZDEQZAWBDAVMWAAVMUH
ZVTCWFVOVSWFVOUHZVLVLGOZVNVLGOZGOZWHVLWIGOZGOZGOZVLPZVSWGLUAZMUAZGOZWONUAZW
PGOZGOZGOZWRPZNEQMEQLEQZWNAXCVMVOAVQVPVLVNGOZGOZGOZVLPZDEQCEQBEQXCKXGXBWOVN
GOZWOXDGOZGOZVLPWQWOVLWPGOZGOZGOZVLPBCDLMNEEEBLUFZXFXJVLXNVQXHXEXIGVPWOVNGR
VPWOXDGRUGSCMUFZXJXMVLXOXHWQXIXLGVNWPWOGUIXOXDXKWOGVNWPVLGUITUGSDNUFZXMXAVL
WRXPXLWTWQGXPXKWSWOGVLWRWPGRTTXPUJUKULUMUNZWGWHEUBZWIEUBZVMXCWNUDWGFUOUBZVM
VMXRAXTVMVOJUNZAVMVOUPZYBEFVLVLGHIUQUTZWGXTVOVMXSYAWFVOURZYBEFVNVLGHIUQUTZY
BXBWNWHWPGOZWHWSGOZGOZWRPWJWHWRWIGOZGOZGOZWRPLMNWHWIVLEEEWOWHPZXAYHWRYLWQYF
WTYGGWOWHWPGRWOWHWSGRUGSWPWIPZYHYKWRYMYFWJYGYJGWPWIWHGUIYMWSYIWHGWPWIWRGUIT
UGSNDUFZYKWMWRVLYNYJWLWJGYNYIWKWHGWRVLWIGRTTYNUJUKUSUTVAWGWJEUBZWNWJVNGOZVL
PZVSWGXTXRXSYOYAYCYEEFWHWIGHIUQUTWGWNYQWGWMYPVLWGWLVNWJGWGXCWLVNPZXQWGVMVMV
OXCYRUDYBYBYDXBYRXKVLWSGOZGOZWRPWHVLWRVLGOZGOZGOZWRPLMNVLVLVNEEELDUFZXAYTWR
UUDWQXKWTYSGWOVLWPGRWOVLWSGRUGSMDUFZYTUUCWRUUEXKWHYSUUBGWPVLVLGUIUUEWSUUAVL
GWPVLWRGUITUGSNCUFZUUCWLWRVNUUFUUBWKWHGUUFUUAWIVLGWRVNVLGRTTUUFUJUKUSUTVATS
VBVRYQBWJEVPWJPVQYPVLVPWJVNGRSVCVDVAVEVFVEVFWEVMWDUDZDUEWCWDDEVGUUGWBDWDWAV
MVSCEVGVHVIVJVK $.
$}
Il giorno sabato 7 dicembre 2024 alle 20:25:11 UTC+1 Gino Giotto ha scritto:
> 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/78428663-d586-4217-853f-8fed20886f2bn%40googlegroups.com.
