![]() |
Metamath
Proof Explorer Theorem List (p. 222 of 481) | < 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-30595) |
![]() (30596-32118) |
![]() (32119-48006) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | coe1mul2 22101* | The coefficient vector of multiplication in the univariate power series ring. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝑆 = (PwSer1‘𝑅) & ⊢ ∙ = (.r‘𝑆) & ⊢ · = (.r‘𝑅) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (coe1‘(𝐹 ∙ 𝐺)) = (𝑘 ∈ ℕ0 ↦ (𝑅 Σg (𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) · ((coe1‘𝐺)‘(𝑘 − 𝑥))))))) | ||
Theorem | coe1mul 22102* | The coefficient vector of multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ ∙ = (.r‘𝑌) & ⊢ · = (.r‘𝑅) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (coe1‘(𝐹 ∙ 𝐺)) = (𝑘 ∈ ℕ0 ↦ (𝑅 Σg (𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) · ((coe1‘𝐺)‘(𝑘 − 𝑥))))))) | ||
Theorem | ply1moncl 22103 | Closure of the expression for a univariate primitive monomial. (Contributed by AV, 14-Aug-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐷 ∈ ℕ0) → (𝐷 ↑ 𝑋) ∈ 𝐵) | ||
Theorem | ply1tmcl 22104 | Closure of the expression for a univariate polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 25-Nov-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝐷 ↑ 𝑋)) ∈ 𝐵) | ||
Theorem | coe1tm 22105* | Coefficient vector of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ 0 = (0g‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (coe1‘(𝐶 · (𝐷 ↑ 𝑋))) = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 𝐷, 𝐶, 0 ))) | ||
Theorem | coe1tmfv1 22106 | Nonzero coefficient of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ 0 = (0g‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝐷) = 𝐶) | ||
Theorem | coe1tmfv2 22107 | 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 22108* | 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 22109* | 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 22110 | 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 22111* | 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 22112 | 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 22113 | 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 22114 | 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 22115 | 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 22116 | 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 22117 | A scalar polynomial is a polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → 𝐴:𝐾⟶𝐵) | ||
Theorem | ply1sclcl 22118 | 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 22119* | 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 22120 | Recover the base scalar from a scalar polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾) → 𝑋 = ((coe1‘(𝐴‘𝑋))‘0)) | ||
Theorem | ply1sclf1 22121 | The polynomial scalar function is injective. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → 𝐴:𝐾–1-1→𝐵) | ||
Theorem | ply1scl0 22122 | The zero scalar is zero. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑌 = (0g‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → (𝐴‘ 0 ) = 𝑌) | ||
Theorem | ply1scl0OLD 22123 | Obsolete version of ply1scl1 22125 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 22124 | Nonzero scalars create nonzero polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑌 = (0g‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → (𝐴‘𝑋) ≠ 𝑌) | ||
Theorem | ply1scl1 22125 | 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 22126 | Obsolete version of ply1scl1 22125 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 22127 | 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 22128* | 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 22129* | The decomposition of a univariate polynomial is finitely supported. Formerly part of proof for ply1coe 22130. (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 22130* | 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 22131* | 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 22132* | 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 22133* | 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 22134* | 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 22135* | Lemma for coe1fzgsumd 22136 (induction step). (Contributed by AV, 8-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾)))))) | ||
Theorem | coe1fzgsumd 22136* | Value of an evaluated coefficient in a finite group sum of polynomials. (Contributed by AV, 8-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑁 𝑀 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ Fin) ⇒ ⊢ (𝜑 → ((coe1‘(𝑃 Σg (𝑥 ∈ 𝑁 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑁 ↦ ((coe1‘𝑀)‘𝐾)))) | ||
Theorem | gsumsmonply1 22137* | 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 22138* | 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 22139* | 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 22140* | 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 22141* | 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𝑘) · ((𝑆‘((𝑁 − 𝑘)𝐸𝐴)) × (𝑘 ↑ 𝑋)))))) | ||
Syntax | ces1 22142 | Evaluation of a univariate polynomial in a subring. |
class evalSub1 | ||
Syntax | ce1 22143 | Evaluation of a univariate polynomial. |
class eval1 | ||
Definition | df-evls1 22144* | 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 22145* | 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 22146 | Well-behaved binary operation property of evalSub1. (Contributed by AV, 7-Sep-2019.) |
⊢ Rel dom evalSub1 | ||
Theorem | ply1frcl 22147 | Reverse closure for the set of univariate polynomial functions. (Contributed by AV, 9-Sep-2019.) |
⊢ 𝑄 = ran (𝑆 evalSub1 𝑅) ⇒ ⊢ (𝑋 ∈ 𝑄 → (𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 (Base‘𝑆))) | ||
Theorem | evls1fval 22148* | Value of the univariate polynomial evaluation map function. (Contributed by AV, 7-Sep-2019.) |
⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝐸 = (1o evalSub 𝑆) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑄 = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅))) | ||
Theorem | evls1val 22149* | 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 22150* | Lemma for evl1rhm 22161 and evls1rhm 22151 (formerly part of the proof of evl1rhm 22161): 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 22151 | 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 22152 | Univariate polynomial evaluation maps scalars to constant functions. (Contributed by AV, 8-Sep-2019.) |
⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) ⇒ ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = (𝐵 × {𝑋})) | ||
Theorem | evls1gsumadd 22153* | 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 22154* | 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 22155 | 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 22156 | 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 22157* | 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 22158* | 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 22159 | Lemma for evl1fval1 22160. (Contributed by AV, 11-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝑄 = (𝑅 evalSub1 𝐵)) | ||
Theorem | evl1fval1 22160 | Value of the simple/same ring evaluation map function for univariate polynomials. (Contributed by AV, 11-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝑄 = (𝑅 evalSub1 𝐵) | ||
Theorem | evl1rhm 22161 | 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 22162 | 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 22163 | Polynomial evaluation maps scalars to constant functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝑂‘(𝐴‘𝑋)) = (𝐵 × {𝑋})) | ||
Theorem | evl1scad 22164 | Polynomial evaluation builder for scalars. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝑈 ∧ ((𝑂‘(𝐴‘𝑋))‘𝑌) = 𝑋)) | ||
Theorem | evl1var 22165 | Polynomial evaluation maps the variable to the identity function. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → (𝑂‘𝑋) = ( I ↾ 𝐵)) | ||
Theorem | evl1vard 22166 | Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ∧ ((𝑂‘𝑋)‘𝑌) = 𝑌)) | ||
Theorem | evls1var 22167 | 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 22168 | 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 22169 | 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 22170 | Polynomial evaluation builder for addition of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊)) & ⊢ ✚ = (+g‘𝑃) & ⊢ + = (+g‘𝑅) ⇒ ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 ✚ 𝑁))‘𝑌) = (𝑉 + 𝑊))) | ||
Theorem | evl1subd 22171 | Polynomial evaluation builder for subtraction of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊)) & ⊢ − = (-g‘𝑃) & ⊢ 𝐷 = (-g‘𝑅) ⇒ ⊢ (𝜑 → ((𝑀 − 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 − 𝑁))‘𝑌) = (𝑉𝐷𝑊))) | ||
Theorem | evl1muld 22172 | Polynomial evaluation builder for multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊)) & ⊢ ∙ = (.r‘𝑃) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 ∙ 𝑁))‘𝑌) = (𝑉 · 𝑊))) | ||
Theorem | evl1vsd 22173 | Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → 𝑁 ∈ 𝐵) & ⊢ ∙ = ( ·𝑠 ‘𝑃) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝑈 ∧ ((𝑂‘(𝑁 ∙ 𝑀))‘𝑌) = (𝑁 · 𝑉))) | ||
Theorem | evl1expd 22174 | 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 22175 | Constants are polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐵 × {𝑋}) ∈ 𝑄) | ||
Theorem | pf1id 22176 | The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → ( I ↾ 𝐵) ∈ 𝑄) | ||
Theorem | pf1subrg 22177 | 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 22178 | Reverse closure for the set of polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝑄 → 𝑅 ∈ CRing) | ||
Theorem | pf1f 22179 | Polynomial functions are functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑄 → 𝐹:𝐵⟶𝐵) | ||
Theorem | mpfpf1 22180* | Convert a multivariate polynomial function to univariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = ran (1o eval 𝑅) ⇒ ⊢ (𝐹 ∈ 𝐸 → (𝐹 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))) ∈ 𝑄) | ||
Theorem | pf1mpf 22181* | Convert a univariate polynomial function to multivariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = ran (1o eval 𝑅) ⇒ ⊢ (𝐹 ∈ 𝑄 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦ (𝑥‘∅))) ∈ 𝐸) | ||
Theorem | pf1addcl 22182 | The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f + 𝐺) ∈ 𝑄) | ||
Theorem | pf1mulcl 22183 | The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f · 𝐺) ∈ 𝑄) | ||
Theorem | pf1ind 22184* | 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 22185* | Lemma for evl1gsumd 22186 (induction step). (Contributed by AV, 17-Sep-2019.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌)))))) | ||
Theorem | evl1gsumd 22186* | 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 22187* | 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 22153. (Contributed by AV, 15-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝑃 = (𝑅 ↑s 𝐾) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ⊆ ℕ0) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌)))) | ||
Theorem | evl1gsumaddval 22188* | 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 22189* | 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 22190 | Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd 22187, the proof is shorter using evls1varpw 22156 instead of proving it directly. (Contributed by AV, 15-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑊) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘(mulGrp‘(𝑅 ↑s 𝐵)))(𝑄‘𝑋))) | ||
Theorem | evl1varpwval 22191 | 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 22192 | 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 22193 | 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 22194* | 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 (𝑥 ∈ 𝑀 ↦ (𝐴 · (𝑁𝐸𝐶))))) | ||
According to Wikipedia ("Matrix (mathemetics)", 02-Apr-2019, https://en.wikipedia.org/wiki/Matrix_(mathematics)) "A matrix is a rectangular array of numbers or other mathematical objects for which operations such as addition and multiplication are defined. Most commonly, a matrix over a field F is a rectangular array of scalars each of which is a member of F. The numbers, symbols or expressions in the matrix are called its entries or its elements. The horizontal and vertical lines of entries in a matrix are called rows and columns, respectively.", and in the definition of [Lang] p. 503 "By an m x n matrix in [a commutative ring] R one means a doubly indexed family of elements of R, (aij), (i= 1,..., m and j = 1,... n) ... We call the elements aij the coefficients or components of the matrix. A 1 x n matrix is called a row vector (of dimension, or size, n) and a m x 1 matrix is called a column vector (of dimension, or size, m). In general, we say that (m,n) is the size of the matrix, ...". In contrast to these definitions, we denote any free module over a (not necessarily commutative) ring (in the meaning of df-frlm 21602) with a Cartesian product as index set as "matrix". The two sets of the Cartesian product even need neither to be ordered or a range of (nonnegative/positive) integers nor finite. By this, the addition and scalar multiplication for matrices correspond to the addition (see frlmplusgval 21619) and scalar multiplication (see frlmvscafval 21621) for free modules. Actually, there is no definition for (arbitrary) matrices: Even the (general) matrix multiplication can be defined using functions from Cartesian products into a ring (which are elements of the base set of free modules), see df-mamu 22196. Thus, a statement like "Then the set of m x n matrices in R is a module (i.e., an R-module)" as in [Lang] p. 504 follows immediately from frlmlmod 21604. However, for square matrices there is Definition df-mat 22218, defining the algebras of square matrices (of the same size over the same ring), extending the structure of the corresponding free module by the matrix multiplication as ring multiplication. A "usual" matrix (aij), (i = 1,..., m and j = 1,... n) would be represented as an element of (the base set of) (𝑅 freeLMod ((1...𝑚) × (1...𝑛))) and a square matrix (aij), (i = 1,..., n and j = 1,... n) would be represented as an element of (the base set of) ((1...𝑛) Mat 𝑅). Finally, it should be mentioned that our definitions of matrices include the zero-dimensional cases, which are excluded from the definitions of many authors, e.g., in [Lang] p. 503. It is shown in mat0dimbas0 22278 that the empty set is the sole zero-dimensional matrix (also called "empty matrix", see Wikipedia https://en.wikipedia.org/wiki/Matrix_(mathematics)#Empty_matrices). 22278 Its determinant is the ring unity, see mdet0fv0 22406. | ||
This section is about the multiplication of m x n matrices. | ||
Syntax | cmmul 22195 | Syntax for the matrix multiplication operator. |
class maMul | ||
Definition | df-mamu 22196* | The operator which multiplies an m x n matrix with an n x p matrix, see also the definition in [Lang] p. 504. Note that it is not generally possible to recover the dimensions from the matrix, since all n x 0 and all 0 x n matrices are represented by the empty set. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ maMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ ⦋(1st ‘(1st ‘𝑜)) / 𝑚⦌⦋(2nd ‘(1st ‘𝑜)) / 𝑛⦌⦋(2nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))))) | ||
Theorem | mamufval 22197* | Functional value of the matrix multiplication operator. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑃〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ Fin) ⇒ ⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))))) | ||
Theorem | mamuval 22198* | Multiplication of two matrices. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑃〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃))) ⇒ ⊢ (𝜑 → (𝑋𝐹𝑌) = (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑌𝑘)))))) | ||
Theorem | mamufv 22199* | A cell in the multiplication of two matrices. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑃〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃))) & ⊢ (𝜑 → 𝐼 ∈ 𝑀) & ⊢ (𝜑 → 𝐾 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐼(𝑋𝐹𝑌)𝐾) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝐼𝑋𝑗) · (𝑗𝑌𝐾))))) | ||
Theorem | mamudm 22200 | The domain of the matrix multiplication function. (Contributed by AV, 10-Feb-2019.) |
⊢ 𝐸 = (𝑅 freeLMod (𝑀 × 𝑁)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐹 = (𝑅 freeLMod (𝑁 × 𝑃)) & ⊢ 𝐶 = (Base‘𝐹) & ⊢ × = (𝑅 maMul 〈𝑀, 𝑁, 𝑃〉) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin)) → dom × = (𝐵 × 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |