![]() |
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-30748) |
![]() (30749-32271) |
![]() (32272-48316) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | coe1tmfv2 22201 | Zero coefficient of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ 0 = (0g‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → 𝐹 ∈ ℕ0) & ⊢ (𝜑 → 𝐷 ≠ 𝐹) ⇒ ⊢ (𝜑 → ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝐹) = 0 ) | ||
Theorem | coe1tmmul2 22202* | Coefficient vector of a polynomial multiplied on the right by a term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ 0 = (0g‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ × = (.r‘𝑅) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) ⇒ ⊢ (𝜑 → (coe1‘(𝐴 ∙ (𝐶 · (𝐷 ↑ 𝑋)))) = (𝑥 ∈ ℕ0 ↦ if(𝐷 ≤ 𝑥, (((coe1‘𝐴)‘(𝑥 − 𝐷)) × 𝐶), 0 ))) | ||
Theorem | coe1tmmul 22203* | Coefficient vector of a polynomial multiplied on the left by a term. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 0 = (0g‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ × = (.r‘𝑅) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) ⇒ ⊢ (𝜑 → (coe1‘((𝐶 · (𝐷 ↑ 𝑋)) ∙ 𝐴)) = (𝑥 ∈ ℕ0 ↦ if(𝐷 ≤ 𝑥, (𝐶 × ((coe1‘𝐴)‘(𝑥 − 𝐷))), 0 ))) | ||
Theorem | coe1tmmul2fv 22204 | 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 22205* | 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 22206 | 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 22207 | 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 22208 | 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 22209 | 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 22210 | 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 22211 | A scalar polynomial is a polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → 𝐴:𝐾⟶𝐵) | ||
Theorem | ply1sclcl 22212 | 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 22213* | 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 22214 | Recover the base scalar from a scalar polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾) → 𝑋 = ((coe1‘(𝐴‘𝑋))‘0)) | ||
Theorem | ply1sclf1 22215 | The polynomial scalar function is injective. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → 𝐴:𝐾–1-1→𝐵) | ||
Theorem | ply1scl0 22216 | The zero scalar is zero. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑌 = (0g‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → (𝐴‘ 0 ) = 𝑌) | ||
Theorem | ply1scl0OLD 22217 | Obsolete version of ply1scl1 22219 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 22218 | Nonzero scalars create nonzero polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑌 = (0g‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → (𝐴‘𝑋) ≠ 𝑌) | ||
Theorem | ply1scl1 22219 | 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 22220 | Obsolete version of ply1scl1 22219 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 22221 | 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 22222* | 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 22223* | The decomposition of a univariate polynomial is finitely supported. Formerly part of proof for ply1coe 22224. (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 22224* | 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 22225* | 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 22226* | 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 22227* | 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 22228* | 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 22229* | Lemma for coe1fzgsumd 22230 (induction step). (Contributed by AV, 8-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾)))))) | ||
Theorem | coe1fzgsumd 22230* | 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 22231 | 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 22232 | 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 22233* | 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 22234* | 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 22235* | 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 22236* | 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 22237* | 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 22238 | 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 22239 | Evaluation of a univariate polynomial in a subring. |
class evalSub1 | ||
Syntax | ce1 22240 | Evaluation of a univariate polynomial. |
class eval1 | ||
Definition | df-evls1 22241* | 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 22242* | 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 22243 | Well-behaved binary operation property of evalSub1. (Contributed by AV, 7-Sep-2019.) |
⊢ Rel dom evalSub1 | ||
Theorem | ply1frcl 22244 | Reverse closure for the set of univariate polynomial functions. (Contributed by AV, 9-Sep-2019.) |
⊢ 𝑄 = ran (𝑆 evalSub1 𝑅) ⇒ ⊢ (𝑋 ∈ 𝑄 → (𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 (Base‘𝑆))) | ||
Theorem | evls1fval 22245* | Value of the univariate polynomial evaluation map function. (Contributed by AV, 7-Sep-2019.) |
⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝐸 = (1o evalSub 𝑆) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑄 = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅))) | ||
Theorem | evls1val 22246* | 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 22247* | Lemma for evl1rhm 22258 and evls1rhm 22248 (formerly part of the proof of evl1rhm 22258): 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 22248 | 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 22249 | Univariate polynomial evaluation maps scalars to constant functions. (Contributed by AV, 8-Sep-2019.) |
⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) ⇒ ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = (𝐵 × {𝑋})) | ||
Theorem | evls1gsumadd 22250* | 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 22251* | 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 22252 | 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 22253 | 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 22254* | 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 22255* | 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 22256 | Lemma for evl1fval1 22257. (Contributed by AV, 11-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝑄 = (𝑅 evalSub1 𝐵)) | ||
Theorem | evl1fval1 22257 | Value of the simple/same ring evaluation map function for univariate polynomials. (Contributed by AV, 11-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝑄 = (𝑅 evalSub1 𝐵) | ||
Theorem | evl1rhm 22258 | 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 22259 | 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 22260 | Polynomial evaluation maps scalars to constant functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝑂‘(𝐴‘𝑋)) = (𝐵 × {𝑋})) | ||
Theorem | evl1scad 22261 | Polynomial evaluation builder for scalars. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝑈 ∧ ((𝑂‘(𝐴‘𝑋))‘𝑌) = 𝑋)) | ||
Theorem | evl1var 22262 | Polynomial evaluation maps the variable to the identity function. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → (𝑂‘𝑋) = ( I ↾ 𝐵)) | ||
Theorem | evl1vard 22263 | Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ∧ ((𝑂‘𝑋)‘𝑌) = 𝑌)) | ||
Theorem | evls1var 22264 | 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 22265 | 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 22266 | 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 22267 | Polynomial evaluation builder for addition of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊)) & ⊢ ✚ = (+g‘𝑃) & ⊢ + = (+g‘𝑅) ⇒ ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 ✚ 𝑁))‘𝑌) = (𝑉 + 𝑊))) | ||
Theorem | evl1subd 22268 | Polynomial evaluation builder for subtraction of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊)) & ⊢ − = (-g‘𝑃) & ⊢ 𝐷 = (-g‘𝑅) ⇒ ⊢ (𝜑 → ((𝑀 − 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 − 𝑁))‘𝑌) = (𝑉𝐷𝑊))) | ||
Theorem | evl1muld 22269 | Polynomial evaluation builder for multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊)) & ⊢ ∙ = (.r‘𝑃) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 ∙ 𝑁))‘𝑌) = (𝑉 · 𝑊))) | ||
Theorem | evl1vsd 22270 | Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → 𝑁 ∈ 𝐵) & ⊢ ∙ = ( ·𝑠 ‘𝑃) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝑈 ∧ ((𝑂‘(𝑁 ∙ 𝑀))‘𝑌) = (𝑁 · 𝑉))) | ||
Theorem | evl1expd 22271 | 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 22272 | Constants are polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐵 × {𝑋}) ∈ 𝑄) | ||
Theorem | pf1id 22273 | The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → ( I ↾ 𝐵) ∈ 𝑄) | ||
Theorem | pf1subrg 22274 | 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 22275 | Reverse closure for the set of polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝑄 → 𝑅 ∈ CRing) | ||
Theorem | pf1f 22276 | Polynomial functions are functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑄 → 𝐹:𝐵⟶𝐵) | ||
Theorem | mpfpf1 22277* | Convert a multivariate polynomial function to univariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = ran (1o eval 𝑅) ⇒ ⊢ (𝐹 ∈ 𝐸 → (𝐹 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))) ∈ 𝑄) | ||
Theorem | pf1mpf 22278* | Convert a univariate polynomial function to multivariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = ran (1o eval 𝑅) ⇒ ⊢ (𝐹 ∈ 𝑄 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦ (𝑥‘∅))) ∈ 𝐸) | ||
Theorem | pf1addcl 22279 | The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f + 𝐺) ∈ 𝑄) | ||
Theorem | pf1mulcl 22280 | The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f · 𝐺) ∈ 𝑄) | ||
Theorem | pf1ind 22281* | 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 22282* | Lemma for evl1gsumd 22283 (induction step). (Contributed by AV, 17-Sep-2019.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌)))))) | ||
Theorem | evl1gsumd 22283* | 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 22284* | 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 22250. (Contributed by AV, 15-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝑃 = (𝑅 ↑s 𝐾) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ⊆ ℕ0) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌)))) | ||
Theorem | evl1gsumaddval 22285* | 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 22286* | 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 22287 | Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd 22284, the proof is shorter using evls1varpw 22253 instead of proving it directly. (Contributed by AV, 15-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑊) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘(mulGrp‘(𝑅 ↑s 𝐵)))(𝑄‘𝑋))) | ||
Theorem | evl1varpwval 22288 | 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 22289 | 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 22290 | 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 22291* | 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 22292 | Value of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑄‘(𝐴‘𝑋))‘𝐶) = 𝑋) | ||
Theorem | evls1expd 22293 | Univariate polynomial evaluation builder for an exponential. See also evl1expd 22271. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ ∧ = (.g‘(mulGrp‘𝑊)) & ⊢ ↑ = (.g‘(mulGrp‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑄‘(𝑁 ∧ 𝑀))‘𝐶) = (𝑁 ↑ ((𝑄‘𝑀)‘𝐶))) | ||
Theorem | evls1varpwval 22294 | Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. See evl1varpwval 22288. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑋 = (var1‘𝑈) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ ∧ = (.g‘(mulGrp‘𝑊)) & ⊢ ↑ = (.g‘(mulGrp‘𝑆)) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑄‘(𝑁 ∧ 𝑋))‘𝐶) = (𝑁 ↑ 𝐶)) | ||
Theorem | evls1fpws 22295* | 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 22296 | 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 22297 | 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 22298 | 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 22299 | 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 22300 | 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‘𝑅)) & ⊢ (𝜑 → 𝑍 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴‘𝑍) ∈ 𝑃) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |