![]() |
Metamath
Proof Explorer Theorem List (p. 223 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | coe1tmmul2fv 22201 | 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 22202* | 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 22203 | 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 22204 | 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 22205 | 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 22206 | 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 22207 | 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 22208 | A scalar polynomial is a polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) β β’ (π β Ring β π΄:πΎβΆπ΅) | ||
Theorem | ply1sclcl 22209 | 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 22210* | 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 22211 | Recover the base scalar from a scalar polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ πΎ = (Baseβπ ) β β’ ((π β Ring β§ π β πΎ) β π = ((coe1β(π΄βπ))β0)) | ||
Theorem | ply1sclf1 22212 | The polynomial scalar function is injective. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) β β’ (π β Ring β π΄:πΎβ1-1βπ΅) | ||
Theorem | ply1scl0 22213 | The zero scalar is zero. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) β β’ (π β Ring β (π΄β 0 ) = π) | ||
Theorem | ply1scl0OLD 22214 | Obsolete version of ply1scl1 22216 as of 12-Mar-2025. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) β β’ (π β Ring β (π΄β 0 ) = π) | ||
Theorem | ply1scln0 22215 | Nonzero scalars create nonzero polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ πΎ = (Baseβπ ) β β’ ((π β Ring β§ π β πΎ β§ π β 0 ) β (π΄βπ) β π) | ||
Theorem | ply1scl1 22216 | The one scalar is the unit polynomial. (Contributed by Stefan O'Rear, 1-Apr-2015.) (Proof shortened by SN, 12-Mar-2025.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ 1 = (1rβπ ) & β’ π = (1rβπ) β β’ (π β Ring β (π΄β 1 ) = π) | ||
Theorem | ply1scl1OLD 22217 | Obsolete version of ply1scl1 22216 as of 12-Mar-2025. (Contributed by Stefan O'Rear, 1-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ 1 = (1rβπ ) & β’ π = (1rβπ) β β’ (π β Ring β (π΄β 1 ) = π) | ||
Theorem | ply1idvr1 22218 | 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 22219* | 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 22220* | The decomposition of a univariate polynomial is finitely supported. Formerly part of proof for ply1coe 22221. (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 22221* | 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 22222* | 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 22223* | 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 22224* | 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 22225* | 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 22226* | Lemma for coe1fzgsumd 22227 (induction step). (Contributed by AV, 8-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β Ring) & β’ (π β πΎ β β0) β β’ ((π β Fin β§ Β¬ π β π β§ π) β ((βπ₯ β π π β π΅ β ((coe1β(π Ξ£g (π₯ β π β¦ π)))βπΎ) = (π Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ)))) β (βπ₯ β (π βͺ {π})π β π΅ β ((coe1β(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπΎ) = (π Ξ£g (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ)))))) | ||
Theorem | coe1fzgsumd 22227* | 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 | ply1scleq 22228 | Equality of a constant polynomial is the same as equality of the constant term. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π΄ = (algScβπ) & β’ (π β π β Ring) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) β β’ (π β ((π΄βπΈ) = (π΄βπΉ) β πΈ = πΉ)) | ||
Theorem | ply1chr 22229 | The characteristic of a polynomial ring is the characteristic of the underlying ring. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π = (Poly1βπ ) β β’ (π β CRing β (chrβπ) = (chrβπ )) | ||
Theorem | gsumsmonply1 22230* | 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 22231* | 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 22232* | 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 22233* | 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 22234* | 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π) Β· ((πβ((π β π)πΈπ΄)) Γ (π β π)))))) | ||
Theorem | ply1fermltlchr 22235 | Fermat's little theorem for polynomials in a commutative ring πΉ of characteristic π prime: we have the polynomial equation (π + π΄)βπ = ((πβπ) + π΄). (Contributed by Thierry Arnoux, 9-Jan-2025.) |
β’ π = (Poly1βπΉ) & β’ π = (var1βπΉ) & β’ + = (+gβπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ πΆ = (algScβπ) & β’ π΄ = (πΆβ((β€RHomβπΉ)βπΈ)) & β’ π = (chrβπΉ) & β’ (π β πΉ β CRing) & β’ (π β π β β) & β’ (π β πΈ β β€) β β’ (π β (π β (π + π΄)) = ((π β π) + π΄)) | ||
Syntax | ces1 22236 | Evaluation of a univariate polynomial in a subring. |
class evalSub1 | ||
Syntax | ce1 22237 | Evaluation of a univariate polynomial. |
class eval1 | ||
Definition | df-evls1 22238* | Define the evaluation map for the univariate polynomial algebra. The function (π evalSub1 π ):πβΆ(π βm π) makes sense when π is a ring and π is a subring of π, and where π is the set of polynomials in (Poly1βπ ). This function maps an element of the formal polynomial algebra (with coefficients in π ) to a function from assignments to the variable from π into an element of π formed by evaluating the polynomial with the given assignment. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ evalSub1 = (π β V, π β π« (Baseβπ ) β¦ β¦(Baseβπ ) / πβ¦((π₯ β (π βm (π βm 1o)) β¦ (π₯ β (π¦ β π β¦ (1o Γ {π¦})))) β ((1o evalSub π )βπ))) | ||
Definition | df-evl1 22239* | Define the evaluation map for the univariate polynomial algebra. The function (eval1βπ ):πβΆ(π βm π ) makes sense when π is a ring, and π is the set of polynomials in (Poly1βπ ). This function maps an element of the formal polynomial algebra (with coefficients in π ) to a function from assignments to the variable from π into an element of π formed by evaluating the polynomial with the given assignment. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ eval1 = (π β V β¦ β¦(Baseβπ) / πβ¦((π₯ β (π βm (π βm 1o)) β¦ (π₯ β (π¦ β π β¦ (1o Γ {π¦})))) β (1o eval π))) | ||
Theorem | reldmevls1 22240 | Well-behaved binary operation property of evalSub1. (Contributed by AV, 7-Sep-2019.) |
β’ Rel dom evalSub1 | ||
Theorem | ply1frcl 22241 | Reverse closure for the set of univariate polynomial functions. (Contributed by AV, 9-Sep-2019.) |
β’ π = ran (π evalSub1 π ) β β’ (π β π β (π β V β§ π β π« (Baseβπ))) | ||
Theorem | evls1fval 22242* | Value of the univariate polynomial evaluation map function. (Contributed by AV, 7-Sep-2019.) |
β’ π = (π evalSub1 π ) & β’ πΈ = (1o evalSub π) & β’ π΅ = (Baseβπ) β β’ ((π β π β§ π β π« π΅) β π = ((π₯ β (π΅ βm (π΅ βm 1o)) β¦ (π₯ β (π¦ β π΅ β¦ (1o Γ {π¦})))) β (πΈβπ ))) | ||
Theorem | evls1val 22243* | Value of the univariate polynomial evaluation map. (Contributed by AV, 10-Sep-2019.) |
β’ π = (π evalSub1 π ) & β’ πΈ = (1o evalSub π) & β’ π΅ = (Baseβπ) & β’ π = (1o mPoly (π βΎs π )) & β’ πΎ = (Baseβπ) β β’ ((π β CRing β§ π β (SubRingβπ) β§ π΄ β πΎ) β (πβπ΄) = (((πΈβπ )βπ΄) β (π¦ β π΅ β¦ (1o Γ {π¦})))) | ||
Theorem | evls1rhmlem 22244* | Lemma for evl1rhm 22255 and evls1rhm 22245 (formerly part of the proof of evl1rhm 22255): The first function of the composition forming the univariate polynomial evaluation map function for a (sub)ring is a ring homomorphism. (Contributed by AV, 11-Sep-2019.) |
β’ π΅ = (Baseβπ ) & β’ π = (π βs π΅) & β’ πΉ = (π₯ β (π΅ βm (π΅ βm 1o)) β¦ (π₯ β (π¦ β π΅ β¦ (1o Γ {π¦})))) β β’ (π β CRing β πΉ β ((π βs (π΅ βm 1o)) RingHom π)) | ||
Theorem | evls1rhm 22245 | Polynomial evaluation is a homomorphism (into the product ring). (Contributed by AV, 11-Sep-2019.) |
β’ π = (π evalSub1 π ) & β’ π΅ = (Baseβπ) & β’ π = (π βs π΅) & β’ π = (π βΎs π ) & β’ π = (Poly1βπ) β β’ ((π β CRing β§ π β (SubRingβπ)) β π β (π RingHom π)) | ||
Theorem | evls1sca 22246 | Univariate polynomial evaluation maps scalars to constant functions. (Contributed by AV, 8-Sep-2019.) |
β’ π = (π evalSub1 π ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) β β’ (π β (πβ(π΄βπ)) = (π΅ Γ {π})) | ||
Theorem | evls1gsumadd 22247* | Univariate polynomial evaluation maps (additive) group sums to group sums. (Contributed by AV, 14-Sep-2019.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ 0 = (0gβπ) & β’ π = (π βΎs π ) & β’ π = (π βs πΎ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ ((π β§ π₯ β π) β π β π΅) & β’ (π β π β β0) & β’ (π β (π₯ β π β¦ π) finSupp 0 ) β β’ (π β (πβ(π Ξ£g (π₯ β π β¦ π))) = (π Ξ£g (π₯ β π β¦ (πβπ)))) | ||
Theorem | evls1gsummul 22248* | Univariate polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by AV, 14-Sep-2019.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ πΊ = (mulGrpβπ) & β’ 1 = (1rβπ) & β’ π = (π βΎs π ) & β’ π = (π βs πΎ) & β’ π» = (mulGrpβπ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ ((π β§ π₯ β π) β π β π΅) & β’ (π β π β β0) & β’ (π β (π₯ β π β¦ π) finSupp 1 ) β β’ (π β (πβ(πΊ Ξ£g (π₯ β π β¦ π))) = (π» Ξ£g (π₯ β π β¦ (πβπ)))) | ||
Theorem | evls1pw 22249 | Univariate polynomial evaluation for subrings maps the exponentiation of a polynomial to the exponentiation of the evaluated polynomial. (Contributed by SN, 29-Feb-2024.) |
β’ π = (π evalSub1 π ) & β’ π = (π βΎs π ) & β’ π = (Poly1βπ) & β’ πΊ = (mulGrpβπ) & β’ πΎ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β = (.gβπΊ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β β0) & β’ (π β π β π΅) β β’ (π β (πβ(π β π)) = (π(.gβ(mulGrpβ(π βs πΎ)))(πβπ))) | ||
Theorem | evls1varpw 22250 | Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019.) |
β’ π = (π evalSub1 π ) & β’ π = (π βΎs π ) & β’ π = (Poly1βπ) & β’ πΊ = (mulGrpβπ) & β’ π = (var1βπ) & β’ π΅ = (Baseβπ) & β’ β = (.gβπΊ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β β0) β β’ (π β (πβ(π β π)) = (π(.gβ(mulGrpβ(π βs π΅)))(πβπ))) | ||
Theorem | evl1fval 22251* | Value of the simple/same ring evaluation map. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (eval1βπ ) & β’ π = (1o eval π ) & β’ π΅ = (Baseβπ ) β β’ π = ((π₯ β (π΅ βm (π΅ βm 1o)) β¦ (π₯ β (π¦ β π΅ β¦ (1o Γ {π¦})))) β π) | ||
Theorem | evl1val 22252* | Value of the simple/same ring evaluation map. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (eval1βπ ) & β’ π = (1o eval π ) & β’ π΅ = (Baseβπ ) & β’ π = (1o mPoly π ) & β’ πΎ = (Baseβπ) β β’ ((π β CRing β§ π΄ β πΎ) β (πβπ΄) = ((πβπ΄) β (π¦ β π΅ β¦ (1o Γ {π¦})))) | ||
Theorem | evl1fval1lem 22253 | Lemma for evl1fval1 22254. (Contributed by AV, 11-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π΅ = (Baseβπ ) β β’ (π β π β π = (π evalSub1 π΅)) | ||
Theorem | evl1fval1 22254 | Value of the simple/same ring evaluation map function for univariate polynomials. (Contributed by AV, 11-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π΅ = (Baseβπ ) β β’ π = (π evalSub1 π΅) | ||
Theorem | evl1rhm 22255 | Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Mario Carneiro, 12-Jun-2015.) (Proof shortened by AV, 13-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π = (π βs π΅) & β’ π΅ = (Baseβπ ) β β’ (π β CRing β π β (π RingHom π)) | ||
Theorem | fveval1fvcl 22256 | The function value of the evaluation function of a polynomial is an element of the underlying ring. (Contributed by AV, 17-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β π β π) β β’ (π β ((πβπ)βπ) β π΅) | ||
Theorem | evl1sca 22257 | Polynomial evaluation maps scalars to constant functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π΄ = (algScβπ) β β’ ((π β CRing β§ π β π΅) β (πβ(π΄βπ)) = (π΅ Γ {π})) | ||
Theorem | evl1scad 22258 | Polynomial evaluation builder for scalars. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π΄ = (algScβπ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π΄βπ) β π β§ ((πβ(π΄βπ))βπ) = π)) | ||
Theorem | evl1var 22259 | Polynomial evaluation maps the variable to the identity function. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (eval1βπ ) & β’ π = (var1βπ ) & β’ π΅ = (Baseβπ ) β β’ (π β CRing β (πβπ) = ( I βΎ π΅)) | ||
Theorem | evl1vard 22260 | Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (var1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) β β’ (π β (π β π β§ ((πβπ)βπ) = π)) | ||
Theorem | evls1var 22261 | Univariate polynomial evaluation for subrings maps the variable to the identity function. (Contributed by AV, 13-Sep-2019.) |
β’ π = (π evalSub1 π ) & β’ π = (var1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) β β’ (π β (πβπ) = ( I βΎ π΅)) | ||
Theorem | evls1scasrng 22262 | The evaluation of a scalar of a subring yields the same result as evaluated as a scalar over the ring itself. (Contributed by AV, 13-Sep-2019.) |
β’ π = (π evalSub1 π ) & β’ π = (eval1βπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π = (Poly1βπ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ πΆ = (algScβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) β β’ (π β (πβ(π΄βπ)) = (πβ(πΆβπ))) | ||
Theorem | evls1varsrng 22263 | The evaluation of the variable of univariate polynomials over subring yields the same result as evaluated as variable of the polynomials over the ring itself. (Contributed by AV, 12-Sep-2019.) |
β’ π = (π evalSub1 π ) & β’ π = (eval1βπ) & β’ π = (var1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) β β’ (π β (πβπ) = (πβπ)) | ||
Theorem | evl1addd 22264 | Polynomial evaluation builder for addition of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ β = (+gβπ) & β’ + = (+gβπ ) β β’ (π β ((π β π) β π β§ ((πβ(π β π))βπ) = (π + π))) | ||
Theorem | evl1subd 22265 | Polynomial evaluation builder for subtraction of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ β = (-gβπ) & β’ π· = (-gβπ ) β β’ (π β ((π β π) β π β§ ((πβ(π β π))βπ) = (ππ·π))) | ||
Theorem | evl1muld 22266 | Polynomial evaluation builder for multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) β β’ (π β ((π β π) β π β§ ((πβ(π β π))βπ) = (π Β· π))) | ||
Theorem | evl1vsd 22267 | Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ (π β π β π΅) & β’ β = ( Β·π βπ) & β’ Β· = (.rβπ ) β β’ (π β ((π β π) β π β§ ((πβ(π β π))βπ) = (π Β· π))) | ||
Theorem | evl1expd 22268 | Polynomial evaluation builder for an exponential. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ β = (.gβ(mulGrpβπ)) & β’ β = (.gβ(mulGrpβπ )) & β’ (π β π β β0) β β’ (π β ((π β π) β π β§ ((πβ(π β π))βπ) = (π β π))) | ||
Theorem | pf1const 22269 | Constants are polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = ran (eval1βπ ) β β’ ((π β CRing β§ π β π΅) β (π΅ Γ {π}) β π) | ||
Theorem | pf1id 22270 | The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = ran (eval1βπ ) β β’ (π β CRing β ( I βΎ π΅) β π) | ||
Theorem | pf1subrg 22271 | Polynomial functions are a subring. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = ran (eval1βπ ) β β’ (π β CRing β π β (SubRingβ(π βs π΅))) | ||
Theorem | pf1rcl 22272 | Reverse closure for the set of polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) β β’ (π β π β π β CRing) | ||
Theorem | pf1f 22273 | Polynomial functions are functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ π΅ = (Baseβπ ) β β’ (πΉ β π β πΉ:π΅βΆπ΅) | ||
Theorem | mpfpf1 22274* | Convert a multivariate polynomial function to univariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ π΅ = (Baseβπ ) & β’ πΈ = ran (1o eval π ) β β’ (πΉ β πΈ β (πΉ β (π¦ β π΅ β¦ (1o Γ {π¦}))) β π) | ||
Theorem | pf1mpf 22275* | Convert a univariate polynomial function to multivariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ π΅ = (Baseβπ ) & β’ πΈ = ran (1o eval π ) β β’ (πΉ β π β (πΉ β (π₯ β (π΅ βm 1o) β¦ (π₯ββ ))) β πΈ) | ||
Theorem | pf1addcl 22276 | The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ + = (+gβπ ) β β’ ((πΉ β π β§ πΊ β π) β (πΉ βf + πΊ) β π) | ||
Theorem | pf1mulcl 22277 | The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ Β· = (.rβπ ) β β’ ((πΉ β π β§ πΊ β π) β (πΉ βf Β· πΊ) β π) | ||
Theorem | pf1ind 22278* | Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ π = ran (eval1βπ ) & β’ ((π β§ ((π β π β§ π) β§ (π β π β§ π))) β π) & β’ ((π β§ ((π β π β§ π) β§ (π β π β§ π))) β π) & β’ (π₯ = (π΅ Γ {π}) β (π β π)) & β’ (π₯ = ( I βΎ π΅) β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π₯ = (π βf + π) β (π β π)) & β’ (π₯ = (π βf Β· π) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ ((π β§ π β π΅) β π) & β’ (π β π) & β’ (π β π΄ β π) β β’ (π β π) | ||
Theorem | evl1gsumdlem 22279* | Lemma for evl1gsumd 22280 (induction step). (Contributed by AV, 17-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) β β’ ((π β Fin β§ Β¬ π β π β§ π) β ((βπ₯ β π π β π β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) β (βπ₯ β (π βͺ {π})π β π β ((πβ(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπ) = (π Ξ£g (π₯ β (π βͺ {π}) β¦ ((πβπ)βπ)))))) | ||
Theorem | evl1gsumd 22280* | Polynomial evaluation builder for a finite group sum of polynomials. (Contributed by AV, 17-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β βπ₯ β π π β π) & β’ (π β π β Fin) β β’ (π β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) | ||
Theorem | evl1gsumadd 22281* | Univariate polynomial evaluation maps (additive) group sums to group sums. Remark: the proof would be shorter if the theorem is proved directly instead of using evls1gsumadd 22247. (Contributed by AV, 15-Sep-2019.) |
β’ π = (eval1βπ ) & β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (π βs πΎ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ ((π β§ π₯ β π) β π β π΅) & β’ (π β π β β0) & β’ 0 = (0gβπ) & β’ (π β (π₯ β π β¦ π) finSupp 0 ) β β’ (π β (πβ(π Ξ£g (π₯ β π β¦ π))) = (π Ξ£g (π₯ β π β¦ (πβπ)))) | ||
Theorem | evl1gsumaddval 22282* | Value of a univariate polynomial evaluation mapping an additive group sum to a group sum of the evaluated variable. (Contributed by AV, 17-Sep-2019.) |
β’ π = (eval1βπ ) & β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (π βs πΎ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ ((π β§ π₯ β π) β π β π΅) & β’ (π β π β β0) & β’ (π β π β Fin) & β’ (π β πΆ β πΎ) β β’ (π β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπΆ) = (π Ξ£g (π₯ β π β¦ ((πβπ)βπΆ)))) | ||
Theorem | evl1gsummul 22283* | Univariate polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by AV, 15-Sep-2019.) |
β’ π = (eval1βπ ) & β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (π βs πΎ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ ((π β§ π₯ β π) β π β π΅) & β’ (π β π β β0) & β’ 1 = (1rβπ) & β’ πΊ = (mulGrpβπ) & β’ π» = (mulGrpβπ) & β’ (π β (π₯ β π β¦ π) finSupp 1 ) β β’ (π β (πβ(πΊ Ξ£g (π₯ β π β¦ π))) = (π» Ξ£g (π₯ β π β¦ (πβπ)))) | ||
Theorem | evl1varpw 22284 | Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd 22281, the proof is shorter using evls1varpw 22250 instead of proving it directly. (Contributed by AV, 15-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ πΊ = (mulGrpβπ) & β’ π = (var1βπ ) & β’ π΅ = (Baseβπ ) & β’ β = (.gβπΊ) & β’ (π β π β CRing) & β’ (π β π β β0) β β’ (π β (πβ(π β π)) = (π(.gβ(mulGrpβ(π βs π΅)))(πβπ))) | ||
Theorem | evl1varpwval 22285 | Value of a univariate polynomial evaluation mapping the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ πΊ = (mulGrpβπ) & β’ π = (var1βπ ) & β’ π΅ = (Baseβπ ) & β’ β = (.gβπΊ) & β’ (π β π β CRing) & β’ (π β π β β0) & β’ (π β πΆ β π΅) & β’ π» = (mulGrpβπ ) & β’ πΈ = (.gβπ») β β’ (π β ((πβ(π β π))βπΆ) = (ππΈπΆ)) | ||
Theorem | evl1scvarpw 22286 | Univariate polynomial evaluation maps a multiple of an exponentiation of a variable to the multiple of an exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ πΊ = (mulGrpβπ) & β’ π = (var1βπ ) & β’ π΅ = (Baseβπ ) & β’ β = (.gβπΊ) & β’ (π β π β CRing) & β’ (π β π β β0) & β’ Γ = ( Β·π βπ) & β’ (π β π΄ β π΅) & β’ π = (π βs π΅) & β’ β = (.rβπ) & β’ π = (mulGrpβπ) & β’ πΉ = (.gβπ) β β’ (π β (πβ(π΄ Γ (π β π))) = ((π΅ Γ {π΄}) β (ππΉ(πβπ)))) | ||
Theorem | evl1scvarpwval 22287 | Value of a univariate polynomial evaluation mapping a multiple of an exponentiation of a variable to the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ πΊ = (mulGrpβπ) & β’ π = (var1βπ ) & β’ π΅ = (Baseβπ ) & β’ β = (.gβπΊ) & β’ (π β π β CRing) & β’ (π β π β β0) & β’ Γ = ( Β·π βπ) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ π» = (mulGrpβπ ) & β’ πΈ = (.gβπ») & β’ Β· = (.rβπ ) β β’ (π β ((πβ(π΄ Γ (π β π)))βπΆ) = (π΄ Β· (ππΈπΆ))) | ||
Theorem | evl1gsummon 22288* | Value of a univariate polynomial evaluation mapping an additive group sum of a multiple of an exponentiation of a variable to a group sum of the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019.) |
β’ π = (eval1βπ ) & β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π = (var1βπ ) & β’ π» = (mulGrpβπ ) & β’ πΈ = (.gβπ») & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ Γ = ( Β·π βπ) & β’ Β· = (.rβπ ) & β’ (π β π β CRing) & β’ (π β βπ₯ β π π΄ β πΎ) & β’ (π β π β β0) & β’ (π β π β Fin) & β’ (π β βπ₯ β π π β β0) & β’ (π β πΆ β πΎ) β β’ (π β ((πβ(π Ξ£g (π₯ β π β¦ (π΄ Γ (π β π)))))βπΆ) = (π Ξ£g (π₯ β π β¦ (π΄ Β· (ππΈπΆ))))) | ||
Theorem | evls1scafv 22289 | Value of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) & β’ (π β πΆ β π΅) β β’ (π β ((πβ(π΄βπ))βπΆ) = π) | ||
Theorem | evls1expd 22290 | Univariate polynomial evaluation builder for an exponential. See also evl1expd 22268. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ β§ = (.gβ(mulGrpβπ)) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β β0) & β’ (π β π β π΅) & β’ (π β πΆ β πΎ) β β’ (π β ((πβ(π β§ π))βπΆ) = (π β ((πβπ)βπΆ))) | ||
Theorem | evls1varpwval 22291 | Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. See evl1varpwval 22285. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ π = (π βΎs π ) & β’ π = (Poly1βπ) & β’ π = (var1βπ) & β’ π΅ = (Baseβπ) & β’ β§ = (.gβ(mulGrpβπ)) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β β0) & β’ (π β πΆ β π΅) β β’ (π β ((πβ(π β§ π))βπΆ) = (π β πΆ)) | ||
Theorem | evls1fpws 22292* | Evaluation of a univariate subring polynomial as a function in a power series. (Contributed by Thierry Arnoux, 23-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π΅) & β’ Β· = (.rβπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π΄ = (coe1βπ) β β’ (π β (πβπ) = (π₯ β πΎ β¦ (π Ξ£g (π β β0 β¦ ((π΄βπ) Β· (π β π₯)))))) | ||
Theorem | ressply1evl 22293 | Evaluation of a univariate subring polynomial is the same as the evaluation in the bigger ring. (Contributed by Thierry Arnoux, 23-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ πΈ = (eval1βπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) β β’ (π β π = (πΈ βΎ π΅)) | ||
Theorem | evls1addd 22294 | Univariate polynomial evaluation of a sum of polynomials. (Contributed by Thierry Arnoux, 8-Feb-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & ⒠⨣ = (+gβπ) & β’ + = (+gβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΆ β πΎ) β β’ (π β ((πβ(π ⨣ π))βπΆ) = (((πβπ)βπΆ) + ((πβπ)βπΆ))) | ||
Theorem | evls1muld 22295 | Univariate polynomial evaluation of a product of polynomials. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ Γ = (.rβπ) & β’ Β· = (.rβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΆ β πΎ) β β’ (π β ((πβ(π Γ π))βπΆ) = (((πβπ)βπΆ) Β· ((πβπ)βπΆ))) | ||
Theorem | evls1vsca 22296 | Univariate polynomial evaluation of a scalar product of polynomials. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ Γ = ( Β·π βπ) & β’ Β· = (.rβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π΄ β π ) & β’ (π β π β π΅) & β’ (π β πΆ β πΎ) β β’ (π β ((πβ(π΄ Γ π))βπΆ) = (π΄ Β· ((πβπ)βπΆ))) | ||
Theorem | asclply1subcl 22297 | Closure of the algebra scalar injection function in a polynomial on a subring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
β’ π΄ = (algScβπ) & β’ π = (π βΎs π) & β’ π = (Poly1βπ ) & β’ π = (Poly1βπ) & β’ π = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ (π β π β π) β β’ (π β (π΄βπ) β π) | ||
Theorem | evls1fvcl 22298 | Variant of fveval1fvcl 22256 for the subring evaluation function evalSub1 (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) & β’ (π β π β π΅) & β’ (π β π β π) β β’ (π β ((πβπ)βπ) β π΅) | ||
Theorem | evls1maprhm 22299* | The function πΉ mapping polynomials π to their subring evaluation at a given point π is a ring homomorphism. (Contributed by Thierry Arnoux, 8-Feb-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) & β’ (π β π β π΅) & β’ πΉ = (π β π β¦ ((πβπ)βπ)) β β’ (π β πΉ β (π RingHom π )) | ||
Theorem | evls1maplmhm 22300* | The function πΉ mapping polynomials π to their subring evaluation at a given point π΄ is a module homomorphism, when considering the subring algebra. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) & β’ (π β π β π΅) & β’ πΉ = (π β π β¦ ((πβπ)βπ)) & β’ π΄ = ((subringAlg βπ )βπ) β β’ (π β πΉ β (π LMHom π΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |