![]() |
Metamath
Proof Explorer Theorem List (p. 221 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 | opsrtoslem1 22001* | Lemma for opsrtos 22003. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ π = ((πΌ ordPwSer π )βπ) & β’ (π β πΌ β π) & β’ (π β π β Toset) & β’ (π β π β (πΌ Γ πΌ)) & β’ (π β π We πΌ) & β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ < = (ltβπ ) & β’ πΆ = (π <bag πΌ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€)))) & β’ β€ = (leβπ) β β’ (π β β€ = (({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) βͺ ( I βΎ π΅))) | ||
Theorem | opsrtoslem2 22002* | Lemma for opsrtos 22003. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ π = ((πΌ ordPwSer π )βπ) & β’ (π β πΌ β π) & β’ (π β π β Toset) & β’ (π β π β (πΌ Γ πΌ)) & β’ (π β π We πΌ) & β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ < = (ltβπ ) & β’ πΆ = (π <bag πΌ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€)))) & β’ β€ = (leβπ) β β’ (π β π β Toset) | ||
Theorem | opsrtos 22003 | The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π = ((πΌ ordPwSer π )βπ) & β’ (π β πΌ β π) & β’ (π β π β Toset) & β’ (π β π β (πΌ Γ πΌ)) & β’ (π β π We πΌ) β β’ (π β π β Toset) | ||
Theorem | opsrso 22004 | The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π = ((πΌ ordPwSer π )βπ) & β’ (π β πΌ β π) & β’ (π β π β Toset) & β’ (π β π β (πΌ Γ πΌ)) & β’ (π β π We πΌ) & β’ β€ = (ltβπ) & β’ π΅ = (Baseβπ) β β’ (π β β€ Or π΅) | ||
Theorem | opsrcrng 22005 | The ring of ordered power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π = ((πΌ ordPwSer π )βπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (πΌ Γ πΌ)) β β’ (π β π β CRing) | ||
Theorem | opsrassa 22006 | The ring of ordered power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = ((πΌ ordPwSer π )βπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (πΌ Γ πΌ)) β β’ (π β π β AssAlg) | ||
Theorem | mplmon2 22007* | Express a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ Β· = ( Β·π βπ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 1 = (1rβπ ) & β’ 0 = (0gβπ ) & β’ π΅ = (Baseβπ ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β πΎ β π·) & β’ (π β π β π΅) β β’ (π β (π Β· (π¦ β π· β¦ if(π¦ = πΎ, 1 , 0 ))) = (π¦ β π· β¦ if(π¦ = πΎ, π, 0 ))) | ||
Theorem | psrbag0 22008* | The empty bag is a bag. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ (πΌ β π β (πΌ Γ {0}) β π·) | ||
Theorem | psrbagsn 22009* | A singleton bag is a bag. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} β β’ (πΌ β π β (π₯ β πΌ β¦ if(π₯ = πΎ, 1, 0)) β π·) | ||
Theorem | mplascl 22010* | Value of the scalar injection into the polynomial algebra. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ π΅ = (Baseβπ ) & β’ π΄ = (algScβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β (π΄βπ) = (π¦ β π· β¦ if(π¦ = (πΌ Γ {0}), π, 0 ))) | ||
Theorem | mplasclf 22011 | The scalar injection is a function into the polynomial algebra. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ π΄ = (algScβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) β β’ (π β π΄:πΎβΆπ΅) | ||
Theorem | subrgascl 22012 | 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.) |
β’ π = (πΌ mPoly π ) & β’ π΄ = (algScβπ) & β’ π» = (π βΎs π) & β’ π = (πΌ mPoly π») & β’ (π β πΌ β π) & β’ (π β π β (SubRingβπ )) & β’ πΆ = (algScβπ) β β’ (π β πΆ = (π΄ βΎ π)) | ||
Theorem | subrgasclcl 22013 | 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.) |
β’ π = (πΌ mPoly π ) & β’ π΄ = (algScβπ) & β’ π» = (π βΎs π) & β’ π = (πΌ mPoly π») & β’ (π β πΌ β π) & β’ (π β π β (SubRingβπ )) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ (π β π β πΎ) β β’ (π β ((π΄βπ) β π΅ β π β π)) | ||
Theorem | mplmon2cl 22014* | A scaled monomial is a polynomial. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ πΆ = (Baseβπ ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ (π β π β πΆ) & β’ (π β πΎ β π·) β β’ (π β (π¦ β π· β¦ if(π¦ = πΎ, π, 0 )) β π΅) | ||
Theorem | mplmon2mul 22015* | Product of scaled monomials. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ πΆ = (Baseβπ ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) & β’ (π β π β π·) & β’ (π β π β π·) & β’ (π β πΉ β πΆ) & β’ (π β πΊ β πΆ) β β’ (π β ((π¦ β π· β¦ if(π¦ = π, πΉ, 0 )) β (π¦ β π· β¦ if(π¦ = π, πΊ, 0 ))) = (π¦ β π· β¦ if(π¦ = (π βf + π), (πΉ Β· πΊ), 0 ))) | ||
Theorem | mplind 22016* | Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. The commutativity condition is stronger than strictly needed. (Contributed by Stefan O'Rear, 11-Mar-2015.) |
β’ πΎ = (Baseβπ ) & β’ π = (πΌ mVar π ) & β’ π = (πΌ mPoly π ) & β’ + = (+gβπ) & β’ Β· = (.rβπ) & β’ πΆ = (algScβπ) & β’ π΅ = (Baseβπ) & β’ ((π β§ (π₯ β π» β§ π¦ β π»)) β (π₯ + π¦) β π») & β’ ((π β§ (π₯ β π» β§ π¦ β π»)) β (π₯ Β· π¦) β π») & β’ ((π β§ π₯ β πΎ) β (πΆβπ₯) β π») & β’ ((π β§ π₯ β πΌ) β (πβπ₯) β π») & β’ (π β π β π΅) & β’ (π β πΌ β π) & β’ (π β π β CRing) β β’ (π β π β π») | ||
Theorem | mplcoe4 22017* | Decompose a polynomial into a finite sum of scaled monomials. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β π = (π Ξ£g (π β π· β¦ (π¦ β π· β¦ if(π¦ = π, (πβπ), 0 ))))) | ||
Syntax | ces 22018 | Evaluation of a multivariate polynomial in a subring. |
class evalSub | ||
Syntax | cevl 22019 | Evaluation of a multivariate polynomial. |
class eval | ||
Definition | df-evls 22020* | Define the evaluation map for the polynomial algebra. The function ((πΌ evalSub π)βπ ):πβΆ(π βm (π βm πΌ)) makes sense when πΌ is an index set, π is a ring, π is a subring of π, and where π is the set of polynomials in (πΌ mPoly π ). This function maps an element of the formal polynomial algebra (with coefficients in π ) to a function from assignments πΌβΆπ of the variables to elements of π formed by evaluating the polynomial with the given assignments. (Contributed by Stefan O'Rear, 11-Mar-2015.) |
β’ evalSub = (π β V, π β CRing β¦ β¦(Baseβπ ) / πβ¦(π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))))) | ||
Definition | df-evl 22021* | A simplification of evalSub when the evaluation ring is the same as the coefficient ring. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
β’ eval = (π β V, π β V β¦ ((π evalSub π)β(Baseβπ))) | ||
Theorem | evlslem4 22022* | The support of a tensor product of ring element families is contained in the product of the supports. (Contributed by Stefan O'Rear, 8-Mar-2015.) (Revised by AV, 18-Jul-2019.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ ((π β§ π₯ β πΌ) β π β π΅) & β’ ((π β§ π¦ β π½) β π β π΅) & β’ (π β πΌ β π) & β’ (π β π½ β π) β β’ (π β ((π₯ β πΌ, π¦ β π½ β¦ (π Β· π)) supp 0 ) β (((π₯ β πΌ β¦ π) supp 0 ) Γ ((π¦ β π½ β¦ π) supp 0 ))) | ||
Theorem | psrbagev1 22023* | A bag of multipliers provides the conditions for a valid sum. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) (Revised by AV, 11-Apr-2024.) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024.) |
β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ πΆ = (Baseβπ) & β’ Β· = (.gβπ) & β’ 0 = (0gβπ) & β’ (π β π β CMnd) & β’ (π β π΅ β π·) & β’ (π β πΊ:πΌβΆπΆ) β β’ (π β ((π΅ βf Β· πΊ):πΌβΆπΆ β§ (π΅ βf Β· πΊ) finSupp 0 )) | ||
Theorem | psrbagev1OLD 22024* | Obsolete version of psrbagev1 22023 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) (Revised by AV, 11-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ πΆ = (Baseβπ) & β’ Β· = (.gβπ) & β’ 0 = (0gβπ) & β’ (π β π β CMnd) & β’ (π β π΅ β π·) & β’ (π β πΊ:πΌβΆπΆ) & β’ (π β πΌ β π) β β’ (π β ((π΅ βf Β· πΊ):πΌβΆπΆ β§ (π΅ βf Β· πΊ) finSupp 0 )) | ||
Theorem | psrbagev2 22025* | Closure of a sum using a bag of multipliers. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 18-Jul-2019.) (Revised by AV, 11-Apr-2024.) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024.) |
β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ πΆ = (Baseβπ) & β’ Β· = (.gβπ) & β’ (π β π β CMnd) & β’ (π β π΅ β π·) & β’ (π β πΊ:πΌβΆπΆ) β β’ (π β (π Ξ£g (π΅ βf Β· πΊ)) β πΆ) | ||
Theorem | psrbagev2OLD 22026* | Obsolete version of psrbagev2 22025 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 18-Jul-2019.) (Revised by AV, 11-Apr-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ πΆ = (Baseβπ) & β’ Β· = (.gβπ) & β’ (π β π β CMnd) & β’ (π β π΅ β π·) & β’ (π β πΊ:πΌβΆπΆ) & β’ (π β πΌ β π) β β’ (π β (π Ξ£g (π΅ βf Β· πΊ)) β πΆ) | ||
Theorem | evlslem2 22027* | A linear function on the polynomial ring which is multiplicative on scaled monomials is generally multiplicative. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 11-Apr-2024.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β CRing) & β’ (π β πΈ β (π GrpHom π)) & β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π β π· β§ π β π·))) β (πΈβ(π β π· β¦ if(π = (π βf + π), ((π₯βπ)(.rβπ )(π¦βπ)), 0 ))) = ((πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 ))) Β· (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 ))))) β β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβ(π₯(.rβπ)π¦)) = ((πΈβπ₯) Β· (πΈβπ¦))) | ||
Theorem | evlslem3 22028* | Lemma for evlseu 22031. Polynomial evaluation of a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015.) (Revised by AV, 11-Apr-2024.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ Β· = (.rβπ) & β’ π = (πΌ mVar π ) & β’ πΈ = (π β π΅ β¦ (π Ξ£g (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))))) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β CRing) & β’ (π β πΉ β (π RingHom π)) & β’ (π β πΊ:πΌβΆπΆ) & β’ 0 = (0gβπ ) & β’ (π β π΄ β π·) & β’ (π β π» β πΎ) β β’ (π β (πΈβ(π₯ β π· β¦ if(π₯ = π΄, π», 0 ))) = ((πΉβπ») Β· (π Ξ£g (π΄ βf β πΊ)))) | ||
Theorem | evlslem6 22029* | Lemma for evlseu 22031. Finiteness and consistency of the top-level sum. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 26-Jul-2019.) (Revised by AV, 11-Apr-2024.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ Β· = (.rβπ) & β’ π = (πΌ mVar π ) & β’ πΈ = (π β π΅ β¦ (π Ξ£g (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))))) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β CRing) & β’ (π β πΉ β (π RingHom π)) & β’ (π β πΊ:πΌβΆπΆ) & β’ (π β π β π΅) β β’ (π β ((π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))):π·βΆπΆ β§ (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))) finSupp (0gβπ))) | ||
Theorem | evlslem1 22030* | Lemma for evlseu 22031, give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 26-Jul-2019.) (Revised by AV, 11-Apr-2024.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ Β· = (.rβπ) & β’ π = (πΌ mVar π ) & β’ πΈ = (π β π΅ β¦ (π Ξ£g (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))))) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β CRing) & β’ (π β πΉ β (π RingHom π)) & β’ (π β πΊ:πΌβΆπΆ) & β’ π΄ = (algScβπ) β β’ (π β (πΈ β (π RingHom π) β§ (πΈ β π΄) = πΉ β§ (πΈ β π) = πΊ)) | ||
Theorem | evlseu 22031* | For a given interpretation of the variables πΊ and of the scalars πΉ, this extends to a homomorphic interpretation of the polynomial ring in exactly one way. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 11-Apr-2024.) |
β’ π = (πΌ mPoly π ) & β’ πΆ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ π = (πΌ mVar π ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β CRing) & β’ (π β πΉ β (π RingHom π)) & β’ (π β πΊ:πΌβΆπΆ) β β’ (π β β!π β (π RingHom π)((π β π΄) = πΉ β§ (π β π) = πΊ)) | ||
Theorem | reldmevls 22032 | Well-behaved binary operation property of evalSub. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
β’ Rel dom evalSub | ||
Theorem | mpfrcl 22033 | Reverse closure for the set of polynomial functions. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
β’ π = ran ((πΌ evalSub π)βπ ) β β’ (π β π β (πΌ β V β§ π β CRing β§ π β (SubRingβπ))) | ||
Theorem | evlsval 22034* | Value of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 11-Mar-2015.) (Revised by AV, 18-Sep-2021.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ π = (πΌ mVar π) & β’ π = (π βΎs π ) & β’ π = (π βs (π΅ βm πΌ)) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ π = (π₯ β π β¦ ((π΅ βm πΌ) Γ {π₯})) & β’ π = (π₯ β πΌ β¦ (π β (π΅ βm πΌ) β¦ (πβπ₯))) β β’ ((πΌ β π β§ π β CRing β§ π β (SubRingβπ)) β π = (β©π β (π RingHom π)((π β π΄) = π β§ (π β π) = π))) | ||
Theorem | evlsval2 22035* | Characterizing properties of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 12-Mar-2015.) (Revised by AV, 18-Sep-2021.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ π = (πΌ mVar π) & β’ π = (π βΎs π ) & β’ π = (π βs (π΅ βm πΌ)) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ π = (π₯ β π β¦ ((π΅ βm πΌ) Γ {π₯})) & β’ π = (π₯ β πΌ β¦ (π β (π΅ βm πΌ) β¦ (πβπ₯))) β β’ ((πΌ β π β§ π β CRing β§ π β (SubRingβπ)) β (π β (π RingHom π) β§ ((π β π΄) = π β§ (π β π) = π))) | ||
Theorem | evlsrhm 22036 | Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Stefan O'Rear, 12-Mar-2015.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ π = (π βΎs π ) & β’ π = (π βs (π΅ βm πΌ)) & β’ π΅ = (Baseβπ) β β’ ((πΌ β π β§ π β CRing β§ π β (SubRingβπ)) β π β (π RingHom π)) | ||
Theorem | evlssca 22037 | Polynomial evaluation maps scalars to constant functions. (Contributed by Stefan O'Rear, 13-Mar-2015.) (Proof shortened by AV, 18-Sep-2021.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) β β’ (π β (πβ(π΄βπ)) = ((π΅ βm πΌ) Γ {π})) | ||
Theorem | evlsvar 22038* | Polynomial evaluation maps variables to projections. (Contributed by Stefan O'Rear, 12-Mar-2015.) (Proof shortened by AV, 18-Sep-2021.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mVar π) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β πΌ) β β’ (π β (πβ(πβπ)) = (π β (π΅ βm πΌ) β¦ (πβπ))) | ||
Theorem | evlsgsumadd 22039* | Polynomial evaluation maps (additive) group sums to group sums. (Contributed by SN, 13-Feb-2024.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ 0 = (0gβπ) & β’ π = (π βΎs π ) & β’ π = (π βs (πΎ βm πΌ)) & β’ πΎ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ ((π β§ π₯ β π) β π β π΅) & β’ (π β π β β0) & β’ (π β (π₯ β π β¦ π) finSupp 0 ) β β’ (π β (πβ(π Ξ£g (π₯ β π β¦ π))) = (π Ξ£g (π₯ β π β¦ (πβπ)))) | ||
Theorem | evlsgsummul 22040* | Polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by SN, 13-Feb-2024.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ πΊ = (mulGrpβπ) & β’ 1 = (1rβπ) & β’ π = (π βΎs π ) & β’ π = (π βs (πΎ βm πΌ)) & β’ π» = (mulGrpβπ) & β’ πΎ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ ((π β§ π₯ β π) β π β π΅) & β’ (π β π β β0) & β’ (π β (π₯ β π β¦ π) finSupp 1 ) β β’ (π β (πβ(πΊ Ξ£g (π₯ β π β¦ π))) = (π» Ξ£g (π₯ β π β¦ (πβπ)))) | ||
Theorem | evlspw 22041 | Polynomial evaluation for subrings maps the exponentiation of a polynomial to the exponentiation of the evaluated polynomial. (Contributed by SN, 29-Feb-2024.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ π = (π βΎs π ) & β’ π = (π βs (πΎ βm πΌ)) & β’ π» = (mulGrpβπ) & β’ πΎ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β β0) & β’ (π β π β π΅) β β’ (π β (πβ(π β π)) = (π(.gβπ»)(πβπ))) | ||
Theorem | evlsvarpw 22042 | Polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by SN, 21-Feb-2024.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ π = ((πΌ mVar π)βπ) & β’ π = (π βΎs π ) & β’ π = (π βs (π΅ βm πΌ)) & β’ π» = (mulGrpβπ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β πΌ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β β0) β β’ (π β (πβ(π β π)) = (π(.gβπ»)(πβπ))) | ||
Theorem | evlval 22043 | Value of the simple/same ring evaluation map. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by Mario Carneiro, 12-Jun-2015.) |
β’ π = (πΌ eval π ) & β’ π΅ = (Baseβπ ) β β’ π = ((πΌ evalSub π )βπ΅) | ||
Theorem | evlrhm 22044 | The simple evaluation map is a ring homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (πΌ eval π ) & β’ π΅ = (Baseβπ ) & β’ π = (πΌ mPoly π ) & β’ π = (π βs (π΅ βm πΌ)) β β’ ((πΌ β π β§ π β CRing) β π β (π RingHom π)) | ||
Theorem | evlsscasrng 22045 | The evaluation of a scalar of a subring yields the same result as evaluated as a scalar over the ring itself. (Contributed by AV, 12-Sep-2019.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ eval π) & β’ π = (πΌ mPoly π) & β’ π = (π βΎs π ) & β’ π = (πΌ mPoly π) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ πΆ = (algScβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) β β’ (π β (πβ(π΄βπ)) = (πβ(πΆβπ))) | ||
Theorem | evlsca 22046 | Simple polynomial evaluation maps scalars to constant functions. (Contributed by AV, 12-Sep-2019.) |
β’ π = (πΌ eval π) & β’ π = (πΌ mPoly π) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β π΅) β β’ (π β (πβ(π΄βπ)) = ((π΅ βm πΌ) Γ {π})) | ||
Theorem | evlsvarsrng 22047 | The evaluation of the variable of polynomials over subring yields the same result as evaluated as variable of the polynomials over the ring itself. (Contributed by AV, 12-Sep-2019.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ eval π) & β’ π = (πΌ mVar π) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π΄) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β πΌ) β β’ (π β (πβ(πβπ)) = (πβ(πβπ))) | ||
Theorem | evlvar 22048* | Simple polynomial evaluation maps variables to projections. (Contributed by AV, 12-Sep-2019.) |
β’ π = (πΌ eval π) & β’ π = (πΌ mVar π) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β πΌ) β β’ (π β (πβ(πβπ)) = (π β (π΅ βm πΌ) β¦ (πβπ))) | ||
Theorem | mpfconst 22049 | Constants are multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ π = ran ((πΌ evalSub π)βπ ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) β β’ (π β ((π΅ βm πΌ) Γ {π}) β π) | ||
Theorem | mpfproj 22050* | Projections are multivariate polynomial functions. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ π = ran ((πΌ evalSub π)βπ ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π½ β πΌ) β β’ (π β (π β (π΅ βm πΌ) β¦ (πβπ½)) β π) | ||
Theorem | mpfsubrg 22051 | Polynomial functions are a subring. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) (Revised by AV, 19-Sep-2021.) |
β’ π = ran ((πΌ evalSub π)βπ ) β β’ ((πΌ β π β§ π β CRing β§ π β (SubRingβπ)) β π β (SubRingβ(π βs ((Baseβπ) βm πΌ)))) | ||
Theorem | mpff 22052 | Polynomial functions are functions. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = ran ((πΌ evalSub π)βπ ) & β’ π΅ = (Baseβπ) β β’ (πΉ β π β πΉ:(π΅ βm πΌ)βΆπ΅) | ||
Theorem | mpfaddcl 22053 | The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = ran ((πΌ evalSub π)βπ ) & β’ + = (+gβπ) β β’ ((πΉ β π β§ πΊ β π) β (πΉ βf + πΊ) β π) | ||
Theorem | mpfmulcl 22054 | The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = ran ((πΌ evalSub π)βπ ) & β’ Β· = (.rβπ) β β’ ((πΉ β π β§ πΊ β π) β (πΉ βf Β· πΊ) β π) | ||
Theorem | mpfind 22055* | 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, 19-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = (.rβπ) & β’ π = ran ((πΌ evalSub π)βπ ) & β’ ((π β§ ((π β π β§ π) β§ (π β π β§ π))) β π) & β’ ((π β§ ((π β π β§ π) β§ (π β π β§ π))) β π) & β’ (π₯ = ((π΅ βm πΌ) Γ {π}) β (π β π)) & β’ (π₯ = (π β (π΅ βm πΌ) β¦ (πβπ)) β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π₯ = (π βf + π) β (π β π)) & β’ (π₯ = (π βf Β· π) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ ((π β§ π β π ) β π) & β’ ((π β§ π β πΌ) β π) & β’ (π β π΄ β π) β β’ (π β π) | ||
Syntax | cslv 22056 | Select a subset of variables in a multivariate polynomial. |
class selectVars | ||
Syntax | cmhp 22057 | Multivariate polynomials. |
class mHomP | ||
Syntax | cpsd 22058 | Power series partial derivative function. |
class mPSDer | ||
Syntax | cai 22059 | Algebraically independent. |
class AlgInd | ||
Definition | df-selv 22060* | Define the "variable selection" function. The function ((πΌ selectVars π )βπ½) maps elements of (πΌ mPoly π ) bijectively onto (π½ mPoly ((πΌ β π½) mPoly π )) in the natural way, for example if πΌ = {π₯, π¦} and π½ = {π¦} it would map 1 + π₯ + π¦ + π₯π¦ β ({π₯, π¦} mPoly β€) to (1 + π₯) + (1 + π₯)π¦ β ({π¦} mPoly ({π₯} mPoly β€)). This, for example, allows one to treat a multivariate polynomial as a univariate polynomial with coefficients in a polynomial ring with one less variable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ selectVars = (π β V, π β V β¦ (π β π« π β¦ (π β (Baseβ(π mPoly π)) β¦ β¦((π β π) mPoly π) / π’β¦β¦(π mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((π evalSub π‘)βran π)β(π β π))β(π₯ β π β¦ if(π₯ β π, ((π mVar π’)βπ₯), (πβ(((π β π) mVar π)βπ₯)))))))) | ||
Theorem | selvffval 22061* | Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.) |
β’ (π β πΌ β π) & β’ (π β π β π) β β’ (π β (πΌ selectVars π ) = (π β π« πΌ β¦ (π β (Baseβ(πΌ mPoly π )) β¦ β¦((πΌ β π) mPoly π ) / π’β¦β¦(π mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π, ((π mVar π’)βπ₯), (πβ(((πΌ β π) mVar π )βπ₯)))))))) | ||
Theorem | selvfval 22062* | Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.) |
β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π½ β πΌ) β β’ (π β ((πΌ selectVars π )βπ½) = (π β (Baseβ(πΌ mPoly π )) β¦ β¦((πΌ β π½) mPoly π ) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π )βπ₯))))))) | ||
Theorem | selvval 22063* | Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ π = ((πΌ β π½) mPoly π ) & β’ π = (π½ mPoly π) & β’ πΆ = (algScβπ) & β’ π· = (πΆ β (algScβπ)) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π½ β πΌ) & β’ (π β πΉ β π΅) β β’ (π β (((πΌ selectVars π )βπ½)βπΉ) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π )βπ₯)))))) | ||
Definition | df-mhp 22064* | Define the subspaces of order- π homogeneous polynomials. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ mHomP = (π β V, π β V β¦ (π β β0 β¦ {π β (Baseβ(π mPoly π)) β£ (π supp (0gβπ)) β {π β {β β (β0 βm π) β£ (β‘β β β) β Fin} β£ ((βfld βΎs β0) Ξ£g π) = π}})) | ||
Theorem | reldmmhp 22065 | The domain of the homogeneous polynomial operator is a relation. (Contributed by SN, 18-May-2025.) |
β’ Rel dom mHomP | ||
Theorem | mhpfval 22066* | Value of the "homogeneous polynomial" operator. (Contributed by Steven Nguyen, 25-Aug-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) β β’ (π β π» = (π β β0 β¦ {π β π΅ β£ (π supp 0 ) β {π β π· β£ ((βfld βΎs β0) Ξ£g π) = π}})) | ||
Theorem | mhpval 22067* | Value of the "homogeneous polynomial" function. (Contributed by Steven Nguyen, 25-Aug-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β β0) β β’ (π β (π»βπ) = {π β π΅ β£ (π supp 0 ) β {π β π· β£ ((βfld βΎs β0) Ξ£g π) = π}}) | ||
Theorem | ismhp 22068* | Property of being a homogeneous polynomial. (Contributed by Steven Nguyen, 25-Aug-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β β0) β β’ (π β (π β (π»βπ) β (π β π΅ β§ (π supp 0 ) β {π β π· β£ ((βfld βΎs β0) Ξ£g π) = π}))) | ||
Theorem | ismhp2 22069* | Deduce a homogeneous polynomial from its properties. (Contributed by SN, 25-May-2024.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β β0) & β’ (π β π β π΅) & β’ (π β (π supp 0 ) β {π β π· β£ ((βfld βΎs β0) Ξ£g π) = π}) β β’ (π β π β (π»βπ)) | ||
Theorem | ismhp3 22070* | A polynomial is homogeneous iff the degree of every nonzero term is the same. (Contributed by SN, 22-Jul-2024.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β β0) & β’ (π β π β π΅) β β’ (π β (π β (π»βπ) β βπ β π· ((πβπ) β 0 β ((βfld βΎs β0) Ξ£g π) = π))) | ||
Theorem | mhpmpl 22071 | A homogeneous polynomial is a polynomial. (Contributed by Steven Nguyen, 25-Aug-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β β0) & β’ (π β π β (π»βπ)) β β’ (π β π β π΅) | ||
Theorem | mhpdeg 22072* | All nonzero terms of a homogeneous polynomial have degree π. (Contributed by Steven Nguyen, 25-Aug-2023.) |
β’ π» = (πΌ mHomP π ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β β0) & β’ (π β π β (π»βπ)) β β’ (π β (π supp 0 ) β {π β π· β£ ((βfld βΎs β0) Ξ£g π) = π}) | ||
Theorem | mhp0cl 22073* | The zero polynomial is homogeneous. Under df-mhp 22064, it has any (nonnegative integer) degree which loosely corresponds to the value "undefined". The values -β and 0 are also used in Metamath (by df-mdeg 26001 and df-dgr 26138 respectively) and the literature: https://math.stackexchange.com/a/1796314/593843 26138. (Contributed by SN, 12-Sep-2023.) |
β’ π» = (πΌ mHomP π ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β Grp) & β’ (π β π β β0) β β’ (π β (π· Γ { 0 }) β (π»βπ)) | ||
Theorem | mhpsclcl 22074 | A scalar (or constant) polynomial has degree 0. Compare deg1scl 26062. In other contexts, there may be an exception for the zero polynomial, but under df-mhp 22064 the zero polynomial can be any degree (see mhp0cl 22073) so there is no exception. (Contributed by SN, 25-May-2024.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π΄ = (algScβπ) & β’ πΎ = (Baseβπ ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β πΆ β πΎ) β β’ (π β (π΄βπΆ) β (π»β0)) | ||
Theorem | mhpvarcl 22075 | A power series variable is a polynomial of degree 1. (Contributed by SN, 25-May-2024.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mVar π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β πΌ) β β’ (π β (πβπ) β (π»β1)) | ||
Theorem | mhpmulcl 22076 | A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 26028 (which shows less-than-or-equal instead of equal). (Contributed by SN, 22-Jul-2024.) Remove sethood hypothesis. (Revised by SN, 18-May-2025.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ Β· = (.rβπ) & β’ (π β π β Ring) & β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β π β (π»βπ)) & β’ (π β π β (π»βπ)) β β’ (π β (π Β· π) β (π»β(π + π))) | ||
Theorem | mhppwdeg 22077 | Degree of a homogeneous polynomial raised to a power. General version of deg1pw 26069. (Contributed by SN, 26-Jul-2024.) Remove sethood hypothesis. (Revised by SN, 18-May-2025.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ (π β π β Ring) & β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β π β (π»βπ)) β β’ (π β (π β π) β (π»β(π Β· π))) | ||
Theorem | mhpaddcl 22078 | Homogeneous polynomials are closed under addition. (Contributed by SN, 26-Aug-2023.) Remove sethood hypothesis. (Revised by SN, 18-May-2025.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ + = (+gβπ) & β’ (π β π β Grp) & β’ (π β π β β0) & β’ (π β π β (π»βπ)) & β’ (π β π β (π»βπ)) β β’ (π β (π + π) β (π»βπ)) | ||
Theorem | mhpinvcl 22079 | Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023.) Remove sethood hypothesis. (Revised by SN, 18-May-2025.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π = (invgβπ) & β’ (π β π β Grp) & β’ (π β π β β0) & β’ (π β π β (π»βπ)) β β’ (π β (πβπ) β (π»βπ)) | ||
Theorem | mhpsubg 22080 | Homogeneous polynomials form a subgroup of the polynomials. (Contributed by SN, 25-Sep-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ (π β πΌ β π) & β’ (π β π β Grp) & β’ (π β π β β0) β β’ (π β (π»βπ) β (SubGrpβπ)) | ||
Theorem | mhpvscacl 22081 | Homogeneous polynomials are closed under scalar multiplication. (Contributed by SN, 25-Sep-2023.) Remove sethood hypothesis. (Revised by SN, 18-May-2025.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ ) & β’ (π β π β Ring) & β’ (π β π β β0) & β’ (π β π β πΎ) & β’ (π β πΉ β (π»βπ)) β β’ (π β (π Β· πΉ) β (π»βπ)) | ||
Theorem | mhplss 22082 | Homogeneous polynomials form a linear subspace of the polynomials. (Contributed by SN, 25-Sep-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β β0) β β’ (π β (π»βπ) β (LSubSpβπ)) | ||
Definition | df-psd 22083* | Define the differentiation operation on multivariate polynomials. (((πΌ mPSDer π )βπ)βπΉ) is the partial derivative of the polynomial πΉ with respect to π. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ mPSDer = (π β V, π β V β¦ (π₯ β π β¦ (π β (Baseβ(π mPwSer π)) β¦ (π β {β β (β0 βm π) β£ (β‘β β β) β Fin} β¦ (((πβπ₯) + 1)(.gβπ)(πβ(π βf + (π¦ β π β¦ if(π¦ = π₯, 1, 0))))))))) | ||
Theorem | psdffval 22084* | Value of the power series differentiation operation. (Contributed by SN, 11-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) β β’ (π β (πΌ mPSDer π ) = (π₯ β πΌ β¦ (π β π΅ β¦ (π β π· β¦ (((πβπ₯) + 1)(.gβπ )(πβ(π βf + (π¦ β πΌ β¦ if(π¦ = π₯, 1, 0))))))))) | ||
Theorem | psdfval 22085* | Give a map between power series and their partial derivatives with respect to a given variable π. (Contributed by SN, 11-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β πΌ) β β’ (π β ((πΌ mPSDer π )βπ) = (π β π΅ β¦ (π β π· β¦ (((πβπ) + 1)(.gβπ )(πβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))))))) | ||
Theorem | psdval 22086* | Evaluate the partial derivative of a power series. (Contributed by SN, 11-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β πΌ) & β’ (π β πΉ β π΅) β β’ (π β (((πΌ mPSDer π )βπ)βπΉ) = (π β π· β¦ (((πβπ) + 1)(.gβπ )(πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))))) | ||
Theorem | psdcoef 22087* | Coefficient of a term of the derivative of a power series. (Contributed by SN, 12-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΎ β π·) β β’ (π β ((((πΌ mPSDer π )βπ)βπΉ)βπΎ) = (((πΎβπ) + 1)(.gβπ )(πΉβ(πΎ βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))))) | ||
Theorem | psdcl 22088 | The derivative of a power series is a power series. (Contributed by SN, 11-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Mgm) & β’ (π β π β πΌ) & β’ (π β πΉ β π΅) β β’ (π β (((πΌ mPSDer π )βπ)βπΉ) β π΅) | ||
Theorem | psdmplcl 22089 | The derivative of a polynomial is a polynomial. (Contributed by SN, 12-Apr-2025.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Mnd) & β’ (π β π β πΌ) & β’ (π β πΉ β π΅) β β’ (π β (((πΌ mPSDer π )βπ)βπΉ) β π΅) | ||
Theorem | psdadd 22090 | The derivative of a sum is the sum of the derivatives. (Contributed by SN, 12-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β πΌ β π) & β’ (π β π β CMnd) & β’ (π β π β πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (((πΌ mPSDer π )βπ)β(πΉ + πΊ)) = ((((πΌ mPSDer π )βπ)βπΉ) + (((πΌ mPSDer π )βπ)βπΊ))) | ||
Theorem | psdvsca 22091 | The derivative of a scaled power series is the scaled derivative. (Contributed by SN, 12-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΆ β πΎ) β β’ (π β (((πΌ mPSDer π )βπ)β(πΆ Β· πΉ)) = (πΆ Β· (((πΌ mPSDer π )βπ)βπΉ))) | ||
Theorem | psdmullem 22092 | Lemma for psdmul 22093. Transitive law for union of class difference. (Contributed by SN, 5-May-2025.) |
β’ (π β πΆ β π΅) & β’ (π β π΅ β π΄) β β’ (π β ((π΄ β π΅) βͺ (π΅ β πΆ)) = (π΄ β πΆ)) | ||
Theorem | psdmul 22093 | Product rule for power series. An outline is available at https://github.com/icecream17/Stuff/blob/main/math/psdmul.pdf. (Contributed by SN, 25-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = (.rβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (((πΌ mPSDer π )βπ)β(πΉ Β· πΊ)) = (((((πΌ mPSDer π )βπ)βπΉ) Β· πΊ) + (πΉ Β· (((πΌ mPSDer π )βπ)βπΊ)))) | ||
Theorem | psd1 22094 | The derivative of one is zero. (Contributed by SN, 25-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ 1 = (1rβπ) & β’ 0 = (0gβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β πΌ) β β’ (π β (((πΌ mPSDer π )βπ)β 1 ) = 0 ) | ||
Theorem | psdascl 22095 | The derivative of a constant polynomial is zero. (Contributed by SN, 25-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ 0 = (0gβπ) & β’ π΄ = (algScβπ) & β’ π΅ = (Baseβπ ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β πΌ) & β’ (π β πΆ β π΅) β β’ (π β (((πΌ mPSDer π )βπ)β(π΄βπΆ)) = 0 ) | ||
Definition | df-algind 22096* | Define the predicate "the set π£ is algebraically independent in the algebra π€". A collection of vectors is algebraically independent if no nontrivial polynomial with elements from the subset evaluates to zero. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ AlgInd = (π€ β V, π β π« (Baseβπ€) β¦ {π£ β π« (Baseβπ€) β£ Fun β‘(π β (Baseβ(π£ mPoly (π€ βΎs π))) β¦ ((((π£ evalSub π€)βπ)βπ)β( I βΎ π£)))}) | ||
According to Wikipedia ("Polynomial", 23-Dec-2019, https://en.wikipedia.org/wiki/Polynomial) "A polynomial in one indeterminate is called a univariate polynomial, a polynomial in more than one indeterminate is called a multivariate polynomial." In this sense univariate polynomials are defined as multivariate polynomials restricted to one indeterminate/polynomial variable in the following, see ply1bascl2 22127. According to the definition in Wikipedia "a polynomial can either be zero or can be written as the sum of a finite number of nonzero terms. Each term consists of the product of a number - called the coefficient of the term - and a finite number of indeterminates, raised to nonnegative integer powers.". By this, a term of a univariate polynomial (often also called "polynomial term") is the product of a coefficient (usually a member of the underlying ring) and the variable, raised to a nonnegative integer power. A (univariate) polynomial which has only one term is called (univariate) monomial - therefore, the notions "term" and "monomial" are often used synonymously, see also the definition in [Lang] p. 102. Sometimes, however, a monomial is defined as power product, "a product of powers of variables with nonnegative integer exponents", see Wikipedia ("Monomial", 23-Dec-2019, https://en.wikipedia.org/wiki/Mononomial 22127). In [Lang] p. 101, such terms are called "primitive monomials". To avoid any ambiguity, the notion "primitive monomial" is used for such power products ("x^i") in the following, whereas the synonym for "term" ("ai x^i") will be "scaled monomial". | ||
Syntax | cps1 22097 | Univariate power series. |
class PwSer1 | ||
Syntax | cv1 22098 | The base variable of a univariate power series. |
class var1 | ||
Syntax | cpl1 22099 | Univariate polynomials. |
class Poly1 | ||
Syntax | cco1 22100 | Coefficient function for a univariate polynomial. |
class coe1 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |