Open
Description
This issue spawns from #4632 (comment)
Essentially, in multivariable polynomials, the polynomial ({x, y} -> exponent 1) -> coefficient 1 could represent either the polynomial xy or yx, meaning that to evaluate uniquely a multivariable polynomial, we need commutativity. But we don't need it for polynomials in one variable.
I tried to generalize evls1rhm by rewriting all lemmas used in evlsrhm, however evlslem1 uses asclrhm uses ascldimul uses asclmul1 uses assaass, meaning this route would need to show asclrhm for all the properties that df-assa brings (including the associativity) except the scalars can just form a ring instead of CRing.
So this is nontrivial.
Progress I made until running into this long chain
diff --git a/changes-set.txt b/changes-set.txt
index 0db9d466..c694fc95 100644
--- a/changes-set.txt
+++ b/changes-set.txt
@@ -85,6 +85,7 @@ make a github issue.)
DONE:
Date Old New Notes
+14-Feb-25 psrbagev1 [same] ` T e. CMnd ` changed to ` T e. Mnd `
10-Feb-25 --- --- Moved surreal addition theorems
from SF's mathbox to main set.mm
10-Feb-25 onunel --- Moved from SF's mathbox to main set.mm
diff --git a/set.mm b/set.mm
index ba037c9a..c4409e79 100644
--- a/set.mm
+++ b/set.mm
@@ -274405,6 +274405,18 @@ $)
ascldimul.k $e |- K = ( Base ` F ) $.
ascldimul.t $e |- .X. = ( .r ` W ) $.
ascldimul.s $e |- .x. = ( .r ` F ) $.
+ ${
+ ascldimulg.1 $e |- ( ph -> W e. LMod ) $.
+ ascldimulg.2 $e |- ( ph -> W e. Ring ) $.
+ ascldimulg.3 $e |- ( ph -> R e. K ) $.
+ ascldimulg.4 $e |- ( ph -> S e. K ) $.
+ $( The algebra scalars function distributes over multiplication.
+ (Contributed by SN, 15-Feb-2025.) $)
+ ascldimulg $p |-
+ ( ph -> ( A ` ( R .x. S ) ) = ( ( A ` R ) .X. ( A ` S ) ) ) $=
+ ? $.
+ $}
+
$( The algebra scalars function distributes over multiplication.
(Contributed by Mario Carneiro, 8-Mar-2015.) (Proof shortened by SN,
5-Nov-2023.) $)
@@ -278419,15 +278431,43 @@ $)
psrbagev1.c $e |- C = ( Base ` T ) $.
psrbagev1.x $e |- .x. = ( .g ` T ) $.
psrbagev1.z $e |- .0. = ( 0g ` T ) $.
- psrbagev1.t $e |- ( ph -> T e. CMnd ) $.
+ psrbagev1.t $e |- ( ph -> T e. Mnd ) $.
psrbagev1.b $e |- ( ph -> B e. D ) $.
psrbagev1.g $e |- ( ph -> G : I --> C ) $.
$( A bag of multipliers provides the conditions for a valid sum.
(Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV,
18-Jul-2019.) (Revised by AV, 11-Apr-2024.) Remove a sethood
- hypothesis. (Revised by SN, 7-Aug-2024.) $)
+ hypothesis. (Revised by SN, 7-Aug-2024.) Generalize ` T e. CMnd ` to
+ ` T e. Mnd ` . (Revised by SN, 14-Feb-2025.) $)
psrbagev1 $p |- ( ph -> ( ( B oF .x. G ) : I --> C
/\ ( B oF .x. G ) finSupp .0. ) ) $=
+ ( cvv wcel cc0 vy vz cof co wf cfsupp wbr cn0 cv wa mulgnn0cl 3expb sylan
+ cmnd psrbagf syl ffnd fndmexd inidm off csupp cfn wss ovexd offun c0g a1i
+ wfun fvexi psrbagfsupp fsuppimpd ssidd wceq mulg0 suppssof1 suppssfifsupp
+ adantl c0ex syl32anc jca ) AICBHFUCZUDZUEWBJUFUGZAUAUBIIIFUHCCBHRRAEUNSZU
+ AUIZUHSZUBUIZCSZUJWEWGFUDCSZOWDWFWHWICFEWEWGLMUKULUMABDSZIUHBUEPDGBIKUOUP
+ ZQAIBDPAIUHBWKUQZURZWMIUSUTAWBRSWBVHJRSZBTVAUDZVBSWBJVAUDWOVCWCABHWAVDAII
+ FBHRRWLAICHQUQWMWMVEWNAJEVFNVIVGABTAWJBTUFUGPDGBIKVJUPVKAUBBHICRWOFUHRTJA
+ WOVLWHTWGFUDJVMACFEWGJLNMVNVQWKQWMTRSAVRVGVOWOWBRRJVPVSVT $.
+ $}
+
+ ${
+ $d ph y z $. $d B h $. $d B y z $. $d C y z $. $d G z $. $d I h $.
+ $d .x. y z $. $d .0. z $.
+ psrbagev1OLD.d $e |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } $.
+ psrbagev1OLD.c $e |- C = ( Base ` T ) $.
+ psrbagev1OLD.x $e |- .x. = ( .g ` T ) $.
+ psrbagev1OLD.z $e |- .0. = ( 0g ` T ) $.
+ psrbagev1OLD.t $e |- ( ph -> T e. CMnd ) $.
+ psrbagev1OLD.b $e |- ( ph -> B e. D ) $.
+ psrbagev1OLD.g $e |- ( ph -> G : I --> C ) $.
+ $( Obsolete version of ~ psrbagev1 as of 14-Feb-2025. (Contributed by
+ Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) (Revised by
+ AV, 11-Apr-2024.) Remove a sethood hypothesis. (Revised by SN,
+ 7-Aug-2024.) (Proof modification is discouraged.)
+ (New usage is discouraged.) $)
+ psrbagev1OLD $p |- ( ph -> ( ( B oF .x. G ) : I --> C
+ /\ ( B oF .x. G ) finSupp .0. ) ) $=
( cvv wcel cc0 vy vz cof co wf cfsupp wbr cmnd cv cmnmndd mulgnn0cl 3expb
cn0 wa sylan psrbagf syl ffnd fndmexd inidm off csupp cfn wss ovexd offun
wfun c0g fvexi a1i psrbagfsupp fsuppimpd ssidd wceq adantl c0ex suppssof1
@@ -278442,7 +278482,7 @@ $)
Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) (Revised by
AV, 11-Apr-2024.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
- psrbagev1OLD $p |- ( ph -> ( ( B oF .x. G ) : I --> C
+ psrbagev1OLDOLD $p |- ( ph -> ( ( B oF .x. G ) : I --> C
/\ ( B oF .x. G ) finSupp .0. ) ) $=
( wcel vy vz cof co wf cfsupp wbr cn0 cv wa cmnmndd mulgnn0cl 3expb sylan
cmnd psrbagfOLD syl2anc inidm off cvv wfun cc0 csupp cfn ovexd ffnd offun
@@ -278468,9 +278508,9 @@ $)
AV, 11-Apr-2024.) Remove a sethood hypothesis. (Revised by SN,
7-Aug-2024.) $)
psrbagev2 $p |- ( ph -> ( T gsum ( B oF .x. G ) ) e. C ) $=
- ( cof co cvv c0g cfv eqid ovexd wf cfsupp psrbagev1 simpld fndmexd simprd
- wbr ffnd gsumcl ) AICBHFPZQZERESTZKUNUAZMAIUMRABHULUBAICUMAICUMUCZUMUNUDU
- IZABCDEFGHIUNJKLUOMNOUEZUFZUJUGUSAUPUQURUHUK $.
+ ( cof co cvv c0g cfv ovexd wf cfsupp wbr cmnmndd psrbagev1 simpld fndmexd
+ eqid ffnd simprd gsumcl ) AICBHFPZQZERESTZKUOUIZMAIUNRABHUMUAAICUNAICUNUB
+ ZUNUOUCUDZABCDEFGHIUOJKLUPAEMUENOUFZUGZUJUHUTAUQURUSUKUL $.
psrbagev2OLD.i $e |- ( ph -> I e. W ) $.
$( Obsolete version of ~ psrbagev2 as of 7-Aug-2024. (Contributed by
@@ -278478,9 +278518,9 @@ $)
(Revised by AV, 11-Apr-2024.) (New usage is discouraged.)
(Proof modification is discouraged.) $)
psrbagev2OLD $p |- ( ph -> ( T gsum ( B oF .x. G ) ) e. C ) $=
- ( cof co c0g cfv eqid wf cfsupp wbr psrbagev1OLD simpld simprd gsumcl ) A
- ICBHFRSZEJETUAZLUKUBZNQAICUJUCZUJUKUDUEZABCDEFGHIJUKKLMULNOPQUFZUGAUMUNUO
- UHUI $.
+ ( cof co c0g cfv eqid wf cfsupp wbr psrbagev1OLDOLD simpld simprd gsumcl
+ ) AICBHFRSZEJETUAZLUKUBZNQAICUJUCZUJUKUDUEZABCDEFGHIJUKKLMULNOPQUFZUGAUMU
+ NUOUHUI $.
$}
${
@@ -278664,22 +278704,21 @@ $)
( T gsum ( b oF .^ G ) ) ) ) : D --> C /\ ( b e. D |->
( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) )
finSupp ( 0g ` S ) ) ) $=
- ( vx cv cfv cof co cgsu cmpt wf c0g cfsupp wbr wcel wa crg crngring syl
- ccrg adantr cbs eqid rhmf mplelf ffvelcdmda ffvelcdmd mgpbas ccmn simpr
- crh crngmgp psrbagev2 ringcl syl3anc fmpttd cvv wfun csupp cfn wss ccnv
- cn cima cn0 cmap ovexd rabexd mptexd funmpt a1i mplelsfi fsuppimpd wceq
- fvexd feqmptd oveq1d eqimss2 cghm rhmghm 3syl suppssfv ringlz suppssov1
- ghmid sylan suppssfifsupp syl32anc jca ) ADCTDTUQZRURZMURZHYBNLUSUTVAUT
- ZIUTZVBZVCYGGVDURZVEVFZATDYFCAYBDVGZVHZGVIVGZYDCVGYECVGYFCVGAYLYJAGVLVG
- ZYLULGVJVKZVMYKFVNURZCYCMAYOCMVCZYJAMFGWCUTVGZYPUMYOCFGMYOVOZUCVPVKVMAD
- YOYBRABDEFJOYORUAYRUBUDUOVQZVRVSYKYBCDHLJNOUDCGHUEUCVTUFAHWAVGZYJAYMYTU
- LGHUEWDVKVMAYJWBAOCNVCYJUNVMWEZCGIYDYEUCUGWFWGWHAYGWIVGYGWJZYHWIVGRFVDU
- RZWKUTZWLVGYGYHWKUTUUDWMYIATDYFWIAJUQWNWOWPWLVGJWQOWRUTDWIUDAWQOWRWSWTX
- AUUBATDYFXBXCAGVDXGZARUUCABEFROVLUUCUAUBUUCVOZUOUKXDXEATUPYDYEDCUUDIWIW
- IYHYHATYCDWIMUUDWIUUCYHAUUDTDYCVBZUUCWKUTZXFUUHUUDWMARUUGUUCWKATDYORYSX
- HXIUUHUUDXJVKAYQMFGXKUTVGUUCMURYHXFUMFGMXLFGMUUCYHUUFYHVOZXQXMYKYBRXGAF
- VDXGXNAYLUPUQZCVGYHUUJIUTYHXFYNCGIUUJYHUCUGUUIXOXRYKYCMXGUUAUUEXPUUDYGW
- IWIYHXSXTYA $.
+ ( vx cv cfv cof co cgsu cmpt wf c0g cfsupp wbr wcel wa crngringd adantr
+ crg cbs crh eqid rhmf syl mplelf ffvelcdmda ffvelcdmd ccmn ccrg crngmgp
+ mgpbas simpr psrbagev2 ringcld fmpttd cvv wfun cfn wss ccnv cn cima cn0
+ csupp cmap ovexd rabexd mptexd funmpt a1i fvexd mplelsfi fsuppimpd wceq
+ feqmptd oveq1d eqimss2 cghm rhmghm ghmid 3syl suppssfv ringlz suppssov1
+ sylan suppssfifsupp syl32anc jca ) ADCTDTUQZRURZMURZHYANLUSUTVAUTZIUTZV
+ BZVCYFGVDURZVEVFZATDYECAYADVGZVHZCGIYCYDUCUGAGVKVGZYIAGULVIZVJYJFVLURZC
+ YBMAYMCMVCZYIAMFGVMUTVGZYNUMYMCFGMYMVNZUCVOVPVJADYMYARABDEFJOYMRUAYPUBU
+ DUOVQZVRZVSYJYACDHLJNOUDCGHUEUCWCUFAHVTVGZYIAGWAVGYSULGHUEWBVPVJAYIWDAO
+ CNVCYIUNVJWEZWFWGAYFWHVGYFWIZYGWHVGRFVDURZWPUTZWJVGYFYGWPUTUUCWKYHATDYE
+ WHAJUQWLWMWNWJVGJWOOWQUTDWHUDAWOOWQWRWSWTUUAATDYEXAXBAGVDXCZARUUBABEFRO
+ WAUUBUAUBUUBVNZUOUKXDXEATUPYCYDDCUUCIWHWHYGYGATYBDWHMUUCYMUUBYGAUUCTDYB
+ VBZUUBWPUTZXFUUGUUCWKARUUFUUBWPATDYMRYQXGXHUUGUUCXIVPAYOMFGXJUTVGUUBMUR
+ YGXFUMFGMXKFGMUUBYGUUEYGVNZXLXMYRAFVDXCXNAYKUPUQZCVGYGUUIIUTYGXFYLCGIUU
+ IYGUCUGUUHXOXQYJYBMXCYTUUDXPUUCYFWHWHYGXRXSXT $.
$}
$d x A $. $d b p v w x y z B $. $d b p x y z C $. $d b p v w x y z ph $.
@@ -278774,38 +278813,38 @@ $)
WKWKXURXUMXUDXUGMYFXUMXUEXUGMYFXUBUTPPXUDXUGMPWWTORRXUSAOPYAWXDAPDOUNXTZW
DZXURXURXVAXVBXUMXUGYGZYQXUBUTPPXUEXUGMPWXBORRXUTXVEXURXURXVAXVCXVFYQWNYO
XAXUBPDJWXQIWYARVUEVWKVWLXUAAVWNWXDVWOWDZXURXUBPDWXQWHZWXQVUEXMXNZXUBWWTD
- EIMKOPVUEUDVWKUFVWLXVGXUNXUQUXAZXPXUBPDWYAWHZWYAVUEXMXNZXUBWXBDEIMKOPVUEU
- DVWKUFVWLXVGAWXAWXCYBZXUQUXAZXPXUBXVHXVIXVJXQXUBXVKXVLXVNXQUWEWTYRYNWXFVW
- NWXPDVCWXTDVCWXRDVCZWYBDVCZWYJWYDVEAVWNWXEVWOWDWXFVVBDWXGNAVWRWXEVWSWDZWY
- QYDWXFVVBDWXHNXVQWYSYDAWXDXVOVYQXUBWWTDEIMKOPUDVWKUFXVGXUNXUQYEYRAWXDXVPV
- YQXUBWXBDEIMKOPUDVWKUFXVGXVMXUQYEYRDJIWYBWXPWXTWXRVWKXUAUXBUXDWTWXFUTWXLC
- DEFGHIJKLMNOWXJPVVBQRVVGSTUAUBUCVVNUDUEUFUGUHUIAVUHWXEUJWDZAVVQWXEUKWDZAV
- VRWXEULWDZAVVSWXEUMWDZAVVTWXEUNWDZVVMWXDWXLEVCAVYQEKWWTWXBPUDUXCYMWXFVUIW
- YMWYNWXJVVBVCAVUIWXEVUJWDWYQWYSVVBGWXIWXGWXHVVNWYTUXEYKWJWXFWYFWXSWYGWYCJ
- WXFUTWWTCDEFGHIJKLMNOWXGPVVBQRVVGSTUAUBUCVVNUDUEUFUGUHUIXVRXVSXVTXWAXWBVV
- MWYPWYQWJWXFUTWXBCDEFGHIJKLMNOWXHPVVBQRVVGSTUAUBUCVVNUDUEUFUGUHUIXVRXVSXV
- TXWAXWBVVMWYRWYSWJYNYOUXFUCVXLVXMVYNWWSUXGAUPVVBUYSNALCYAZBVVBYAZBUXHCUXO
- UYSVVBYAXWCASCVYBLHVYAWCXLUIUXIWLZAVVBCBAVXEVVBCBWHVXIVVBCGFBVVNUBXCWIZXT
- ZAVVBCBXWFUXJCVVBLBUXKYKAVVBDNVWSXTVVDVUQUYSVGZVUSVUTAXWDVVCXWHVUSVEXWGVV
- BLBVUQUXLUXMVWTWTUXNAUPPUYTOAXWCQPYAZQUXHCUXOUYTPYAXWEAPCQACFGPQRUAUHUBUJ
- VUJUXPZXTZAPCQXWJUXJCPLQUXKYKXVDVWHVUQUYTVGZVUQQVGZLVGZVWEAXWIVWGXWLXWNVE
- XWKPLQVUQUXLUXMVWHXWNUQEVVEUSPWWTVUQVEZYSVQVTZWAZVEVUMVVGVTWAZLVGVUPIXWQO
- VVIVBZWCVBZJVBZVWEVWHXWMXWRLVWHUSEGVUMUQKPQRVUQWFVVGUHUDVVMVXBAVUHVWGUJWD
- ZAVVQVWGUKWDZAVWGWGZUXQWEVWHUQXWQCDEFGHIJKLMNOVUMPVVBQRVVGSTUAUBUCVVNUDUE
- UFUGUHUIXXBXXCAVVRVWGULWDAVVSVWGUMWDAVVTVWGUNWDVVMAXWQEVCZVWGAVUHXXEUJUSE
- KPVUQRUDUXRWIWDAVXAVWGVXCWDWJVWHXXAVUEVWEJVBZVWEVWHVUPVUEXWTVWEJAVXJVWGVX
- KWDVWHXWTIUSPXWOWWTOVGZVUEVTZWAZWCVBVUQXXIVGZVWEVWHXWSXXIIWCAXWSXXIVEVWGA
- XWSUSPXWPXXGMVBZWAXXIAUSPXWPXXGMXWQORXJDUJXWPXJVCAWWTPVCZVPZXWOYSVQXJUXSU
- YGUXTWLAPDWWTOUNWOZAXWQYGAUSPDOUNWMWNAUSPXXKXXHXWOYSXXGMVBZXXHVEVQXXGMVBZ
- XXHVEXXKXXHVEXXMYSVQYSXWPVEXXOXXKXXHYSXWPXXGMUYAUYBVQXWPVEXXPXXKXXHVQXWPX
- XGMUYAUYBXXMXWOVPZXXOXXGXXHXXQXXGDVCZXXOXXGVEXXMXXRXWOXXNWDDMIXXGVWKUFUYC
- WIXWOXXHXXGVEXXMXWOXXGVUEUYDZYTYHXXMXWOUYEZVPXXPVUEXXHXXMXXPVUEVEZXXTXXMX
- XRXYAXXNDMIXXGVUEVWKVWLUFWSWIWDXXTXXHVUEVEZXXMXWOXXGVUEUYFZYTYHUYHWQWTWDX
- AVWHPDXXIIRVUQVUEVWKVWLAVWMVWGVWPWDXXBXXDVWHUSPXXHDVWHXXLVPXWOXXGVUEDAXXL
- XXRVWGXXNUYIAVUEDVCZVWGXXLAVWQXYDVULDHVUEUCVUGXFWIYCUYQUYJVWHPXXHUSRVUQVR
- ZVUEWWTPXYEUYKVCZXYBVWHXYFXXTXYBWWTPVUQUYLXYCWIYTXXBUYMUYNVWGXXJVWEVEAUSV
- UQXXHVWEPXXIXWOXXHXXGVWEXXSWWTVUQOVOWTXXIVLVUQOUYOYLYTXEYNAVWQVWGVWIXXFVW
- EVEVULVWJDHJVUEVWEUCUGVUGUYPXDWTXEWTUXNUYR $.
+ EIMKOPVUEUDVWKUFVWLAVWMWXDVWPWDZXUNXUQUXAZXPXUBPDWYAWHZWYAVUEXMXNZXUBWXBD
+ EIMKOPVUEUDVWKUFVWLXVJAWXAWXCYBZXUQUXAZXPXUBXVHXVIXVKXQXUBXVLXVMXVOXQUWEW
+ TYRYNWXFVWNWXPDVCWXTDVCWXRDVCZWYBDVCZWYJWYDVEAVWNWXEVWOWDWXFVVBDWXGNAVWRW
+ XEVWSWDZWYQYDWXFVVBDWXHNXVRWYSYDAWXDXVPVYQXUBWWTDEIMKOPUDVWKUFXVGXUNXUQYE
+ YRAWXDXVQVYQXUBWXBDEIMKOPUDVWKUFXVGXVNXUQYEYRDJIWYBWXPWXTWXRVWKXUAUXBUXDW
+ TWXFUTWXLCDEFGHIJKLMNOWXJPVVBQRVVGSTUAUBUCVVNUDUEUFUGUHUIAVUHWXEUJWDZAVVQ
+ WXEUKWDZAVVRWXEULWDZAVVSWXEUMWDZAVVTWXEUNWDZVVMWXDWXLEVCAVYQEKWWTWXBPUDUX
+ CYMWXFVUIWYMWYNWXJVVBVCAVUIWXEVUJWDWYQWYSVVBGWXIWXGWXHVVNWYTUXEYKWJWXFWYF
+ WXSWYGWYCJWXFUTWWTCDEFGHIJKLMNOWXGPVVBQRVVGSTUAUBUCVVNUDUEUFUGUHUIXVSXVTX
+ WAXWBXWCVVMWYPWYQWJWXFUTWXBCDEFGHIJKLMNOWXHPVVBQRVVGSTUAUBUCVVNUDUEUFUGUH
+ UIXVSXVTXWAXWBXWCVVMWYRWYSWJYNYOUXFUCVXLVXMVYNWWSUXGAUPVVBUYSNALCYAZBVVBY
+ AZBUXHCUXOUYSVVBYAXWDASCVYBLHVYAWCXLUIUXIWLZAVVBCBAVXEVVBCBWHVXIVVBCGFBVV
+ NUBXCWIZXTZAVVBCBXWGUXJCVVBLBUXKYKAVVBDNVWSXTVVDVUQUYSVGZVUSVUTAXWEVVCXWI
+ VUSVEXWHVVBLBVUQUXLUXMVWTWTUXNAUPPUYTOAXWDQPYAZQUXHCUXOUYTPYAXWFAPCQACFGP
+ QRUAUHUBUJVUJUXPZXTZAPCQXWKUXJCPLQUXKYKXVDVWHVUQUYTVGZVUQQVGZLVGZVWEAXWJV
+ WGXWMXWOVEXWLPLQVUQUXLUXMVWHXWOUQEVVEUSPWWTVUQVEZYSVQVTZWAZVEVUMVVGVTWAZL
+ VGVUPIXWROVVIVBZWCVBZJVBZVWEVWHXWNXWSLVWHUSEGVUMUQKPQRVUQWFVVGUHUDVVMVXBA
+ VUHVWGUJWDZAVVQVWGUKWDZAVWGWGZUXQWEVWHUQXWRCDEFGHIJKLMNOVUMPVVBQRVVGSTUAU
+ BUCVVNUDUEUFUGUHUIXXCXXDAVVRVWGULWDAVVSVWGUMWDAVVTVWGUNWDVVMAXWREVCZVWGAV
+ UHXXFUJUSEKPVUQRUDUXRWIWDAVXAVWGVXCWDWJVWHXXBVUEVWEJVBZVWEVWHVUPVUEXXAVWE
+ JAVXJVWGVXKWDVWHXXAIUSPXWPWWTOVGZVUEVTZWAZWCVBVUQXXJVGZVWEVWHXWTXXJIWCAXW
+ TXXJVEVWGAXWTUSPXWQXXHMVBZWAXXJAUSPXWQXXHMXWRORXJDUJXWQXJVCAWWTPVCZVPZXWP
+ YSVQXJUXSUYGUXTWLAPDWWTOUNWOZAXWRYGAUSPDOUNWMWNAUSPXXLXXIXWPYSXXHMVBZXXIV
+ EVQXXHMVBZXXIVEXXLXXIVEXXNYSVQYSXWQVEXXPXXLXXIYSXWQXXHMUYAUYBVQXWQVEXXQXX
+ LXXIVQXWQXXHMUYAUYBXXNXWPVPZXXPXXHXXIXXRXXHDVCZXXPXXHVEXXNXXSXWPXXOWDDMIX
+ XHVWKUFUYCWIXWPXXIXXHVEXXNXWPXXHVUEUYDZYTYHXXNXWPUYEZVPXXQVUEXXIXXNXXQVUE
+ VEZXYAXXNXXSXYBXXODMIXXHVUEVWKVWLUFWSWIWDXYAXXIVUEVEZXXNXWPXXHVUEUYFZYTYH
+ UYHWQWTWDXAVWHPDXXJIRVUQVUEVWKVWLAVWMVWGVWPWDXXCXXEVWHUSPXXIDVWHXXMVPXWPX
+ XHVUEDAXXMXXSVWGXXOUYIAVUEDVCZVWGXXMAVWQXYEVULDHVUEUCVUGXFWIYCUYQUYJVWHPX
+ XIUSRVUQVRZVUEWWTPXYFUYKVCZXYCVWHXYGXYAXYCWWTPVUQUYLXYDWIYTXXCUYMUYNVWGXX
+ KVWEVEAUSVUQXXIVWEPXXJXWPXXIXXHVWEXXTWWTVUQOVOWTXXJVLVUQOUYOYLYTXEYNAVWQV
+ WGVWIXXGVWEVEVULVWJDHJVUEVWEUCUGVUGUYPXDWTXEWTUXNUYR $.
$}
${
@@ -282266,6 +282305,175 @@ $)
VNVO $.
$}
+ ${
+ $d ph i j k y $. $d B i j k x y z $. $d D i j k x y z $. $d E i j z $.
+ $d .x. i j $. $d P i j k x y z $. $d R h i j k $. $d S i j $.
+ $d W i j k $. $d .0. h i j k x y $. $d .0. z $.
+ evls1lem2.p $e |- P = ( 1o mPoly R ) $.
+ evls1lem2.b $e |- B = ( Base ` P ) $.
+ evls1lem2.m $e |- .x. = ( .r ` S ) $.
+ evls1lem2.z $e |- .0. = ( 0g ` R ) $.
+ evls1lem2.d $e |- D = { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } $.
+ evls1lem2.r $e |- ( ph -> R e. Ring ) $.
+ evls1lem2.s $e |- ( ph -> S e. Ring ) $.
+ evls1lem2.e1 $e |- ( ph -> E e. ( P GrpHom S ) ) $.
+ evls1lem2.e2 $e |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( j e. D /\
+ i e. D ) ) ) -> ( E ` ( k e. D |-> if ( k = ( j oF + i ) , ( ( x ` j )
+ ( .r ` R ) ( y ` i ) ) , .0. ) ) ) = ( ( E ` ( k e. D |-> if ( k = j ,
+ ( x ` j ) , .0. ) ) ) .x. ( E ` ( k e. D |->
+ if ( k = i , ( y ` i ) , .0. ) ) ) ) ) $.
+ $( A linear function on the polynomial ring which is multiplicative on
+ scaled monomials is generally multiplicative. Based on ~ evlslem2 .
+ (Contributed by SN, 15-Feb-2025.) $)
+ evls1lem2 $p |- ( ( ph /\ ( x e. B /\ y e. B ) ) ->
+ ( E ` ( x ( .r ` P ) y ) ) = ( ( E ` x ) .x. ( E ` y ) ) ) $=
+ ? $.
+ $}
+
+ ${
+ $d b p x .0. $. $d p B $. $d b y C $. $d b p x y D $. $d b p F $.
+ $d b p y .^ $. $d b h p x A $. $d x K $. $d x R $. $d b x y ph $.
+ $d b p y G $. $d b p x H $. $d b p S $. $d b p y T $. $d b p .x. $.
+ evls1lem3.p $e |- P = ( 1o mPoly R ) $.
+ evls1lem3.b $e |- B = ( Base ` P ) $.
+ evls1lem3.c $e |- C = ( Base ` S ) $.
+ evls1lem3.k $e |- K = ( Base ` R ) $.
+ evls1lem3.d $e |- D = { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } $.
+ evls1lem3.t $e |- T = ( mulGrp ` S ) $.
+ evls1lem3.x $e |- .^ = ( .g ` T ) $.
+ evls1lem3.m $e |- .x. = ( .r ` S ) $.
+ evls1lem3.v $e |- V = ( 1o mVar R ) $.
+ evls1lem3.e $e |- E = ( p e. B |-> ( S gsum ( b e. D |->
+ ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) $.
+ evls1lem3.r $e |- ( ph -> R e. Ring ) $.
+ evls1lem3.s $e |- ( ph -> S e. Ring ) $.
+ evls1lem3.f $e |- ( ph -> F e. ( R RingHom S ) ) $.
+ evls1lem3.g $e |- ( ph -> G : 1o --> C ) $.
+ evls1lem3.z $e |- .0. = ( 0g ` R ) $.
+ evls1lem3.a $e |- ( ph -> A e. D ) $.
+ evls1lem3.q $e |- ( ph -> H e. K ) $.
+ $( Lemma for ~ evls1eu . Polynomial evaluation of a scaled monomial.
+ Based on ~ evlslem3 . (Contributed by SN, 14-Feb-2025.) $)
+ evls1lem3 $p |- ( ph -> ( E ` ( x e. D |-> if ( x = A , H , .0. ) ) ) =
+ ( ( F ` H ) .x. ( T gsum ( A oF .^ G ) ) ) ) $=
+ ( vy cv wceq cif cmpt cfv cof cgsu wcel c1o cvv 1oex a1i mplmon2cl fveq2d
+ co fveq1 oveq1d mpteq2dv oveq2d ovex fvmpt syl eqid eqeq1 ifbid simpr c0g
+ wa fvexi ifexd adantr fvmptd3 mpteq2dva crg cmnd ringmnd ccnv cn cima cfn
+ cn0 cmap rabex2 crh wf rhmf ring0cl ifcld ffvelcdmd c0 csn psrbagf adantl
+ wfn ffnd inidm eqidd offval df1o2 mpteq1d eqtrd mgpbas ringmgp mulgnn0cld
+ 0lt1o fveq2 oveq12d gsumsnd eqeltrd ringcld cdif eldifsnneq iffalsed cghm
+ fmpttd rhmghm ghmid 3syl eldifi sylan2 ringlz suppss2 gsumpt iftrue oveq1
+ syl2an2r 3eqtrd ) ABFBVAZCVBZQTVCZVDZMVEZIUBFUBVAZUUKVEZOVEZJUUMPNVFZVOZV
+ GVOZKVOZVDZVGVOZCUBFUUMCVBZQTVCZOVEZUURKVOZVDZVEZQOVEZJCPUUPVOZVGVOZKVOZA
+ UUKDVHUULUVAVBABDRFGHLVICVJQTUCUGUQUFVIVJVHZAVKVLUMUDUSURVMUAUUKIUBFUUMUA
+ VAZVEZOVEZUURKVOZVDZVGVOUVADMUVMUUKVBZUVQUUTIVGUVRUBFUVPUUSUVRUVOUUOUURKU
+ VRUVNUUNOUUMUVMUUKVPVNVQVRVSULIUUTVGVTWAWBAUVAIUVFVGVOUVGAUUTUVFIVGAUBFUU
+ SUVEAUUMFVHZWHZUUOUVDUURKUVTUUNUVCOUVTBUUMUUJUVCFUUKVJUUKWCUUHUUMVBUUIUVB
+ QTUUHUUMCWDWEAUVSWFAUVCVJVHUVSAUVBQTRVJUSTVJVHATHWGUQWIVLWJWKWLVNVQWMVSAF
+ EUVFIVJCIWGVEZUEUWAWCZAIWNVHZIWOVHUNIWPWBFVJVHALVAWQWRWSWTVHLXAVIXBVOFUGX
+ AVIXBVTXCVLZURAUBFUVEEUVTEIKUVDUURUEUJAUWCUVSUNWKAUVDEVHUVSAREUVCOAOHIXDV
+ OVHZREOXEUOREHIOUFUEXFWBAUVBQTRUSAHWNVHTRVHUMRHTUFUQXGWBXHXIWKUVTUURXJUUM
+ VEZXJPVEZNVOZEUVTUURJUTXJXKZUTVAZUUMVEZUWJPVEZNVOZVDZVGVOUWHUVTUUQUWNJVGU
+ VTUUQUTVIUWMVDUWNUVTUTVIVIUWKUWLNVIUUMPVJVJUVSUUMVIXNAUVSVIXAUUMFLUUMVIUG
+ XLZXOXMAPVIXNUVSAVIEPUPXOWKUVLUVTVKVLZUWPVIXPUVTUWJVIVHWHZUWKXQUWQUWLXQXR
+ UVTUTVIUWIUWMVIUWIVBUVTXSVLXTYAVSUVTUWMEUWHUTJXJVIEIJUHUEYBZAJWOVHZUVSAUW
+ CUWSUNIJUHYCWBWKZXJVIVHZUVTYEVLUVTENJUWFUWGUWRUIUWTUVSUWFXAVHAUVSVIXAXJUU
+ MUWOUXAUVSYEVLXIXMAUWGEVHUVSAVIEXJPUPUXAAYEVLXIWKYDZUWJXJVBZUWMUWHVBUVTUX
+ CUWKUWFUWLUWGNUWJXJUUMYFUWJXJPYFYGXMYHYAUXBYIZYJYOAFUVEUBVJCXKZUWAAUUMFUX
+ EYKVHZWHZUVEUWAUURKVOZUWAUXGUVDUWAUURKUXGUVDTOVEZUWAUXGUVCTOUXFUVCTVBAUXF
+ UVBQTUUMFCYLYMXMVNAUXIUWAVBZUXFAUWEOHIYNVOVHUXJUOHIOYPHIOTUWAUQUWBYQYRWKY
+ AVQAUWCUXFUUREVHZUXHUWAVBUNUXFAUVSUXKUUMFUXEYSUXDYTEIKUURUWAUEUJUWBUUAUUF
+ YAUWDUUBUUCYAACFVHUVGUVKVBURUBCUVEUVKFUVFUVBUVDUVHUURUVJKUVBUVCQOUVBQTUUD
+ VNUVBUUQUVIJVGUUMCPUUPUUEVSYGUVFWCUVHUVJKVTWAWBUUG $.
+ $}
+
+ ${
+ $d .x. x $. $d ph x $. $d B h $. $d B x $. $d G x $.
+ psr1bagev2.d $e |- D = { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } $.
+ psr1bagev2.c $e |- C = ( Base ` T ) $.
+ psr1bagev2.x $e |- .x. = ( .g ` T ) $.
+ psr1bagev2.t $e |- ( ph -> T e. Mnd ) $.
+ psr1bagev2.b $e |- ( ph -> B e. D ) $.
+ psr1bagev2.g $e |- ( ph -> G : 1o --> C ) $.
+ $( Closure of a sum using a bag of multipliers. Version of ~ psrbagev2
+ where ` T e. CMnd ` is generalized to ` T e. Mnd ` when ` I = 1o ` .
+ (Contributed by SN, 14-Feb-2025.) $)
+ psr1bagev2 $p |- ( ph -> ( T gsum ( B oF .x. G ) ) e. C ) $=
+ ( vx co c0 cfv c1o wcel cof cgsu csn cv cmpt cvv cn0 wf psrbagf ffnd 1oex
+ syl inidm wa eqidd offval wceq df1o2 mpteq1d eqtrd oveq2d 0lt1o ffvelcdmd
+ a1i mulgnn0cld fveq2 oveq12d adantl gsumsnd eqeltrd ) AEBHFUAPZUBPZQBRZQH
+ RZFPZCAVLEOQUCZOUDZBRZVQHRZFPZUEZUBPVOAVKWAEUBAVKOSVTUEWAAOSSVRVSFSBHUFUF
+ ASUGBABDTSUGBUHMDGBSIUIULZUJASCHNUJSUFTAUKVDZWCSUMAVQSTUNZVRUOWDVSUOUPAOS
+ VPVTSVPUQAURVDUSUTVAAVTCVOOEQSJLQSTAVBVDZACFEVMVNJKLASUGQBWBWEVCASCQHNWEV
+ CVEZVQQUQZVTVOUQAWGVRVMVSVNFVQQBVFVQQHVFVGVHVIUTWFVJ $.
+ $}
+
+ ${
+ evls1lem1.p $e |- P = ( 1o mPoly R ) $.
+ evls1lem1.b $e |- B = ( Base ` P ) $.
+ evls1lem1.c $e |- C = ( Base ` S ) $.
+ evls1lem1.d $e |- D = { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } $.
+ evls1lem1.t $e |- T = ( mulGrp ` S ) $.
+ evls1lem1.x $e |- .^ = ( .g ` T ) $.
+ evls1lem1.m $e |- .x. = ( .r ` S ) $.
+ evls1lem1.v $e |- V = ( 1o mVar R ) $.
+ evls1lem1.e $e |- E = ( p e. B |-> ( S gsum ( b e. D |->
+ ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) $.
+ evls1lem1.r $e |- ( ph -> R e. Ring ) $.
+ evls1lem1.s $e |- ( ph -> S e. Ring ) $.
+ evls1lem1.f $e |- ( ph -> F e. ( R RingHom S ) ) $.
+ evls1lem1.g $e |- ( ph -> G : 1o --> C ) $.
+
+ ${
+ $d ph b x $. $d C b x $. $d D b $. $d G x $. $d I h $. $d .x. x $.
+ $d R b $. $d S b x $. $d T x $. $d .^ x $. $d Y b $. $d b h $.
+ evls1lem6.y $e |- ( ph -> Y e. B ) $.
+ $( Lemma for ~ evls1eu . Finiteness and consistency of the top-level
+ sum. Based on ~ evlslem6 . (Contributed by SN, 14-Feb-2025.) $)
+ evls1lem6 $p |- ( ph -> ( ( b e. D |-> ( ( F ` ( Y ` b ) ) .x.
+ ( T gsum ( b oF .^ G ) ) ) ) : D --> C /\ ( b e. D |->
+ ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) )
+ finSupp ( 0g ` S ) ) ) $=
+ ( vx cv cfv cof co cgsu cmpt wf c0g cfsupp wbr wcel crg adantr cbs eqid
+ wa crh rhmf syl c1o mplelf ffvelcdmda ffvelcdmd cmnd ringmgp psr1bagev2
+ mgpbas simpr ringcld fmpttd cvv wfun csupp cfn wss ccnv cima cmap ovexd
+ cn cn0 rabexd mptexd funmpt a1i fvexd mplelsfi fsuppimpd feqmptd oveq1d
+ wceq eqimss2 cghm rhmghm ghmid 3syl suppssfv ringlz sylan suppssfifsupp
+ suppssov1 syl32anc jca ) ADCRDRUNZPUOZMUOZHXQNLUPUQURUQZIUQZUSZUTYBGVAU
+ OZVBVCZARDYACAXQDVDZVIZCGIXSXTUAUEAGVEVDZYEUIVFYFFVGUOZCXRMAYHCMUTZYEAM
+ FGVJUQVDZYIUJYHCFGMYHVHZUAVKVLVFADYHXQPABDEFJVMYHPSYKTUBULVNZVOZVPYFXQC
+ DHLJNUBCGHUCUAVTUDAHVQVDZYEAYGYNUIGHUCVRVLVFAYEWAAVMCNUTYEUKVFVSZWBWCAY
+ BWDVDYBWEZYCWDVDPFVAUOZWFUQZWGVDYBYCWFUQYRWHYDARDYAWDAJUNWIWMWJWGVDJWNV
+ MWKUQDWDUBAWNVMWKWLWOWPYPARDYAWQWRAGVAWSZAPYQABEFPVMVEYQSTYQVHZULUHWTXA
+ ARUMXSXTDCYRIWDWDYCYCARXRDWDMYRYHYQYCAYRRDXRUSZYQWFUQZXDUUBYRWHAPUUAYQW
+ FARDYHPYLXBXCUUBYRXEVLAYJMFGXFUQVDYQMUOYCXDUJFGMXGFGMYQYCYTYCVHZXHXIYMA
+ FVAWSXJAYGUMUNZCVDYCUUDIUQYCXDUICGIUUDYCUAUEUUCXKXLYFXRMWSYOYSXNYRYBWDW
+ DYCXMXOXP $.
+ $}
+
+ $d x A $. $d b p v w x y z B $. $d b p x y z C $. $d b p v w x y z ph $.
+ $d w x y z E $. $d b p x F $. $d b p x z T $. $d x V $.
+ $d b p v w x y z D $. $d b h p v w x y z R $. $d b p v x z G $.
+ $d b p v w x y z P $. $d b p w x y z S $. $d b p v w z .x. $.
+ $d b p v x z .^ $. $d v w x y z W $.
+ evls1lem1.a $e |- A = ( algSc ` P ) $.
+ $( Lemma for ~ evls1eu , give a formula for (the unique) polynomial
+ evaluation homomorphism. Based on ~ evlslem1 . (Contributed by SN,
+ 15-Feb-2025.) $)
+ evls1lem1 $p |- ( ph -> ( E e. ( P RingHom S ) /\
+ ( E o. A ) = F /\ ( E o. V ) = G ) ) $=
+ ( vx vy crh wcel ccom wceq cplusg cfv cmulr cur eqid c1o cvv crg 1oex a1i
+ co mplring syl2anc isrhmd cbs wfn crn wss cv cof cgsu cmpt fnmpti syl3anc
+ ovex fnco wf rhmf syl ffnd csca casa asclrhm mplsca oveq1d eleqtrrd fvco2
+ wa sylan eqtrd eqfnfvd 3jca ) ALFHUOVIUPLBUQZNURLPUQOURAUMUNCDFUSUTZHUSUT
+ ZFHFVAUTZJFVBUTZLHVBUTZTXEVCXFVCXDVCUEAVDVEUPZGVFUPFVFUPXGAVGVHZUHFGVDVES
+ VJVKUI??UAXBVCXCVC??VLAUMGVMUTZXANALCVNZBXIVNZBVOCVPXAXIVNXJAQCHRERVQZQVQ
+ UTNUTIXLOMVRVIVSVIJVIVTZVSVILHXMVSWCUGWAVH??CXILBWDWBAXIDNANGHUOVIUPXIDNW
+ EUJXIDGHNXIVCZUAWFWGWHAUMVQZXIUPZWPXOXAUTZXOBUTLUTZXONUTAXKXPXQXRURAXICBA
+ BGFUOVIZUPXICBWEABFWIUTZFUOVIZXSAFWJUPBYAUP?BXTFULXTVCWKWGAGXTFUOAFGVDVEV
+ FSXHUHWLWMWNXICGFBXNTWFWGWHXILBXOWOWQ?WRWS?WT $.
+ $}
+
${
$d B b r s x y $. $d E r s $. $d R b r s $. $d S b r s $.
evls1fval.q $e |- Q = ( S evalSub1 R ) $.
@@ -660189,6 +660397,11 @@ $)
6-Nov-2024.) $)
eqimssd $p |- ( ph -> A C_ B ) $=
( ssid eqsstrdi ) ABCCDCEF $.
+
+ $( Equality implies inclusion, deduction version. (Contributed by SN,
+ 15-Feb-2025.) $)
+ eqimss2d $p |- ( ph -> B C_ A ) $=
+ ( ssid eqsstrrdi ) ACBBDBEF $.
$}Metadata
Metadata
Assignees
Labels
No labels