Home | Metamath
Proof Explorer Theorem List (p. 216 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | coe1fval3 21501* | Univariate power series coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
β’ π΄ = (coe1βπΉ) & β’ π΅ = (Baseβπ) & β’ π = (PwSer1βπ ) & β’ πΊ = (π¦ β β0 β¦ (1o Γ {π¦})) β β’ (πΉ β π΅ β π΄ = (πΉ β πΊ)) | ||
Theorem | coe1f2 21502 | Functionality of univariate power series coefficient vectors. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
β’ π΄ = (coe1βπΉ) & β’ π΅ = (Baseβπ) & β’ π = (PwSer1βπ ) & β’ πΎ = (Baseβπ ) β β’ (πΉ β π΅ β π΄:β0βΆπΎ) | ||
Theorem | coe1fval2 21503* | Univariate polynomial coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
β’ π΄ = (coe1βπΉ) & β’ π΅ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ πΊ = (π¦ β β0 β¦ (1o Γ {π¦})) β β’ (πΉ β π΅ β π΄ = (πΉ β πΊ)) | ||
Theorem | coe1f 21504 | Functionality of univariate polynomial coefficient vectors. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
β’ π΄ = (coe1βπΉ) & β’ π΅ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ πΎ = (Baseβπ ) β β’ (πΉ β π΅ β π΄:β0βΆπΎ) | ||
Theorem | coe1fvalcl 21505 | A coefficient of a univariate polynomial over a class/ring is an element of this class/ring. (Contributed by AV, 9-Oct-2019.) |
β’ π΄ = (coe1βπΉ) & β’ π΅ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ πΎ = (Baseβπ ) β β’ ((πΉ β π΅ β§ π β β0) β (π΄βπ) β πΎ) | ||
Theorem | coe1sfi 21506 | Finite support of univariate polynomial coefficient vectors. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 19-Jul-2019.) |
β’ π΄ = (coe1βπΉ) & β’ π΅ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ ) β β’ (πΉ β π΅ β π΄ finSupp 0 ) | ||
Theorem | coe1fsupp 21507* | The coefficient vector of a univariate polynomial is a finitely supported mapping from the nonnegative integers to the elements of the coefficient class/ring for the polynomial. (Contributed by AV, 3-Oct-2019.) |
β’ π΄ = (coe1βπΉ) & β’ π΅ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ ) & β’ πΎ = (Baseβπ ) β β’ (πΉ β π΅ β π΄ β {π β (πΎ βm β0) β£ π finSupp 0 }) | ||
Theorem | mptcoe1fsupp 21508* | A mapping involving coefficients of polynomials is finitely supported. (Contributed by AV, 12-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β π΅) β (π β β0 β¦ ((coe1βπ)βπ)) finSupp 0 ) | ||
Theorem | coe1ae0 21509* | The coefficient vector of a univariate polynomial is 0 almost everywhere. (Contributed by AV, 19-Oct-2019.) |
β’ π΄ = (coe1βπΉ) & β’ π΅ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ ) β β’ (πΉ β π΅ β βπ β β0 βπ β β0 (π < π β (π΄βπ) = 0 )) | ||
Theorem | vr1cl 21510 | The generator of a univariate polynomial algebra is contained in the base set. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
β’ π = (var1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) β β’ (π β Ring β π β π΅) | ||
Theorem | opsr0 21511 | Zero in the ordered power series ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (πΌ mPwSer π ) & β’ π = ((πΌ ordPwSer π )βπ) & β’ (π β π β (πΌ Γ πΌ)) β β’ (π β (0gβπ) = (0gβπ)) | ||
Theorem | opsr1 21512 | One in the ordered power series ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (πΌ mPwSer π ) & β’ π = ((πΌ ordPwSer π )βπ) & β’ (π β π β (πΌ Γ πΌ)) β β’ (π β (1rβπ) = (1rβπ)) | ||
Theorem | mplplusg 21513 | 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 21514 | 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 | psr1plusg 21515 | Value of addition in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (PwSer1βπ ) & β’ π = (1o mPwSer π ) & β’ + = (+gβπ) β β’ + = (+gβπ) | ||
Theorem | psr1vsca 21516 | Value of scalar multiplication in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (PwSer1βπ ) & β’ π = (1o mPwSer π ) & β’ Β· = ( Β·π βπ) β β’ Β· = ( Β·π βπ) | ||
Theorem | psr1mulr 21517 | Value of multiplication in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (PwSer1βπ ) & β’ π = (1o mPwSer π ) & β’ Β· = (.rβπ) β β’ Β· = (.rβπ) | ||
Theorem | ply1plusg 21518 | Value of addition in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.) |
β’ π = (Poly1βπ ) & β’ π = (1o mPoly π ) & β’ + = (+gβπ) β β’ + = (+gβπ) | ||
Theorem | ply1vsca 21519 | Value of scalar multiplication in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.) |
β’ π = (Poly1βπ ) & β’ π = (1o mPoly π ) & β’ Β· = ( Β·π βπ) β β’ Β· = ( Β·π βπ) | ||
Theorem | ply1mulr 21520 | Value of multiplication in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.) |
β’ π = (Poly1βπ ) & β’ π = (1o mPoly π ) & β’ Β· = (.rβπ) β β’ Β· = (.rβπ) | ||
Theorem | ressply1bas2 21521 | 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.) |
β’ π = (Poly1βπ ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ π = (PwSer1βπ») & β’ πΆ = (Baseβπ) & β’ πΎ = (Baseβπ) β β’ (π β π΅ = (πΆ β© πΎ)) | ||
Theorem | ressply1bas 21522 | A restricted polynomial algebra has the same base set. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (Poly1βπ ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ π = (π βΎs π΅) β β’ (π β π΅ = (Baseβπ)) | ||
Theorem | ressply1add 21523 | A restricted polynomial algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (Poly1βπ ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ π = (π βΎs π΅) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(+gβπ)π) = (π(+gβπ)π)) | ||
Theorem | ressply1mul 21524 | A restricted polynomial algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (Poly1βπ ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ π = (π βΎs π΅) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(.rβπ)π) = (π(.rβπ)π)) | ||
Theorem | ressply1vsca 21525 | A restricted power series algebra has the same scalar multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (Poly1βπ ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ π = (π βΎs π΅) β β’ ((π β§ (π β π β§ π β π΅)) β (π( Β·π βπ)π) = (π( Β·π βπ)π)) | ||
Theorem | subrgply1 21526 | A subring of the base ring induces a subring of polynomials. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (Poly1βπ ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) β β’ (π β (SubRingβπ ) β π΅ β (SubRingβπ)) | ||
Theorem | gsumply1subr 21527 | Evaluate a group sum in a polynomial ring over a subring. (Contributed by AV, 22-Sep-2019.) (Proof shortened by AV, 31-Jan-2020.) |
β’ π = (Poly1βπ ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β (π Ξ£g πΉ) = (π Ξ£g πΉ)) | ||
Theorem | psrbaspropd 21528 | Property deduction for power series base set. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ (π β (Baseβπ ) = (Baseβπ)) β β’ (π β (Baseβ(πΌ mPwSer π )) = (Baseβ(πΌ mPwSer π))) | ||
Theorem | psrplusgpropd 21529* | Property deduction for power series addition. (Contributed by Stefan O'Rear, 27-Mar-2015.) (Revised by Mario Carneiro, 3-Oct-2015.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β π΅ = (Baseβπ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ )π¦) = (π₯(+gβπ)π¦)) β β’ (π β (+gβ(πΌ mPwSer π )) = (+gβ(πΌ mPwSer π))) | ||
Theorem | mplbaspropd 21530* | Property deduction for polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 19-Jul-2019.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β π΅ = (Baseβπ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ )π¦) = (π₯(+gβπ)π¦)) β β’ (π β (Baseβ(πΌ mPoly π )) = (Baseβ(πΌ mPoly π))) | ||
Theorem | psropprmul 21531 | Reversing multiplication in a ring reverses multiplication in the power series ring. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ π = (πΌ mPwSer π ) & β’ π = (opprβπ ) & β’ π = (πΌ mPwSer π) & β’ Β· = (.rβπ) & β’ β = (.rβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (πΉ β πΊ) = (πΊ Β· πΉ)) | ||
Theorem | ply1opprmul 21532 | Reversing multiplication in a ring reverses multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π = (opprβπ ) & β’ π = (Poly1βπ) & β’ Β· = (.rβπ) & β’ β = (.rβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (πΉ β πΊ) = (πΊ Β· πΉ)) | ||
Theorem | 00ply1bas 21533 | Lemma for ply1basfvi 21534 and deg1fvi 25372. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ β = (Baseβ(Poly1ββ )) | ||
Theorem | ply1basfvi 21534 | Protection compatibility of the univariate polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ (Baseβ(Poly1βπ )) = (Baseβ(Poly1β( I βπ ))) | ||
Theorem | ply1plusgfvi 21535 | Protection compatibility of the univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ (+gβ(Poly1βπ )) = (+gβ(Poly1β( I βπ ))) | ||
Theorem | ply1baspropd 21536* | Property deduction for univariate polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β π΅ = (Baseβπ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ )π¦) = (π₯(+gβπ)π¦)) β β’ (π β (Baseβ(Poly1βπ )) = (Baseβ(Poly1βπ))) | ||
Theorem | ply1plusgpropd 21537* | Property deduction for univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β π΅ = (Baseβπ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ )π¦) = (π₯(+gβπ)π¦)) β β’ (π β (+gβ(Poly1βπ )) = (+gβ(Poly1βπ))) | ||
Theorem | opsrring 21538 | Ordered power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
β’ π = ((πΌ ordPwSer π )βπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β (πΌ Γ πΌ)) β β’ (π β π β Ring) | ||
Theorem | opsrlmod 21539 | Ordered power series form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = ((πΌ ordPwSer π )βπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β (πΌ Γ πΌ)) β β’ (π β π β LMod) | ||
Theorem | psr1ring 21540 | Univariate power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
β’ π = (PwSer1βπ ) β β’ (π β Ring β π β Ring) | ||
Theorem | ply1ring 21541 | Univariate polynomials form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
β’ π = (Poly1βπ ) β β’ (π β Ring β π β Ring) | ||
Theorem | psr1lmod 21542 | Univariate power series form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (PwSer1βπ ) β β’ (π β Ring β π β LMod) | ||
Theorem | psr1sca 21543 | Scalars of a univariate power series ring. (Contributed by Stefan O'Rear, 4-Jul-2015.) |
β’ π = (PwSer1βπ ) β β’ (π β π β π = (Scalarβπ)) | ||
Theorem | psr1sca2 21544 | Scalars of a univariate power series ring. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.) |
β’ π = (PwSer1βπ ) β β’ ( I βπ ) = (Scalarβπ) | ||
Theorem | ply1lmod 21545 | Univariate polynomials form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (Poly1βπ ) β β’ (π β Ring β π β LMod) | ||
Theorem | ply1sca 21546 | Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (Poly1βπ ) β β’ (π β π β π = (Scalarβπ)) | ||
Theorem | ply1sca2 21547 | Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (Poly1βπ ) β β’ ( I βπ ) = (Scalarβπ) | ||
Theorem | ply1mpl0 21548 | The univariate polynomial ring has the same zero as the corresponding multivariate polynomial ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 3-Oct-2015.) |
β’ π = (1o mPoly π ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) β β’ 0 = (0gβπ) | ||
Theorem | ply10s0 21549 | Zero times a univariate polynomial is the zero polynomial (lmod0vs 20278 analog.) (Contributed by AV, 2-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ β = ( Β·π βπ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β π΅) β ( 0 β π) = (0gβπ)) | ||
Theorem | ply1mpl1 21550 | The univariate polynomial ring has the same one as the corresponding multivariate polynomial ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 3-Oct-2015.) |
β’ π = (1o mPoly π ) & β’ π = (Poly1βπ ) & β’ 1 = (1rβπ) β β’ 1 = (1rβπ) | ||
Theorem | ply1ascl 21551 | The univariate polynomial ring inherits the multivariate ring's scalar function. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by Fan Zheng, 26-Jun-2016.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) β β’ π΄ = (algScβ(1o mPoly π )) | ||
Theorem | subrg1ascl 21552 | The scalar injection function in a subring algebra is the same up to a restriction to the subring. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ (π β π β (SubRingβπ )) & β’ πΆ = (algScβπ) β β’ (π β πΆ = (π΄ βΎ π)) | ||
Theorem | subrg1asclcl 21553 | The scalars in a polynomial algebra are in the subring algebra iff the scalar value is in the subring. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ (π β π β (SubRingβπ )) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ (π β π β πΎ) β β’ (π β ((π΄βπ) β π΅ β π β π)) | ||
Theorem | subrgvr1 21554 | The variables in a subring polynomial algebra are the same as the original ring. (Contributed by Mario Carneiro, 5-Jul-2015.) |
β’ π = (var1βπ ) & β’ (π β π β (SubRingβπ )) & β’ π» = (π βΎs π) β β’ (π β π = (var1βπ»)) | ||
Theorem | subrgvr1cl 21555 | The variables in a polynomial algebra are contained in every subring algebra. (Contributed by Mario Carneiro, 5-Jul-2015.) |
β’ π = (var1βπ ) & β’ (π β π β (SubRingβπ )) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) β β’ (π β π β π΅) | ||
Theorem | coe1z 21556 | The coefficient vector of 0. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π = (0gβπ ) β β’ (π β Ring β (coe1β 0 ) = (β0 Γ {π})) | ||
Theorem | coe1add 21557 | The coefficient vector of an addition. (Contributed by Stefan O'Rear, 24-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ β = (+gβπ) & β’ + = (+gβπ ) β β’ ((π β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (coe1β(πΉ β πΊ)) = ((coe1βπΉ) βf + (coe1βπΊ))) | ||
Theorem | coe1addfv 21558 | A particular coefficient of an addition. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ β = (+gβπ) & β’ + = (+gβπ ) β β’ (((π β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β ((coe1β(πΉ β πΊ))βπ) = (((coe1βπΉ)βπ) + ((coe1βπΊ)βπ))) | ||
Theorem | coe1subfv 21559 | A particular coefficient of a subtraction. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ β = (-gβπ) & β’ π = (-gβπ ) β β’ (((π β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β ((coe1β(πΉ β πΊ))βπ) = (((coe1βπΉ)βπ)π((coe1βπΊ)βπ))) | ||
Theorem | coe1mul2lem1 21560 | An equivalence for coe1mul2 21562. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
β’ ((π΄ β β0 β§ π β (β0 βm 1o)) β (π βr β€ (1o Γ {π΄}) β (πββ ) β (0...π΄))) | ||
Theorem | coe1mul2lem2 21561* | An equivalence for coe1mul2 21562. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
β’ π» = {π β (β0 βm 1o) β£ π βr β€ (1o Γ {π})} β β’ (π β β0 β (π β π» β¦ (πββ )):π»β1-1-ontoβ(0...π)) | ||
Theorem | coe1mul2 21562* | The coefficient vector of multiplication in the univariate power series ring. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
β’ π = (PwSer1βπ ) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (coe1β(πΉ β πΊ)) = (π β β0 β¦ (π Ξ£g (π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β· ((coe1βπΊ)β(π β π₯))))))) | ||
Theorem | coe1mul 21563* | The coefficient vector of multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (coe1β(πΉ β πΊ)) = (π β β0 β¦ (π Ξ£g (π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β· ((coe1βπΊ)β(π β π₯))))))) | ||
Theorem | ply1moncl 21564 | Closure of the expression for a univariate primitive monomial. (Contributed by AV, 14-Aug-2019.) |
β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ π· β β0) β (π· β π) β π΅) | ||
Theorem | ply1tmcl 21565 | Closure of the expression for a univariate polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 25-Nov-2019.) |
β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΆ β πΎ β§ π· β β0) β (πΆ Β· (π· β π)) β π΅) | ||
Theorem | coe1tm 21566* | Coefficient vector of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ 0 = (0gβπ ) & β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ ((π β Ring β§ πΆ β πΎ β§ π· β β0) β (coe1β(πΆ Β· (π· β π))) = (π₯ β β0 β¦ if(π₯ = π·, πΆ, 0 ))) | ||
Theorem | coe1tmfv1 21567 | Nonzero coefficient of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ 0 = (0gβπ ) & β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ ((π β Ring β§ πΆ β πΎ β§ π· β β0) β ((coe1β(πΆ Β· (π· β π)))βπ·) = πΆ) | ||
Theorem | coe1tmfv2 21568 | Zero coefficient of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ 0 = (0gβπ ) & β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ (π β π β Ring) & β’ (π β πΆ β πΎ) & β’ (π β π· β β0) & β’ (π β πΉ β β0) & β’ (π β π· β πΉ) β β’ (π β ((coe1β(πΆ Β· (π· β π)))βπΉ) = 0 ) | ||
Theorem | coe1tmmul2 21569* | Coefficient vector of a polynomial multiplied on the right by a term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ 0 = (0gβπ ) & β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ π΅ = (Baseβπ) & β’ β = (.rβπ) & β’ Γ = (.rβπ ) & β’ (π β π΄ β π΅) & β’ (π β π β Ring) & β’ (π β πΆ β πΎ) & β’ (π β π· β β0) β β’ (π β (coe1β(π΄ β (πΆ Β· (π· β π)))) = (π₯ β β0 β¦ if(π· β€ π₯, (((coe1βπ΄)β(π₯ β π·)) Γ πΆ), 0 ))) | ||
Theorem | coe1tmmul 21570* | Coefficient vector of a polynomial multiplied on the left by a term. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ 0 = (0gβπ ) & β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ π΅ = (Baseβπ) & β’ β = (.rβπ) & β’ Γ = (.rβπ ) & β’ (π β π΄ β π΅) & β’ (π β π β Ring) & β’ (π β πΆ β πΎ) & β’ (π β π· β β0) β β’ (π β (coe1β((πΆ Β· (π· β π)) β π΄)) = (π₯ β β0 β¦ if(π· β€ π₯, (πΆ Γ ((coe1βπ΄)β(π₯ β π·))), 0 ))) | ||
Theorem | coe1tmmul2fv 21571 | Function value of a right-multiplication by a term in the shifted domain. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ 0 = (0gβπ ) & β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ π΅ = (Baseβπ) & β’ β = (.rβπ) & β’ Γ = (.rβπ ) & β’ (π β π΄ β π΅) & β’ (π β π β Ring) & β’ (π β πΆ β πΎ) & β’ (π β π· β β0) & β’ (π β π β β0) β β’ (π β ((coe1β(π΄ β (πΆ Β· (π· β π))))β(π· + π)) = (((coe1βπ΄)βπ) Γ πΆ)) | ||
Theorem | coe1pwmul 21572* | Coefficient vector of a polynomial multiplied on the left by a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ 0 = (0gβπ ) & β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β π β Ring) & β’ (π β π΄ β π΅) & β’ (π β π· β β0) β β’ (π β (coe1β((π· β π) Β· π΄)) = (π₯ β β0 β¦ if(π· β€ π₯, ((coe1βπ΄)β(π₯ β π·)), 0 ))) | ||
Theorem | coe1pwmulfv 21573 | Function value of a right-multiplication by a variable power in the shifted domain. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ 0 = (0gβπ ) & β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β π β Ring) & β’ (π β π΄ β π΅) & β’ (π β π· β β0) & β’ (π β π β β0) β β’ (π β ((coe1β((π· β π) Β· π΄))β(π· + π)) = ((coe1βπ΄)βπ)) | ||
Theorem | ply1scltm 21574 | A scalar is a term with zero exponent. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ π΄ = (algScβπ) β β’ ((π β Ring β§ πΉ β πΎ) β (π΄βπΉ) = (πΉ Β· (0 β π))) | ||
Theorem | coe1sclmul 21575 | Coefficient vector of a polynomial multiplied on the left by a scalar. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ π΄ = (algScβπ) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β πΎ β§ π β π΅) β (coe1β((π΄βπ) β π)) = ((β0 Γ {π}) βf Β· (coe1βπ))) | ||
Theorem | coe1sclmulfv 21576 | A single coefficient of a polynomial multiplied on the left by a scalar. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ π΄ = (algScβπ) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β πΎ β§ π β π΅) β§ 0 β β0) β ((coe1β((π΄βπ) β π))β 0 ) = (π Β· ((coe1βπ)β 0 ))) | ||
Theorem | coe1sclmul2 21577 | Coefficient vector of a polynomial multiplied on the right by a scalar. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ π΄ = (algScβπ) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β πΎ β§ π β π΅) β (coe1β(π β (π΄βπ))) = ((coe1βπ) βf Β· (β0 Γ {π}))) | ||
Theorem | ply1sclf 21578 | A scalar polynomial is a polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) β β’ (π β Ring β π΄:πΎβΆπ΅) | ||
Theorem | ply1sclcl 21579 | The value of the algebra scalars function for (univariate) polynomials applied to a scalar results in a constant polynomial. (Contributed by AV, 27-Nov-2019.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ π β πΎ) β (π΄βπ) β π΅) | ||
Theorem | coe1scl 21580* | Coefficient vector of a scalar. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ πΎ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β πΎ) β (coe1β(π΄βπ)) = (π₯ β β0 β¦ if(π₯ = 0, π, 0 ))) | ||
Theorem | ply1sclid 21581 | Recover the base scalar from a scalar polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ πΎ = (Baseβπ ) β β’ ((π β Ring β§ π β πΎ) β π = ((coe1β(π΄βπ))β0)) | ||
Theorem | ply1sclf1 21582 | The polynomial scalar function is injective. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) β β’ (π β Ring β π΄:πΎβ1-1βπ΅) | ||
Theorem | ply1scl0 21583 | The zero scalar is zero. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) β β’ (π β Ring β (π΄β 0 ) = π) | ||
Theorem | ply1scln0 21584 | Nonzero scalars create nonzero polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ πΎ = (Baseβπ ) β β’ ((π β Ring β§ π β πΎ β§ π β 0 ) β (π΄βπ) β π) | ||
Theorem | ply1scl1 21585 | The one scalar is the unit polynomial. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ 1 = (1rβπ ) & β’ π = (1rβπ) β β’ (π β Ring β (π΄β 1 ) = π) | ||
Theorem | ply1idvr1 21586 | The identity of a polynomial ring expressed as power of the polynomial variable. (Contributed by AV, 14-Aug-2019.) |
β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ (π β Ring β (0 β π) = (1rβπ)) | ||
Theorem | cply1mul 21587* | The product of two constant polynomials is a constant polynomial. (Contributed by AV, 18-Nov-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ Γ = (.rβπ) β β’ ((π β Ring β§ (πΉ β π΅ β§ πΊ β π΅)) β (βπ β β (((coe1βπΉ)βπ) = 0 β§ ((coe1βπΊ)βπ) = 0 ) β βπ β β ((coe1β(πΉ Γ πΊ))βπ) = 0 )) | ||
Theorem | ply1coefsupp 21588* | The decomposition of a univariate polynomial is finitely supported. Formerly part of proof for ply1coe 21589. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 8-Aug-2019.) |
β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ π΄ = (coe1βπΎ) β β’ ((π β Ring β§ πΎ β π΅) β (π β β0 β¦ ((π΄βπ) Β· (π β π))) finSupp (0gβπ)) | ||
Theorem | ply1coe 21589* | Decompose a univariate polynomial as a sum of powers. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 7-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ π΄ = (coe1βπΎ) β β’ ((π β Ring β§ πΎ β π΅) β πΎ = (π Ξ£g (π β β0 β¦ ((π΄βπ) Β· (π β π))))) | ||
Theorem | eqcoe1ply1eq 21590* | Two polynomials over the same ring are equal if they have identical coefficients. (Contributed by AV, 7-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (coe1βπΎ) & β’ πΆ = (coe1βπΏ) β β’ ((π β Ring β§ πΎ β π΅ β§ πΏ β π΅) β (βπ β β0 (π΄βπ) = (πΆβπ) β πΎ = πΏ)) | ||
Theorem | ply1coe1eq 21591* | Two polynomials over the same ring are equal iff they have identical coefficients. (Contributed by AV, 13-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (coe1βπΎ) & β’ πΆ = (coe1βπΏ) β β’ ((π β Ring β§ πΎ β π΅ β§ πΏ β π΅) β (βπ β β0 (π΄βπ) = (πΆβπ) β πΎ = πΏ)) | ||
Theorem | cply1coe0 21592* | All but the first coefficient of a constant polynomial ( i.e. a "lifted scalar") are zero. (Contributed by AV, 16-Nov-2019.) |
β’ πΎ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) β β’ ((π β Ring β§ π β πΎ) β βπ β β ((coe1β(π΄βπ))βπ) = 0 ) | ||
Theorem | cply1coe0bi 21593* | A polynomial is constant (i.e. a "lifted scalar") iff all but the first coefficient are zero. (Contributed by AV, 16-Nov-2019.) |
β’ πΎ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) β β’ ((π β Ring β§ π β π΅) β (βπ β πΎ π = (π΄βπ ) β βπ β β ((coe1βπ)βπ) = 0 )) | ||
Theorem | coe1fzgsumdlem 21594* | Lemma for coe1fzgsumd 21595 (induction step). (Contributed by AV, 8-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β Ring) & β’ (π β πΎ β β0) β β’ ((π β Fin β§ Β¬ π β π β§ π) β ((βπ₯ β π π β π΅ β ((coe1β(π Ξ£g (π₯ β π β¦ π)))βπΎ) = (π Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ)))) β (βπ₯ β (π βͺ {π})π β π΅ β ((coe1β(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπΎ) = (π Ξ£g (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ)))))) | ||
Theorem | coe1fzgsumd 21595* | Value of an evaluated coefficient in a finite group sum of polynomials. (Contributed by AV, 8-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β Ring) & β’ (π β πΎ β β0) & β’ (π β βπ₯ β π π β π΅) & β’ (π β π β Fin) β β’ (π β ((coe1β(π Ξ£g (π₯ β π β¦ π)))βπΎ) = (π Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ)))) | ||
Theorem | gsumsmonply1 21596* | A finite group sum of scaled monomials is a univariate polynomial. (Contributed by AV, 8-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β Ring) & β’ πΎ = (Baseβπ ) & β’ β = ( Β·π βπ) & β’ 0 = (0gβπ ) & β’ (π β βπ β β0 π΄ β πΎ) & β’ (π β (π β β0 β¦ π΄) finSupp 0 ) β β’ (π β (π Ξ£g (π β β0 β¦ (π΄ β (π β π)))) β π΅) | ||
Theorem | gsummoncoe1 21597* | A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. (Contributed by AV, 13-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β Ring) & β’ πΎ = (Baseβπ ) & β’ β = ( Β·π βπ) & β’ 0 = (0gβπ ) & β’ (π β βπ β β0 π΄ β πΎ) & β’ (π β (π β β0 β¦ π΄) finSupp 0 ) & β’ (π β πΏ β β0) β β’ (π β ((coe1β(π Ξ£g (π β β0 β¦ (π΄ β (π β π)))))βπΏ) = β¦πΏ / πβ¦π΄) | ||
Theorem | gsumply1eq 21598* | Two univariate polynomials given as (finitely supported) sum of scaled monomials are equal iff the corresponding coefficients are equal. (Contributed by AV, 21-Nov-2019.) |
β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β Ring) & β’ πΎ = (Baseβπ ) & β’ β = ( Β·π βπ) & β’ 0 = (0gβπ ) & β’ (π β βπ β β0 π΄ β πΎ) & β’ (π β (π β β0 β¦ π΄) finSupp 0 ) & β’ (π β βπ β β0 π΅ β πΎ) & β’ (π β (π β β0 β¦ π΅) finSupp 0 ) & β’ (π β π = (π Ξ£g (π β β0 β¦ (π΄ β (π β π))))) & β’ (π β π = (π Ξ£g (π β β0 β¦ (π΅ β (π β π))))) β β’ (π β (π = π β βπ β β0 π΄ = π΅)) | ||
Theorem | lply1binom 21599* | The binomial theorem for linear polynomials (monic polynomials of degree 1) over commutative rings: (π + π΄)βπ is the sum from π = 0 to π of (πCπ) Β· ((π΄β(π β π)) Β· (πβπ)). (Contributed by AV, 25-Aug-2019.) |
β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ + = (+gβπ) & β’ Γ = (.rβπ) & β’ Β· = (.gβπ) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ π΅ = (Baseβπ) β β’ ((π β CRing β§ π β β0 β§ π΄ β π΅) β (π β (π + π΄)) = (π Ξ£g (π β (0...π) β¦ ((πCπ) Β· (((π β π) β π΄) Γ (π β π)))))) | ||
Theorem | lply1binomsc 21600* | The binomial theorem for linear polynomials (monic polynomials of degree 1) over commutative rings, expressed by an element of this ring: (π + π΄)βπ is the sum from π = 0 to π of (πCπ) Β· ((π΄β(π β π)) Β· (πβπ)). (Contributed by AV, 25-Aug-2019.) |
β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ + = (+gβπ) & β’ Γ = (.rβπ) & β’ Β· = (.gβπ) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ πΎ = (Baseβπ ) & β’ π = (algScβπ) & β’ π» = (mulGrpβπ ) & β’ πΈ = (.gβπ») β β’ ((π β CRing β§ π β β0 β§ π΄ β πΎ) β (π β (π + (πβπ΄))) = (π Ξ£g (π β (0...π) β¦ ((πCπ) Β· ((πβ((π β π)πΈπ΄)) Γ (π β π)))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |