![]() |
Metamath
Proof Explorer Theorem List (p. 216 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | psradd 21501 | The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ ) & β’ β = (+gβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β π) = (π βf + π)) | ||
Theorem | psraddcl 21502 | Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β Grp) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π + π) β π΅) | ||
Theorem | psrmulr 21503* | The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 2-Mar-2024.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} β β’ β = (π β π΅, π β π΅ β¦ (π β π· β¦ (π Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯))))))) | ||
Theorem | psrmulfval 21504* | The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (πΉ β πΊ) = (π β π· β¦ (π Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πΉβπ₯) Β· (πΊβ(π βf β π₯))))))) | ||
Theorem | psrmulval 21505* | The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β π β π·) β β’ (π β ((πΉ β πΊ)βπ) = (π Ξ£g (π β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πΉβπ) Β· (πΊβ(π βf β π)))))) | ||
Theorem | psrmulcllem 21506* | Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ (π β (π Β· π) β π΅) | ||
Theorem | psrmulcl 21507 | Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π Β· π) β π΅) | ||
Theorem | psrsca 21508 | The scalar field of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β π) β β’ (π β π = (Scalarβπ)) | ||
Theorem | psrvscafval 21509* | The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 2-Nov-2024.) |
β’ π = (πΌ mPwSer π ) & β’ β = ( Β·π βπ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} β β’ β = (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π)) | ||
Theorem | psrvsca 21510* | The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ β = ( Β·π βπ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β π β πΎ) & β’ (π β πΉ β π΅) β β’ (π β (π β πΉ) = ((π· Γ {π}) βf Β· πΉ)) | ||
Theorem | psrvscaval 21511* | The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ β = ( Β·π βπ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β π β πΎ) & β’ (π β πΉ β π΅) & β’ (π β π β π·) β β’ (π β ((π β πΉ)βπ) = (π Β· (πΉβπ))) | ||
Theorem | psrvscacl 21512 | Closure of the power series scalar multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β Ring) & β’ (π β π β πΎ) & β’ (π β πΉ β π΅) β β’ (π β (π Β· πΉ) β π΅) | ||
Theorem | psr0cl 21513* | The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Grp) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ π΅ = (Baseβπ) β β’ (π β (π· Γ { 0 }) β π΅) | ||
Theorem | psr0lid 21514* | The zero element of the ring of power series is a left identity. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Grp) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β π΅) β β’ (π β ((π· Γ { 0 }) + π) = π) | ||
Theorem | psrnegcl 21515* | The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Grp) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = (invgβπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π΅) β β’ (π β (π β π) β π΅) | ||
Theorem | psrlinv 21516* | The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Grp) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = (invgβπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π΅) & β’ 0 = (0gβπ ) & β’ + = (+gβπ) β β’ (π β ((π β π) + π) = (π· Γ { 0 })) | ||
Theorem | psrgrp 21517 | The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by SN, 7-Feb-2025.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Grp) β β’ (π β π β Grp) | ||
Theorem | psrgrpOLD 21518 | Obsolete proof of psrgrp 21517 as of 7-Feb-2025. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Grp) β β’ (π β π β Grp) | ||
Theorem | psr0 21519* | The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Grp) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = (0gβπ ) & β’ 0 = (0gβπ) β β’ (π β 0 = (π· Γ {π})) | ||
Theorem | psrneg 21520* | The negative function of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Grp) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = (invgβπ ) & β’ π΅ = (Baseβπ) & β’ π = (invgβπ) & β’ (π β π β π΅) β β’ (π β (πβπ) = (π β π)) | ||
Theorem | psrlmod 21521 | The ring of power series is a left module. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) β β’ (π β π β LMod) | ||
Theorem | psr1cl 21522* | The identity element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ π = (π₯ β π· β¦ if(π₯ = (πΌ Γ {0}), 1 , 0 )) & β’ π΅ = (Baseβπ) β β’ (π β π β π΅) | ||
Theorem | psrlidm 21523* | The identity element of the ring of power series is a left identity. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by AV, 8-Jul-2019.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ π = (π₯ β π· β¦ if(π₯ = (πΌ Γ {0}), 1 , 0 )) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β π β π΅) β β’ (π β (π Β· π) = π) | ||
Theorem | psrridm 21524* | The identity element of the ring of power series is a right identity. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by AV, 8-Jul-2019.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ π = (π₯ β π· β¦ if(π₯ = (πΌ Γ {0}), 1 , 0 )) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β π β π΅) β β’ (π β (π Β· π) = π) | ||
Theorem | psrass1 21525* | Associative identity for the ring of power series. (Contributed by Mario Carneiro, 5-Jan-2015.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ Γ = (.rβπ) & β’ π΅ = (Baseβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π Γ π) Γ π) = (π Γ (π Γ π))) | ||
Theorem | psrdi 21526* | Distributive law for the ring of power series (left-distributivity). (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ Γ = (.rβπ) & β’ π΅ = (Baseβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ + = (+gβπ) β β’ (π β (π Γ (π + π)) = ((π Γ π) + (π Γ π))) | ||
Theorem | psrdir 21527* | Distributive law for the ring of power series (right-distributivity). (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ Γ = (.rβπ) & β’ π΅ = (Baseβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ + = (+gβπ) β β’ (π β ((π + π) Γ π) = ((π Γ π) + (π Γ π))) | ||
Theorem | psrass23l 21528* | Associative identity for the ring of power series. Part of psrass23 21530 which does not require the scalar ring to be commutative. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 14-Aug-2019.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ Γ = (.rβπ) & β’ π΅ = (Baseβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΎ = (Baseβπ ) & β’ Β· = ( Β·π βπ) & β’ (π β π΄ β πΎ) β β’ (π β ((π΄ Β· π) Γ π) = (π΄ Β· (π Γ π))) | ||
Theorem | psrcom 21529* | Commutative law for the ring of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ Γ = (.rβπ) & β’ π΅ = (Baseβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β CRing) β β’ (π β (π Γ π) = (π Γ π)) | ||
Theorem | psrass23 21530* | Associative identities for the ring of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) (Proof shortened by AV, 25-Nov-2019.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ Γ = (.rβπ) & β’ π΅ = (Baseβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β CRing) & β’ πΎ = (Baseβπ ) & β’ Β· = ( Β·π βπ) & β’ (π β π΄ β πΎ) β β’ (π β (((π΄ Β· π) Γ π) = (π΄ Β· (π Γ π)) β§ (π Γ (π΄ Β· π)) = (π΄ Β· (π Γ π)))) | ||
Theorem | psrring 21531 | The ring of power series is a ring. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) β β’ (π β π β Ring) | ||
Theorem | psr1 21532* | The identity element of the ring of power series. (Contributed by Mario Carneiro, 8-Jan-2015.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ π = (1rβπ) β β’ (π β π = (π₯ β π· β¦ if(π₯ = (πΌ Γ {0}), 1 , 0 ))) | ||
Theorem | psrcrng 21533 | The ring of power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β CRing) β β’ (π β π β CRing) | ||
Theorem | psrassa 21534 | The ring of power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ (π β πΌ β π) & β’ (π β π β CRing) β β’ (π β π β AssAlg) | ||
Theorem | resspsrbas 21535 | A restricted power series algebra has the same base set. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (πΌ mPwSer π ) & β’ π» = (π βΎs π) & β’ π = (πΌ mPwSer π») & β’ π΅ = (Baseβπ) & β’ π = (π βΎs π΅) & β’ (π β π β (SubRingβπ )) β β’ (π β π΅ = (Baseβπ)) | ||
Theorem | resspsradd 21536 | A restricted power series algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (πΌ mPwSer π ) & β’ π» = (π βΎs π) & β’ π = (πΌ mPwSer π») & β’ π΅ = (Baseβπ) & β’ π = (π βΎs π΅) & β’ (π β π β (SubRingβπ )) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(+gβπ)π) = (π(+gβπ)π)) | ||
Theorem | resspsrmul 21537 | A restricted power series algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (πΌ mPwSer π ) & β’ π» = (π βΎs π) & β’ π = (πΌ mPwSer π») & β’ π΅ = (Baseβπ) & β’ π = (π βΎs π΅) & β’ (π β π β (SubRingβπ )) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(.rβπ)π) = (π(.rβπ)π)) | ||
Theorem | resspsrvsca 21538 | A restricted power series algebra has the same scalar multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (πΌ mPwSer π ) & β’ π» = (π βΎs π) & β’ π = (πΌ mPwSer π») & β’ π΅ = (Baseβπ) & β’ π = (π βΎs π΅) & β’ (π β π β (SubRingβπ )) β β’ ((π β§ (π β π β§ π β π΅)) β (π( Β·π βπ)π) = (π( Β·π βπ)π)) | ||
Theorem | subrgpsr 21539 | A subring of the base ring induces a subring of power series. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (πΌ mPwSer π ) & β’ π» = (π βΎs π) & β’ π = (πΌ mPwSer π») & β’ π΅ = (Baseβπ) β β’ ((πΌ β π β§ π β (SubRingβπ )) β π΅ β (SubRingβπ)) | ||
Theorem | mvrfval 21540* | Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π = (πΌ mVar π ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ (π β πΌ β π) & β’ (π β π β π) β β’ (π β π = (π₯ β πΌ β¦ (π β π· β¦ if(π = (π¦ β πΌ β¦ if(π¦ = π₯, 1, 0)), 1 , 0 )))) | ||
Theorem | mvrval 21541* | Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π = (πΌ mVar π ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β πΌ) β β’ (π β (πβπ) = (π β π· β¦ if(π = (π¦ β πΌ β¦ if(π¦ = π, 1, 0)), 1 , 0 ))) | ||
Theorem | mvrval2 21542* | Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π = (πΌ mVar π ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β πΌ) & β’ (π β πΉ β π·) β β’ (π β ((πβπ)βπΉ) = if(πΉ = (π¦ β πΌ β¦ if(π¦ = π, 1, 0)), 1 , 0 )) | ||
Theorem | mvrid 21543* | The ππ-th coefficient of the term ππ is 1. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π = (πΌ mVar π ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β πΌ) β β’ (π β ((πβπ)β(π¦ β πΌ β¦ if(π¦ = π, 1, 0))) = 1 ) | ||
Theorem | mvrf 21544 | The power series variable function is a function from the index set to elements of the power series structure representing ππ for each π. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ π = (πΌ mVar π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) β β’ (π β π:πΌβΆπ΅) | ||
Theorem | mvrf1 21545 | The power series variable function is injective if the base ring is nonzero. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ π = (πΌ mVar π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ (π β 1 β 0 ) β β’ (π β π:πΌβ1-1βπ΅) | ||
Theorem | mvrcl2 21546 | A power series variable is an element of the base set. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (πΌ mPwSer π ) & β’ π = (πΌ mVar π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β πΌ) β β’ (π β (πβπ) β π΅) | ||
Theorem | reldmmpl 21547 | The multivariate polynomial constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ Rel dom mPoly | ||
Theorem | mplval 21548* | Value of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) |
β’ π = (πΌ mPoly π ) & β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π = {π β π΅ β£ π finSupp 0 } β β’ π = (π βΎs π) | ||
Theorem | mplbas 21549* | Base set of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) |
β’ π = (πΌ mPoly π ) & β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π = (Baseβπ) β β’ π = {π β π΅ β£ π finSupp 0 } | ||
Theorem | mplelbas 21550 | Property of being a polynomial. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) |
β’ π = (πΌ mPoly π ) & β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π = (Baseβπ) β β’ (π β π β (π β π΅ β§ π finSupp 0 )) | ||
Theorem | mvrcl 21551 | A power series variable is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPoly π ) & β’ π = (πΌ mVar π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β πΌ) β β’ (π β (πβπ) β π΅) | ||
Theorem | mvrf2 21552 | The power series/polynomial variable function maps indices to polynomials. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π = (πΌ mVar π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) β β’ (π β π:πΌβΆπ΅) | ||
Theorem | mplrcl 21553 | Reverse closure for the polynomial index set. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) β β’ (π β π΅ β πΌ β V) | ||
Theorem | mplelsfi 21554 | A polynomial treated as a coefficient function has finitely many nonzero terms. (Contributed by Stefan O'Rear, 22-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ (π β πΉ β π΅) & β’ (π β π β π) β β’ (π β πΉ finSupp 0 ) | ||
Theorem | mplval2 21555 | Self-referential expression for the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (πΌ mPoly π ) & β’ π = (πΌ mPwSer π ) & β’ π = (Baseβπ) β β’ π = (π βΎs π) | ||
Theorem | mplbasss 21556 | The set of polynomials is a subset of the set of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (πΌ mPoly π ) & β’ π = (πΌ mPwSer π ) & β’ π = (Baseβπ) & β’ π΅ = (Baseβπ) β β’ π β π΅ | ||
Theorem | mplelf 21557* | A polynomial is defined as a function on the coefficients. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (πΌ mPoly π ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ (π β π β π΅) β β’ (π β π:π·βΆπΎ) | ||
Theorem | mplsubglem 21558* | If π΄ is an ideal of sets (a nonempty collection closed under subset and binary union) of the set π· of finite bags (the primary applications being π΄ = Fin and π΄ = π« π΅ for some π΅), then the set of all power series whose coefficient functions are supported on an element of π΄ is a subgroup of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015.) (Revised by AV, 16-Jul-2019.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ (π β πΌ β π) & β’ (π β β β π΄) & β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β (π₯ βͺ π¦) β π΄) & β’ ((π β§ (π₯ β π΄ β§ π¦ β π₯)) β π¦ β π΄) & β’ (π β π = {π β π΅ β£ (π supp 0 ) β π΄}) & β’ (π β π β Grp) β β’ (π β π β (SubGrpβπ)) | ||
Theorem | mpllsslem 21559* | If π΄ is an ideal of subsets (a nonempty collection closed under subset and binary union) of the set π· of finite bags (the primary applications being π΄ = Fin and π΄ = π« π΅ for some π΅), then the set of all power series whose coefficient functions are supported on an element of π΄ is a linear subspace of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015.) (Revised by AV, 16-Jul-2019.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ (π β πΌ β π) & β’ (π β β β π΄) & β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β (π₯ βͺ π¦) β π΄) & β’ ((π β§ (π₯ β π΄ β§ π¦ β π₯)) β π¦ β π΄) & β’ (π β π = {π β π΅ β£ (π supp 0 ) β π΄}) & β’ (π β π β Ring) β β’ (π β π β (LSubSpβπ)) | ||
Theorem | mplsubglem2 21560* | Lemma for mplsubg 21561 and mpllss 21562. (Contributed by AV, 16-Jul-2019.) |
β’ π = (πΌ mPwSer π ) & β’ π = (πΌ mPoly π ) & β’ π = (Baseβπ) & β’ (π β πΌ β π) β β’ (π β π = {π β (Baseβπ) β£ (π supp (0gβπ )) β Fin}) | ||
Theorem | mplsubg 21561 | The set of polynomials is closed under addition, i.e. it is a subgroup of the set of power series. (Contributed by Mario Carneiro, 8-Jan-2015.) (Proof shortened by AV, 16-Jul-2019.) |
β’ π = (πΌ mPwSer π ) & β’ π = (πΌ mPoly π ) & β’ π = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Grp) β β’ (π β π β (SubGrpβπ)) | ||
Theorem | mpllss 21562 | The set of polynomials is closed under scalar multiplication, i.e. it is a linear subspace of the set of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) (Proof shortened by AV, 16-Jul-2019.) |
β’ π = (πΌ mPwSer π ) & β’ π = (πΌ mPoly π ) & β’ π = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) β β’ (π β π β (LSubSpβπ)) | ||
Theorem | mplsubrglem 21563* | Lemma for mplsubrg 21564. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by AV, 18-Jul-2019.) |
β’ π = (πΌ mPwSer π ) & β’ π = (πΌ mPoly π ) & β’ π = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ π΄ = ( βf + β ((π supp 0 ) Γ (π supp 0 ))) & β’ Β· = (.rβπ ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π(.rβπ)π) β π) | ||
Theorem | mplsubrg 21564 | The set of polynomials is closed under multiplication, i.e. it is a subring of the set of power series. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPwSer π ) & β’ π = (πΌ mPoly π ) & β’ π = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) β β’ (π β π β (SubRingβπ)) | ||
Theorem | mpl0 21565* | The zero polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π = (0gβπ ) & β’ 0 = (0gβπ) & β’ (π β πΌ β π) & β’ (π β π β Grp) β β’ (π β 0 = (π· Γ {π})) | ||
Theorem | mplplusg 21566 | Value of addition in a polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (πΌ mPoly π ) & β’ π = (πΌ mPwSer π ) & β’ + = (+gβπ) β β’ + = (+gβπ) | ||
Theorem | mplmulr 21567 | Value of multiplication in a polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (πΌ mPoly π ) & β’ π = (πΌ mPwSer π ) & β’ Β· = (.rβπ) β β’ Β· = (.rβπ) | ||
Theorem | mpladd 21568 | The addition operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ ) & β’ β = (+gβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β π) = (π βf + π)) | ||
Theorem | mplneg 21569 | The negative function on multivariate polynomials. (Contributed by SN, 25-May-2024.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ π = (invgβπ ) & β’ π = (invgβπ) & β’ (π β πΌ β π) & β’ (π β π β Grp) & β’ (π β π β π΅) β β’ (π β (πβπ) = (π β π)) | ||
Theorem | mplmul 21570* | The multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (πΉ β πΊ) = (π β π· β¦ (π Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πΉβπ₯) Β· (πΊβ(π βf β π₯))))))) | ||
Theorem | mpl1 21571* | The identity element of the ring of polynomials. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ π = (1rβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) β β’ (π β π = (π₯ β π· β¦ if(π₯ = (πΌ Γ {0}), 1 , 0 ))) | ||
Theorem | mplsca 21572 | The scalar field of a multivariate polynomial structure. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPoly π ) & β’ (π β πΌ β π) & β’ (π β π β π) β β’ (π β π = (Scalarβπ)) | ||
Theorem | mplvsca2 21573 | The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPoly π ) & β’ π = (πΌ mPwSer π ) & β’ Β· = ( Β·π βπ) β β’ Β· = ( Β·π βπ) | ||
Theorem | mplvsca 21574* | The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (πΌ mPoly π ) & β’ β = ( Β·π βπ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β π β πΎ) & β’ (π β πΉ β π΅) β β’ (π β (π β πΉ) = ((π· Γ {π}) βf Β· πΉ)) | ||
Theorem | mplvscaval 21575* | The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPoly π ) & β’ β = ( Β·π βπ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β π β πΎ) & β’ (π β πΉ β π΅) & β’ (π β π β π·) β β’ (π β ((π β πΉ)βπ) = (π Β· (πΉβπ))) | ||
Theorem | mplgrp 21576 | The polynomial ring is a group. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPoly π ) β β’ ((πΌ β π β§ π β Grp) β π β Grp) | ||
Theorem | mpllmod 21577 | The polynomial ring is a left module. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPoly π ) β β’ ((πΌ β π β§ π β Ring) β π β LMod) | ||
Theorem | mplring 21578 | The polynomial ring is a ring. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPoly π ) β β’ ((πΌ β π β§ π β Ring) β π β Ring) | ||
Theorem | mpllvec 21579 | The polynomial ring is a vector space. (Contributed by SN, 29-Feb-2024.) |
β’ π = (πΌ mPoly π ) β β’ ((πΌ β π β§ π β DivRing) β π β LVec) | ||
Theorem | mplcrng 21580 | The polynomial ring is a commutative ring. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPoly π ) β β’ ((πΌ β π β§ π β CRing) β π β CRing) | ||
Theorem | mplassa 21581 | The polynomial ring is an associative algebra. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPoly π ) β β’ ((πΌ β π β§ π β CRing) β π β AssAlg) | ||
Theorem | ressmplbas2 21582 | The base set of a restricted polynomial algebra consists of power series in the subring which are also polynomials (in the parent ring). (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (πΌ mPoly π ) & β’ π» = (π βΎs π) & β’ π = (πΌ mPoly π») & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β (SubRingβπ )) & β’ π = (πΌ mPwSer π») & β’ πΆ = (Baseβπ) & β’ πΎ = (Baseβπ) β β’ (π β π΅ = (πΆ β© πΎ)) | ||
Theorem | ressmplbas 21583 | A restricted polynomial algebra has the same base set. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (πΌ mPoly π ) & β’ π» = (π βΎs π) & β’ π = (πΌ mPoly π») & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β (SubRingβπ )) & β’ π = (π βΎs π΅) β β’ (π β π΅ = (Baseβπ)) | ||
Theorem | ressmpladd 21584 | A restricted polynomial algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (πΌ mPoly π ) & β’ π» = (π βΎs π) & β’ π = (πΌ mPoly π») & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β (SubRingβπ )) & β’ π = (π βΎs π΅) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(+gβπ)π) = (π(+gβπ)π)) | ||
Theorem | ressmplmul 21585 | A restricted polynomial algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (πΌ mPoly π ) & β’ π» = (π βΎs π) & β’ π = (πΌ mPoly π») & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β (SubRingβπ )) & β’ π = (π βΎs π΅) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(.rβπ)π) = (π(.rβπ)π)) | ||
Theorem | ressmplvsca 21586 | A restricted power series algebra has the same scalar multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (πΌ mPoly π ) & β’ π» = (π βΎs π) & β’ π = (πΌ mPoly π») & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β (SubRingβπ )) & β’ π = (π βΎs π΅) β β’ ((π β§ (π β π β§ π β π΅)) β (π( Β·π βπ)π) = (π( Β·π βπ)π)) | ||
Theorem | subrgmpl 21587 | A subring of the base ring induces a subring of polynomials. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (πΌ mPoly π ) & β’ π» = (π βΎs π) & β’ π = (πΌ mPoly π») & β’ π΅ = (Baseβπ) β β’ ((πΌ β π β§ π β (SubRingβπ )) β π΅ β (SubRingβπ)) | ||
Theorem | subrgmvr 21588 | The variables in a subring polynomial algebra are the same as the original ring. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (πΌ mVar π ) & β’ (π β πΌ β π) & β’ (π β π β (SubRingβπ )) & β’ π» = (π βΎs π) β β’ (π β π = (πΌ mVar π»)) | ||
Theorem | subrgmvrf 21589 | The variables in a polynomial algebra are contained in every subring algebra. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (πΌ mVar π ) & β’ (π β πΌ β π) & β’ (π β π β (SubRingβπ )) & β’ π» = (π βΎs π) & β’ π = (πΌ mPoly π») & β’ π΅ = (Baseβπ) β β’ (π β π:πΌβΆπ΅) | ||
Theorem | mplmon 21590* | A monomial is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β π·) β β’ (π β (π¦ β π· β¦ if(π¦ = π, 1 , 0 )) β π΅) | ||
Theorem | mplmonmul 21591* | The product of two monomials adds the exponent vectors together. For example, the product of (π₯β2)(π¦β2) with (π¦β1)(π§β3) is (π₯β2)(π¦β3)(π§β3), where the exponent vectors β¨2, 2, 0β© and β¨0, 1, 3β© are added to give β¨2, 3, 3β©. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β π·) & β’ Β· = (.rβπ) & β’ (π β π β π·) β β’ (π β ((π¦ β π· β¦ if(π¦ = π, 1 , 0 )) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) = (π¦ β π· β¦ if(π¦ = (π βf + π), 1 , 0 ))) | ||
Theorem | mplcoe1 21592* | Decompose a polynomial into a finite sum of monomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ (π β πΌ β π) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β π = (π Ξ£g (π β π· β¦ ((πβπ) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 )))))) | ||
Theorem | mplcoe3 21593* | Decompose a monomial in one variable into a power of a variable. (Contributed by Mario Carneiro, 7-Jan-2015.) (Proof shortened by AV, 18-Jul-2019.) |
β’ π = (πΌ mPoly π ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ (π β πΌ β π) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ π = (πΌ mVar π ) & β’ (π β π β Ring) & β’ (π β π β πΌ) & β’ (π β π β β0) β β’ (π β (π¦ β π· β¦ if(π¦ = (π β πΌ β¦ if(π = π, π, 0)), 1 , 0 )) = (π β (πβπ))) | ||
Theorem | mplcoe5lem 21594* | Lemma for mplcoe4 21632. (Contributed by AV, 7-Oct-2019.) |
β’ π = (πΌ mPoly π ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ (π β πΌ β π) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ π = (πΌ mVar π ) & β’ (π β π β Ring) & β’ (π β π β π·) & β’ (π β βπ₯ β πΌ βπ¦ β πΌ ((πβπ¦)(+gβπΊ)(πβπ₯)) = ((πβπ₯)(+gβπΊ)(πβπ¦))) & β’ (π β π β πΌ) β β’ (π β ran (π β π β¦ ((πβπ) β (πβπ))) β ((CntzβπΊ)βran (π β π β¦ ((πβπ) β (πβπ))))) | ||
Theorem | mplcoe5 21595* | Decompose a monomial into a finite product of powers of variables. Instead of assuming that π is a commutative ring (as in mplcoe2 21596), it is sufficient that π is a ring and all the variables of the multivariate polynomial commute. (Contributed by AV, 7-Oct-2019.) |
β’ π = (πΌ mPoly π ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ (π β πΌ β π) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ π = (πΌ mVar π ) & β’ (π β π β Ring) & β’ (π β π β π·) & β’ (π β βπ₯ β πΌ βπ¦ β πΌ ((πβπ¦)(+gβπΊ)(πβπ₯)) = ((πβπ₯)(+gβπΊ)(πβπ¦))) β β’ (π β (π¦ β π· β¦ if(π¦ = π, 1 , 0 )) = (πΊ Ξ£g (π β πΌ β¦ ((πβπ) β (πβπ))))) | ||
Theorem | mplcoe2 21596* | Decompose a monomial into a finite product of powers of variables. (The assumption that π is a commutative ring is not strictly necessary, because the submonoid of monomials is in the center of the multiplicative monoid of polynomials, but it simplifies the proof.) (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof shortened by AV, 18-Oct-2019.) |
β’ π = (πΌ mPoly π ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ (π β πΌ β π) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ π = (πΌ mVar π ) & β’ (π β π β CRing) & β’ (π β π β π·) β β’ (π β (π¦ β π· β¦ if(π¦ = π, 1 , 0 )) = (πΊ Ξ£g (π β πΌ β¦ ((πβπ) β (πβπ))))) | ||
Theorem | mplbas2 21597 | An alternative expression for the set of polynomials, as the smallest subalgebra of the set of power series that contains all the variable generators. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π = (πΌ mPoly π ) & β’ π = (πΌ mPwSer π ) & β’ π = (πΌ mVar π ) & β’ π΄ = (AlgSpanβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) β β’ (π β (π΄βran π) = (Baseβπ)) | ||
Theorem | ltbval 21598* | Value of the well-order on finite bags. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ πΆ = (π <bag πΌ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) β β’ (π β πΆ = {β¨π₯, π¦β© β£ ({π₯, π¦} β π· β§ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€))))}) | ||
Theorem | ltbwe 21599* | The finite bag order is a well-order, given a well-order of the index set. (Contributed by Mario Carneiro, 2-Jun-2015.) |
β’ πΆ = (π <bag πΌ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π We πΌ) β β’ (π β πΆ We π·) | ||
Theorem | reldmopsr 21600 | Lemma for ordered power series. (Contributed by Stefan O'Rear, 2-Oct-2015.) |
β’ Rel dom ordPwSer |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |