Home | Metamath
Proof Explorer Theorem List (p. 203 of 449) | < 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44899) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | reldmmpl 20201 | The multivariate polynomial constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ Rel dom mPoly | ||
Theorem | mplval 20202* | Value of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = {𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 } ⇒ ⊢ 𝑃 = (𝑆 ↾s 𝑈) | ||
Theorem | mplbas 20203* | Base set of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) ⇒ ⊢ 𝑈 = {𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 } | ||
Theorem | mplelbas 20204 | Property of being a polynomial. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) ⇒ ⊢ (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 finSupp 0 )) | ||
Theorem | mplval2 20205 | Self-referential expression for the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑈 = (Base‘𝑃) ⇒ ⊢ 𝑃 = (𝑆 ↾s 𝑈) | ||
Theorem | mplbasss 20206 | The set of polynomials is a subset of the set of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ 𝑈 ⊆ 𝐵 | ||
Theorem | mplelf 20207* | A polynomial is defined as a function on the coefficients. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋:𝐷⟶𝐾) | ||
Theorem | mplsubglem 20208* | If 𝐴 is an ideal of sets (a nonempty collection closed under subset and binary union) of the set 𝐷 of finite bags (the primary applications being 𝐴 = Fin and 𝐴 = 𝒫 𝐵 for some 𝐵), then the set of all power series whose coefficient functions are supported on an element of 𝐴 is a subgroup of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015.) (Revised by AV, 16-Jul-2019.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → ∅ ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∪ 𝑦) ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ∈ 𝐴) & ⊢ (𝜑 → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) & ⊢ (𝜑 → 𝑅 ∈ Grp) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑆)) | ||
Theorem | mpllsslem 20209* | If 𝐴 is an ideal of subsets (a nonempty collection closed under subset and binary union) of the set 𝐷 of finite bags (the primary applications being 𝐴 = Fin and 𝐴 = 𝒫 𝐵 for some 𝐵), then the set of all power series whose coefficient functions are supported on an element of 𝐴 is a linear subspace of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015.) (Revised by AV, 16-Jul-2019.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → ∅ ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∪ 𝑦) ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ∈ 𝐴) & ⊢ (𝜑 → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑆)) | ||
Theorem | mplsubglem2 20210* | Lemma for mplsubg 20211 and mpllss 20212. (Contributed by AV, 16-Jul-2019.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑈 = {𝑔 ∈ (Base‘𝑆) ∣ (𝑔 supp (0g‘𝑅)) ∈ Fin}) | ||
Theorem | mplsubg 20211 | The set of polynomials is closed under addition, i.e. it is a subgroup of the set of power series. (Contributed by Mario Carneiro, 8-Jan-2015.) (Proof shortened by AV, 16-Jul-2019.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Grp) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑆)) | ||
Theorem | mpllss 20212 | The set of polynomials is closed under scalar multiplication, i.e. it is a linear subspace of the set of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) (Proof shortened by AV, 16-Jul-2019.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑆)) | ||
Theorem | mplsubrglem 20213* | Lemma for mplsubrg 20214. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by AV, 18-Jul-2019.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = ( ∘f + “ ((𝑋 supp 0 ) × (𝑌 supp 0 ))) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑋(.r‘𝑆)𝑌) ∈ 𝑈) | ||
Theorem | mplsubrg 20214 | The set of polynomials is closed under multiplication, i.e. it is a subring of the set of power series. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑆)) | ||
Theorem | mpl0 20215* | The zero polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝑂 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Grp) ⇒ ⊢ (𝜑 → 0 = (𝐷 × {𝑂})) | ||
Theorem | mpladd 20216 | The addition operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ + = (+g‘𝑅) & ⊢ ✚ = (+g‘𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌)) | ||
Theorem | mplmul 20217* | The multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝑃) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∙ 𝐺) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝐹‘𝑥) · (𝐺‘(𝑘 ∘f − 𝑥))))))) | ||
Theorem | mpl1 20218* | The identity element of the ring of polynomials. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑈 = (1r‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 ))) | ||
Theorem | mplsca 20219 | The scalar field of a multivariate polynomial structure. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) | ||
Theorem | mplvsca2 20220 | The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) ⇒ ⊢ · = ( ·𝑠 ‘𝑆) | ||
Theorem | mplvsca 20221* | The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ ∙ = ( ·𝑠 ‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∙ 𝐹) = ((𝐷 × {𝑋}) ∘f · 𝐹)) | ||
Theorem | mplvscaval 20222* | The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ ∙ = ( ·𝑠 ‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → ((𝑋 ∙ 𝐹)‘𝑌) = (𝑋 · (𝐹‘𝑌))) | ||
Theorem | mvrcl 20223 | A power series variable is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑉‘𝑋) ∈ 𝐵) | ||
Theorem | mplgrp 20224 | The polynomial ring is a group. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp) → 𝑃 ∈ Grp) | ||
Theorem | mpllmod 20225 | The polynomial ring is a left module. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ LMod) | ||
Theorem | mplring 20226 | The polynomial ring is a ring. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring) | ||
Theorem | mpllvec 20227 | The polynomial ring is a vector space. (Contributed by SN, 29-Feb-2024.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ DivRing) → 𝑃 ∈ LVec) | ||
Theorem | mplcrng 20228 | The polynomial ring is a commutative ring. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ CRing) | ||
Theorem | mplassa 20229 | The polynomial ring is an associative algebra. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg) | ||
Theorem | ressmplbas2 20230 | The base set of a restricted polynomial algebra consists of power series in the subring which are also polynomials (in the parent ring). (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (𝐼 mPoly 𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (𝐼 mPoly 𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑊 = (𝐼 mPwSer 𝐻) & ⊢ 𝐶 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 ∩ 𝐾)) | ||
Theorem | ressmplbas 20231 | A restricted polynomial algebra has the same base set. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (𝐼 mPoly 𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (𝐼 mPoly 𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝑃)) | ||
Theorem | ressmpladd 20232 | A restricted polynomial algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (𝐼 mPoly 𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (𝐼 mPoly 𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑈)𝑌) = (𝑋(+g‘𝑃)𝑌)) | ||
Theorem | ressmplmul 20233 | A restricted polynomial algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (𝐼 mPoly 𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (𝐼 mPoly 𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑈)𝑌) = (𝑋(.r‘𝑃)𝑌)) | ||
Theorem | ressmplvsca 20234 | A restricted power series algebra has the same scalar multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (𝐼 mPoly 𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (𝐼 mPoly 𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵)) → (𝑋( ·𝑠 ‘𝑈)𝑌) = (𝑋( ·𝑠 ‘𝑃)𝑌)) | ||
Theorem | subrgmpl 20235 | A subring of the base ring induces a subring of polynomials. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (𝐼 mPoly 𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (𝐼 mPoly 𝐻) & ⊢ 𝐵 = (Base‘𝑈) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝐵 ∈ (SubRing‘𝑆)) | ||
Theorem | subrgmvr 20236 | The variables in a subring polynomial algebra are the same as the original ring. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) ⇒ ⊢ (𝜑 → 𝑉 = (𝐼 mVar 𝐻)) | ||
Theorem | subrgmvrf 20237 | The variables in a polynomial algebra are contained in every subring algebra. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (𝐼 mPoly 𝐻) & ⊢ 𝐵 = (Base‘𝑈) ⇒ ⊢ (𝜑 → 𝑉:𝐼⟶𝐵) | ||
Theorem | mplmon 20238* | A monomial is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )) ∈ 𝐵) | ||
Theorem | mplmonmul 20239* | The product of two monomials adds the exponent vectors together. For example, the product of (𝑥↑2)(𝑦↑2) with (𝑦↑1)(𝑧↑3) is (𝑥↑2)(𝑦↑3)(𝑧↑3), where the exponent vectors 〈2, 2, 0〉 and 〈0, 1, 3〉 are added to give 〈2, 3, 3〉. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ · = (.r‘𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑋 ∘f + 𝑌), 1 , 0 ))) | ||
Theorem | mplcoe1 20240* | Decompose a polynomial into a finite sum of monomials. (Contributed by Mario Carneiro, 9-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = (𝑃 Σg (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))) | ||
Theorem | mplcoe3 20241* | Decompose a monomial in one variable into a power of a variable. (Contributed by Mario Carneiro, 7-Jan-2015.) (Proof shortened by AV, 18-Jul-2019.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑘 ∈ 𝐼 ↦ if(𝑘 = 𝑋, 𝑁, 0)), 1 , 0 )) = (𝑁 ↑ (𝑉‘𝑋))) | ||
Theorem | mplcoe5lem 20242* | Lemma for mplcoe4 20277. (Contributed by AV, 7-Oct-2019.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐼 ((𝑉‘𝑦)(+g‘𝐺)(𝑉‘𝑥)) = ((𝑉‘𝑥)(+g‘𝐺)(𝑉‘𝑦))) & ⊢ (𝜑 → 𝑆 ⊆ 𝐼) ⇒ ⊢ (𝜑 → ran (𝑘 ∈ 𝑆 ↦ ((𝑌‘𝑘) ↑ (𝑉‘𝑘))) ⊆ ((Cntz‘𝐺)‘ran (𝑘 ∈ 𝑆 ↦ ((𝑌‘𝑘) ↑ (𝑉‘𝑘))))) | ||
Theorem | mplcoe5 20243* | Decompose a monomial into a finite product of powers of variables. Instead of assuming that 𝑅 is a commutative ring (as in mplcoe2 20244), it is sufficient that 𝑅 is a ring and all the variables of the multivariate polynomial commute. (Contributed by AV, 7-Oct-2019.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐼 ((𝑉‘𝑦)(+g‘𝐺)(𝑉‘𝑥)) = ((𝑉‘𝑥)(+g‘𝐺)(𝑉‘𝑦))) ⇒ ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )) = (𝐺 Σg (𝑘 ∈ 𝐼 ↦ ((𝑌‘𝑘) ↑ (𝑉‘𝑘))))) | ||
Theorem | mplcoe2 20244* | Decompose a monomial into a finite product of powers of variables. (The assumption that 𝑅 is a commutative ring is not strictly necessary, because the submonoid of monomials is in the center of the multiplicative monoid of polynomials, but it simplifies the proof.) (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof shortened by AV, 18-Oct-2019.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )) = (𝐺 Σg (𝑘 ∈ 𝐼 ↦ ((𝑌‘𝑘) ↑ (𝑉‘𝑘))))) | ||
Theorem | mplbas2 20245 | An alternative expression for the set of polynomials, as the smallest subalgebra of the set of power series that contains all the variable generators. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐴 = (AlgSpan‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → (𝐴‘ran 𝑉) = (Base‘𝑃)) | ||
Theorem | ltbval 20246* | Value of the well-order on finite bags. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐶 = (𝑇 <bag 𝐼) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐶 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))}) | ||
Theorem | ltbwe 20247* | The finite bag order is a well-order, given a well-order of the index set. (Contributed by Mario Carneiro, 2-Jun-2015.) |
⊢ 𝐶 = (𝑇 <bag 𝐼) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 We 𝐼) ⇒ ⊢ (𝜑 → 𝐶 We 𝐷) | ||
Theorem | reldmopsr 20248 | Lemma for ordered power series. (Contributed by Stefan O'Rear, 2-Oct-2015.) |
⊢ Rel dom ordPwSer | ||
Theorem | opsrval 20249* | The value of the "ordered power series" function. This is the same as mPwSer psrval 20136, but with the addition of a well-order on 𝐼 we can turn a strict order on 𝑅 into a strict order on the power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ < = (lt‘𝑅) & ⊢ 𝐶 = (𝑇 <bag 𝐼) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ ≤ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → 𝑂 = (𝑆 sSet 〈(le‘ndx), ≤ 〉)) | ||
Theorem | opsrle 20250* | An alternative expression for the set of polynomials, as the smallest subalgebra of the set of power series that contains all the variable generators. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ < = (lt‘𝑅) & ⊢ 𝐶 = (𝑇 <bag 𝐼) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ ≤ = (le‘𝑂) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → ≤ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}) | ||
Theorem | opsrval2 20251 | Self-referential expression for the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ ≤ = (le‘𝑂) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → 𝑂 = (𝑆 sSet 〈(le‘ndx), ≤ 〉)) | ||
Theorem | opsrbaslem 20252 | Get a component of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 9-Sep-2021.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < ;10 ⇒ ⊢ (𝜑 → (𝐸‘𝑆) = (𝐸‘𝑂)) | ||
Theorem | opsrbas 20253 | The base set of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → (Base‘𝑆) = (Base‘𝑂)) | ||
Theorem | opsrplusg 20254 | The addition operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → (+g‘𝑆) = (+g‘𝑂)) | ||
Theorem | opsrmulr 20255 | The multiplication operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → (.r‘𝑆) = (.r‘𝑂)) | ||
Theorem | opsrvsca 20256 | The scalar product operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → ( ·𝑠 ‘𝑆) = ( ·𝑠 ‘𝑂)) | ||
Theorem | opsrsca 20257 | The scalar ring of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑅 = (Scalar‘𝑂)) | ||
Theorem | opsrtoslem1 20258* | Lemma for opsrtos 20260. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Toset) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) & ⊢ (𝜑 → 𝑇 We 𝐼) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ < = (lt‘𝑅) & ⊢ 𝐶 = (𝑇 <bag 𝐼) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ (𝜑 → ≤ = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵))) | ||
Theorem | opsrtoslem2 20259* | Lemma for opsrtos 20260. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Toset) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) & ⊢ (𝜑 → 𝑇 We 𝐼) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ < = (lt‘𝑅) & ⊢ 𝐶 = (𝑇 <bag 𝐼) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ (𝜑 → 𝑂 ∈ Toset) | ||
Theorem | opsrtos 20260 | The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Toset) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) & ⊢ (𝜑 → 𝑇 We 𝐼) ⇒ ⊢ (𝜑 → 𝑂 ∈ Toset) | ||
Theorem | opsrso 20261 | 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 20262 | The ring of ordered power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → 𝑂 ∈ CRing) | ||
Theorem | opsrassa 20263 | The ring of ordered power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → 𝑂 ∈ AssAlg) | ||
Theorem | mplrcl 20264 | Reverse closure for the polynomial index set. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝑋 ∈ 𝐵 → 𝐼 ∈ V) | ||
Theorem | mplelsfi 20265 | A polynomial treated as a coefficient function has finitely many nonzero terms. (Contributed by Stefan O'Rear, 22-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 finSupp 0 ) | ||
Theorem | mvrf2 20266 | The power series/polynomial variable function maps indices to polynomials. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑉:𝐼⟶𝐵) | ||
Theorem | mplmon2 20267* | 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 20268* | The empty bag is a bag. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) ∈ 𝐷) | ||
Theorem | psrbagsn 20269* | A singleton bag is a bag. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝐾, 1, 0)) ∈ 𝐷) | ||
Theorem | mplascl 20270* | 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 20271 | 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 20272 | 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 20273 | 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 20274* | 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 20275* | 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 20276* | 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‘𝑌) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 + 𝑦) ∈ 𝐻) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 · 𝑦) ∈ 𝐻) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐶‘𝑥) ∈ 𝐻) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) ∈ 𝐻) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ V) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐻) | ||
Theorem | mplcoe4 20277* | 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 20278 | Evaluation of a multivariate polynomial in a subring. |
class evalSub | ||
Syntax | cevl 20279 | Evaluation of a multivariate polynomial. |
class eval | ||
Definition | df-evls 20280* | 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 20281* | 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 20282* | 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 | psrbagfsupp 20283* | Finite bags have finite nonzero-support. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ⇒ ⊢ ((𝑋 ∈ 𝐷 ∧ 𝐼 ∈ 𝑉) → 𝑋 finSupp 0) | ||
Theorem | psrbagev1 20284* | 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.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐶 = (Base‘𝑇) & ⊢ · = (.g‘𝑇) & ⊢ 0 = (0g‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ CMnd) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐺:𝐼⟶𝐶) & ⊢ (𝜑 → 𝐼 ∈ V) ⇒ ⊢ (𝜑 → ((𝐵 ∘f · 𝐺):𝐼⟶𝐶 ∧ (𝐵 ∘f · 𝐺) finSupp 0 )) | ||
Theorem | psrbagev2 20285* | Closure of a sum using a bag of multipliers. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 18-Jul-2019.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐶 = (Base‘𝑇) & ⊢ · = (.g‘𝑇) & ⊢ (𝜑 → 𝑇 ∈ CMnd) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐺:𝐼⟶𝐶) & ⊢ (𝜑 → 𝐼 ∈ V) ⇒ ⊢ (𝜑 → (𝑇 Σg (𝐵 ∘f · 𝐺)) ∈ 𝐶) | ||
Theorem | evlslem2 20286* | A linear function on the polynomial ring which is multiplicative on scaled monomials is generally multiplicative. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑆) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ V) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐸 ∈ (𝑃 GrpHom 𝑆)) & ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑗 ∈ 𝐷 ∧ 𝑖 ∈ 𝐷))) → (𝐸‘(𝑘 ∈ 𝐷 ↦ if(𝑘 = (𝑗 ∘f + 𝑖), ((𝑥‘𝑗)(.r‘𝑅)(𝑦‘𝑖)), 0 ))) = ((𝐸‘(𝑘 ∈ 𝐷 ↦ if(𝑘 = 𝑗, (𝑥‘𝑗), 0 ))) · (𝐸‘(𝑘 ∈ 𝐷 ↦ if(𝑘 = 𝑖, (𝑦‘𝑖), 0 ))))) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(.r‘𝑃)𝑦)) = ((𝐸‘𝑥) · (𝐸‘𝑦))) | ||
Theorem | evlslem3 20287* | Lemma for evlseu 20290. Polynomial evaluation of a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑇 = (mulGrp‘𝑆) & ⊢ ↑ = (.g‘𝑇) & ⊢ · = (.r‘𝑆) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) & ⊢ (𝜑 → 𝐼 ∈ V) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → 𝐺:𝐼⟶𝐶) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐻 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘f ↑ 𝐺)))) | ||
Theorem | evlslem6 20288* | Lemma for evlseu 20290. Finiteness and consistency of the top-level sum. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 26-Jul-2019.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑇 = (mulGrp‘𝑆) & ⊢ ↑ = (.g‘𝑇) & ⊢ · = (.r‘𝑆) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) & ⊢ (𝜑 → 𝐼 ∈ V) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → 𝐺:𝐼⟶𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑌‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆))) | ||
Theorem | evlslem1 20289* | Lemma for evlseu 20290, give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 26-Jul-2019.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑇 = (mulGrp‘𝑆) & ⊢ ↑ = (.g‘𝑇) & ⊢ · = (.r‘𝑆) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) & ⊢ (𝜑 → 𝐼 ∈ V) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → 𝐺:𝐼⟶𝐶) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸 ∘ 𝐴) = 𝐹 ∧ (𝐸 ∘ 𝑉) = 𝐺)) | ||
Theorem | evlseu 20290* | 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.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝑉 = (𝐼 mVar 𝑅) & ⊢ (𝜑 → 𝐼 ∈ V) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → 𝐺:𝐼⟶𝐶) ⇒ ⊢ (𝜑 → ∃!𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) | ||
Theorem | reldmevls 20291 | Well-behaved binary operation property of evalSub. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
⊢ Rel dom evalSub | ||
Theorem | mpfrcl 20292 | Reverse closure for the set of polynomial functions. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝑄 → (𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆))) | ||
Theorem | evlsval 20293* | 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 20294* | 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 20295 | 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 20296 | 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 20297* | 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 20298* | 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 20299* | 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 20300 | 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‘𝐻)(𝑄‘𝑋))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |