I proved the eighth theorem without DV conditions on ph. The price to pay
is the addition of more dummy variables and making the proof a bit longer:
${
$d x y z a b c u v B $. $d x y z a b c u v .o. $. $d u v 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. The identity ` x .o. ( y .o. x ) = y ` holds. $)
mendpadmlem4 $p |- ( ph -> A. x e. B A. y e. B ( x .o. ( y .o. x ) ) = y
) $=
( vu vc co wceq wral wcel oveq1 oveq12d oveq2d vv va vb cv wi wal wa
eqeq1d
weq oveq2 eqeq12d cbvral3vw sylib ad2antrr cmgm simplr mgmcl syl3anc
rspc3v
id simpr mpd 3eqtr3d ex alrimiv df-ral imbi2i albii sylbbr syl
cbvral2vw )
ALUDZUAUDZVLGNZGNZVMOZUAEPZLEPZBUDZCUDZVSGNZGNZVTOZCEPBEPAVLEQZVMEQZVPUEZUA
UFZUEZLUFZVRAWHLAWDWGAWDUGZWFUAWJWEVPWJWEUGZVLVLGNZVOGNZWLVLVOGNZGNZGNZWMWP
GNZGNZWMVOVMWKUBUDZUCUDZGNZWSMUDZWTGNZGNZGNZXBOZMEPUCEPUBEPZWRWMOZAXGWDWEAV
SVTGNZVSDUDZVTGNZGNZGNZXJOZDEPCEPBEPZXGKXNXFWSVTGNZWSXKGNZGNZXJOXAWSXJWTGNZ
GNZGNZXJOBCDUBUCMEEEBUBUIZXMXRXJYBXIXPXLXQGVSWSVTGRVSWSXKGRSUHCUCUIZXRYAXJY
CXPXAXQXTGVTWTWSGUJYCXKXSWSGVTWTXJGUJTSUHDMUIZYAXEXJXBYDXTXDXAGYDXSXCWSGXJX
BWTGRTTYDUTUKULZUMUNZWKWMEQZWOEQZYGXGXHUEWKFUOQZWLEQZVOEQZYGAYIWDWEJUNZWKYI
WDWDYJYLAWDWEUPZYMEFVLVLGHIUQURZWKYIWDVNEQZYKYLYMWKYIWEWDYOYLWJWEVAZYMEFVMV
LGHIUQUREFVLVNGHIUQURZEFWLVOGHIUQURZWKYIYJWNEQZYHYLYNWKYIWDYKYSYLYMYQEFVLVO
GHIUQUREFWLWNGHIUQURYRXFXHWMWTGNZWMXCGNZGNZXBOWPWMXBWOGNZGNZGNZXBOUBUCMWMWO
WMEEEWSWMOZXEUUBXBUUFXAYTXDUUAGWSWMWTGRWSWMXCGRSUHWTWOOZUUBUUEXBUUGYTWPUUAU
UDGWTWOWMGUJUUGXCUUCWMGWTWOXBGUJTSUHXBWMOZUUEWRXBWMUUHUUDWQWPGUUHUUCWPWMGXB
WMWOGRTTUUHUTUKUSURVBWKWPVLWQVNGWKXGWPVLOZYFWKYJYKWDXGUUIUEYNYQYMXFUUIWLWTG
NZWLXCGNZGNZXBOWMWLXBVOGNZGNZGNZXBOUBUCMWLVOVLEEEWSWLOZXEUULXBUUPXAUUJXDUUK
GWSWLWTGRWSWLXCGRSUHWTVOOZUULUUOXBUUQUUJWMUUKUUNGWTVOWLGUJUUQXCUUMWLGWTVOXB
GUJTSUHMLUIZUUOWPXBVLUURUUNWOWMGUURUUMWNWLGXBVLVOGRTTUURUTUKUSURZVBWKWMVMWP
VLGWKXGWMVMOZYFWKWDWDWEXGUUTUEYMYMYPXFUUTVLWTGNZVLXCGNZGNZXBOWLVLXBVLGNZGNZ
GNZXBOUBUCMVLVLVMEEEUBLUIZXEUVCXBUVGXAUVAXDUVBGWSVLWTGRWSVLXCGRSUHUCLUIZUVC
UVFXBUVHUVAWLUVBUVEGWTVLVLGUJUVHXCUVDVLGWTVLXBGUJTSUHMUAUIZUVFWMXBVMUVIUVEV
OWLGUVIUVDVNVLGXBVMVLGRTTUVIUTUKUSURVBZWKXGUUIWKXOXGAXOWDWEKUNYEUMUUSVBSSUV
JVCVDVEVDVEVRWDVQUEZLUFWIVQLEVFUVKWHLVQWGWDVPUAEVFVGVHVIVJVPWCVSVMVSGNZGNZV
MOLUABCEELBUIZVOUVMVMUVNVLVSVNUVLGUVNUTVLVSVMGUJSUHUACUIZUVMWBVMVTUVOUVLWAV
SGVMVTVSGRTUVOUTUKVKUM $.
$}
Il giorno domenica 8 dicembre 2024 alle 11:06:18 UTC+1 Gino Giotto ha
scritto:
> 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/af50bf3e-09f0-4853-a20a-0927d7682fe2n%40googlegroups.com.
