Home | Metamath
Proof Explorer Theorem List (p. 212 of 462) | < 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-28971) |
Hilbert Space Explorer
(28972-30494) |
Users' Mathboxes
(30495-46134) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | coe1fval3 21101* | Univariate power series coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (PwSer1‘𝑅) & ⊢ 𝐺 = (𝑦 ∈ ℕ0 ↦ (1o × {𝑦})) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐴 = (𝐹 ∘ 𝐺)) | ||
Theorem | coe1f2 21102 | Functionality of univariate power series coefficient vectors. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (PwSer1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐴:ℕ0⟶𝐾) | ||
Theorem | coe1fval2 21103* | Univariate polynomial coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (𝑦 ∈ ℕ0 ↦ (1o × {𝑦})) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐴 = (𝐹 ∘ 𝐺)) | ||
Theorem | coe1f 21104 | Functionality of univariate polynomial coefficient vectors. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐴:ℕ0⟶𝐾) | ||
Theorem | coe1fvalcl 21105 | A coefficient of a univariate polynomial over a class/ring is an element of this class/ring. (Contributed by AV, 9-Oct-2019.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0) → (𝐴‘𝑁) ∈ 𝐾) | ||
Theorem | coe1sfi 21106 | Finite support of univariate polynomial coefficient vectors. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 19-Jul-2019.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐴 finSupp 0 ) | ||
Theorem | coe1fsupp 21107* | The coefficient vector of a univariate polynomial is a finitely supported mapping from the nonnegative integers to the elements of the coefficient class/ring for the polynomial. (Contributed by AV, 3-Oct-2019.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐴 ∈ {𝑔 ∈ (𝐾 ↑m ℕ0) ∣ 𝑔 finSupp 0 }) | ||
Theorem | mptcoe1fsupp 21108* | A mapping involving coefficients of polynomials is finitely supported. (Contributed by AV, 12-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((coe1‘𝑀)‘𝑘)) finSupp 0 ) | ||
Theorem | coe1ae0 21109* | The coefficient vector of a univariate polynomial is 0 almost everywhere. (Contributed by AV, 19-Oct-2019.) |
⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐵 → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝐴‘𝑛) = 0 )) | ||
Theorem | vr1cl 21110 | The generator of a univariate polynomial algebra is contained in the base set. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵) | ||
Theorem | opsr0 21111 | Zero in the ordered power series ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → (0g‘𝑆) = (0g‘𝑂)) | ||
Theorem | opsr1 21112 | One in the ordered power series ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → (1r‘𝑆) = (1r‘𝑂)) | ||
Theorem | mplplusg 21113 | Value of addition in a polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ + = (+g‘𝑌) ⇒ ⊢ + = (+g‘𝑆) | ||
Theorem | mplmulr 21114 | Value of multiplication in a polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ · = (.r‘𝑌) ⇒ ⊢ · = (.r‘𝑆) | ||
Theorem | psr1plusg 21115 | Value of addition in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑌 = (PwSer1‘𝑅) & ⊢ 𝑆 = (1o mPwSer 𝑅) & ⊢ + = (+g‘𝑌) ⇒ ⊢ + = (+g‘𝑆) | ||
Theorem | psr1vsca 21116 | Value of scalar multiplication in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑌 = (PwSer1‘𝑅) & ⊢ 𝑆 = (1o mPwSer 𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) ⇒ ⊢ · = ( ·𝑠 ‘𝑆) | ||
Theorem | psr1mulr 21117 | Value of multiplication in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑌 = (PwSer1‘𝑅) & ⊢ 𝑆 = (1o mPwSer 𝑅) & ⊢ · = (.r‘𝑌) ⇒ ⊢ · = (.r‘𝑆) | ||
Theorem | ply1plusg 21118 | Value of addition in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝑆 = (1o mPoly 𝑅) & ⊢ + = (+g‘𝑌) ⇒ ⊢ + = (+g‘𝑆) | ||
Theorem | ply1vsca 21119 | Value of scalar multiplication in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝑆 = (1o mPoly 𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) ⇒ ⊢ · = ( ·𝑠 ‘𝑆) | ||
Theorem | ply1mulr 21120 | Value of multiplication in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝑆 = (1o mPoly 𝑅) & ⊢ · = (.r‘𝑌) ⇒ ⊢ · = (.r‘𝑆) | ||
Theorem | ressply1bas2 21121 | 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.) |
⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑊 = (PwSer1‘𝐻) & ⊢ 𝐶 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 ∩ 𝐾)) | ||
Theorem | ressply1bas 21122 | A restricted polynomial algebra has the same base set. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝑃)) | ||
Theorem | ressply1add 21123 | A restricted polynomial algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(+g‘𝑈)𝑌) = (𝑋(+g‘𝑃)𝑌)) | ||
Theorem | ressply1mul 21124 | A restricted polynomial algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(.r‘𝑈)𝑌) = (𝑋(.r‘𝑃)𝑌)) | ||
Theorem | ressply1vsca 21125 | A restricted power series algebra has the same scalar multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝑃 = (𝑆 ↾s 𝐵) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵)) → (𝑋( ·𝑠 ‘𝑈)𝑌) = (𝑋( ·𝑠 ‘𝑃)𝑌)) | ||
Theorem | subrgply1 21126 | A subring of the base ring induces a subring of polynomials. (Contributed by Mario Carneiro, 3-Jul-2015.) |
⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) ⇒ ⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝐵 ∈ (SubRing‘𝑆)) | ||
Theorem | gsumply1subr 21127 | Evaluate a group sum in a polynomial ring over a subring. (Contributed by AV, 22-Sep-2019.) (Proof shortened by AV, 31-Jan-2020.) |
⊢ 𝑆 = (Poly1‘𝑅) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝑆 Σg 𝐹) = (𝑈 Σg 𝐹)) | ||
Theorem | psrbaspropd 21128 | Property deduction for power series base set. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ (𝜑 → (Base‘𝑅) = (Base‘𝑆)) ⇒ ⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑆))) | ||
Theorem | psrplusgpropd 21129* | Property deduction for power series addition. (Contributed by Stefan O'Rear, 27-Mar-2015.) (Revised by Mario Carneiro, 3-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (+g‘(𝐼 mPwSer 𝑅)) = (+g‘(𝐼 mPwSer 𝑆))) | ||
Theorem | mplbaspropd 21130* | Property deduction for polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 19-Jul-2019.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (Base‘(𝐼 mPoly 𝑅)) = (Base‘(𝐼 mPoly 𝑆))) | ||
Theorem | psropprmul 21131 | Reversing multiplication in a ring reverses multiplication in the power series ring. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ 𝑌 = (𝐼 mPwSer 𝑅) & ⊢ 𝑆 = (oppr‘𝑅) & ⊢ 𝑍 = (𝐼 mPwSer 𝑆) & ⊢ · = (.r‘𝑌) & ⊢ ∙ = (.r‘𝑍) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 ∙ 𝐺) = (𝐺 · 𝐹)) | ||
Theorem | ply1opprmul 21132 | Reversing multiplication in a ring reverses multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝑆 = (oppr‘𝑅) & ⊢ 𝑍 = (Poly1‘𝑆) & ⊢ · = (.r‘𝑌) & ⊢ ∙ = (.r‘𝑍) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 ∙ 𝐺) = (𝐺 · 𝐹)) | ||
Theorem | 00ply1bas 21133 | Lemma for ply1basfvi 21134 and deg1fvi 24955. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ ∅ = (Base‘(Poly1‘∅)) | ||
Theorem | ply1basfvi 21134 | Protection compatibility of the univariate polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ (Base‘(Poly1‘𝑅)) = (Base‘(Poly1‘( I ‘𝑅))) | ||
Theorem | ply1plusgfvi 21135 | Protection compatibility of the univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ (+g‘(Poly1‘𝑅)) = (+g‘(Poly1‘( I ‘𝑅))) | ||
Theorem | ply1baspropd 21136* | Property deduction for univariate polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (Base‘(Poly1‘𝑅)) = (Base‘(Poly1‘𝑆))) | ||
Theorem | ply1plusgpropd 21137* | Property deduction for univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (+g‘(Poly1‘𝑅)) = (+g‘(Poly1‘𝑆))) | ||
Theorem | opsrring 21138 | Ordered power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → 𝑂 ∈ Ring) | ||
Theorem | opsrlmod 21139 | Ordered power series form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) ⇒ ⊢ (𝜑 → 𝑂 ∈ LMod) | ||
Theorem | psr1ring 21140 | Univariate power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝑆 = (PwSer1‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑆 ∈ Ring) | ||
Theorem | ply1ring 21141 | Univariate polynomials form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) | ||
Theorem | psr1lmod 21142 | Univariate power series form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑃 = (PwSer1‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) | ||
Theorem | psr1sca 21143 | Scalars of a univariate power series ring. (Contributed by Stefan O'Rear, 4-Jul-2015.) |
⊢ 𝑃 = (PwSer1‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃)) | ||
Theorem | psr1sca2 21144 | Scalars of a univariate power series ring. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Revised by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑃 = (PwSer1‘𝑅) ⇒ ⊢ ( I ‘𝑅) = (Scalar‘𝑃) | ||
Theorem | ply1lmod 21145 | Univariate polynomials form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) | ||
Theorem | ply1sca 21146 | Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝑅 = (Scalar‘𝑃)) | ||
Theorem | ply1sca2 21147 | Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ ( I ‘𝑅) = (Scalar‘𝑃) | ||
Theorem | ply1mpl0 21148 | The univariate polynomial ring has the same zero as the corresponding multivariate polynomial ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝑀 = (1o mPoly 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) ⇒ ⊢ 0 = (0g‘𝑀) | ||
Theorem | ply10s0 21149 | Zero times a univariate polynomial is the zero polynomial (lmod0vs 19904 analog.) (Contributed by AV, 2-Dec-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ ∗ = ( ·𝑠 ‘𝑃) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ( 0 ∗ 𝑀) = (0g‘𝑃)) | ||
Theorem | ply1mpl1 21150 | The univariate polynomial ring has the same one as the corresponding multivariate polynomial ring. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝑀 = (1o mPoly 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 1 = (1r‘𝑃) ⇒ ⊢ 1 = (1r‘𝑀) | ||
Theorem | ply1ascl 21151 | The univariate polynomial ring inherits the multivariate ring's scalar function. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by Fan Zheng, 26-Jun-2016.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ 𝐴 = (algSc‘(1o mPoly 𝑅)) | ||
Theorem | subrg1ascl 21152 | 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.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝐶 = (algSc‘𝑈) ⇒ ⊢ (𝜑 → 𝐶 = (𝐴 ↾ 𝑇)) | ||
Theorem | subrg1asclcl 21153 | 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.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝐵 = (Base‘𝑈) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝐵 ↔ 𝑋 ∈ 𝑇)) | ||
Theorem | subrgvr1 21154 | The variables in a subring polynomial algebra are the same as the original ring. (Contributed by Mario Carneiro, 5-Jul-2015.) |
⊢ 𝑋 = (var1‘𝑅) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) ⇒ ⊢ (𝜑 → 𝑋 = (var1‘𝐻)) | ||
Theorem | subrgvr1cl 21155 | The variables in a polynomial algebra are contained in every subring algebra. (Contributed by Mario Carneiro, 5-Jul-2015.) |
⊢ 𝑋 = (var1‘𝑅) & ⊢ (𝜑 → 𝑇 ∈ (SubRing‘𝑅)) & ⊢ 𝐻 = (𝑅 ↾s 𝑇) & ⊢ 𝑈 = (Poly1‘𝐻) & ⊢ 𝐵 = (Base‘𝑈) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐵) | ||
Theorem | coe1z 21156 | The coefficient vector of 0. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑌 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (coe1‘ 0 ) = (ℕ0 × {𝑌})) | ||
Theorem | coe1add 21157 | The coefficient vector of an addition. (Contributed by Stefan O'Rear, 24-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ ✚ = (+g‘𝑌) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (coe1‘(𝐹 ✚ 𝐺)) = ((coe1‘𝐹) ∘f + (coe1‘𝐺))) | ||
Theorem | coe1addfv 21158 | A particular coefficient of an addition. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ ✚ = (+g‘𝑌) & ⊢ + = (+g‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) → ((coe1‘(𝐹 ✚ 𝐺))‘𝑋) = (((coe1‘𝐹)‘𝑋) + ((coe1‘𝐺)‘𝑋))) | ||
Theorem | coe1subfv 21159 | A particular coefficient of a subtraction. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 𝑁 = (-g‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑋 ∈ ℕ0) → ((coe1‘(𝐹 − 𝐺))‘𝑋) = (((coe1‘𝐹)‘𝑋)𝑁((coe1‘𝐺)‘𝑋))) | ||
Theorem | coe1mul2lem1 21160 | An equivalence for coe1mul2 21162. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑋 ∈ (ℕ0 ↑m 1o)) → (𝑋 ∘r ≤ (1o × {𝐴}) ↔ (𝑋‘∅) ∈ (0...𝐴))) | ||
Theorem | coe1mul2lem2 21161* | An equivalence for coe1mul2 21162. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝐻 = {𝑑 ∈ (ℕ0 ↑m 1o) ∣ 𝑑 ∘r ≤ (1o × {𝑘})} ⇒ ⊢ (𝑘 ∈ ℕ0 → (𝑐 ∈ 𝐻 ↦ (𝑐‘∅)):𝐻–1-1-onto→(0...𝑘)) | ||
Theorem | coe1mul2 21162* | 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 21163* | 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 21164 | Closure of the expression for a univariate primitive monomial. (Contributed by AV, 14-Aug-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐷 ∈ ℕ0) → (𝐷 ↑ 𝑋) ∈ 𝐵) | ||
Theorem | ply1tmcl 21165 | 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 21166* | 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 21167 | 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 21168 | 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 21169* | 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 21170* | 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 21171 | 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 21172* | 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 21173 | 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 21174 | 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 21175 | 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 21176 | 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 21177 | 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 21178 | A scalar polynomial is a polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → 𝐴:𝐾⟶𝐵) | ||
Theorem | ply1sclcl 21179 | 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 21180* | 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 21181 | Recover the base scalar from a scalar polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾) → 𝑋 = ((coe1‘(𝐴‘𝑋))‘0)) | ||
Theorem | ply1sclf1 21182 | The polynomial scalar function is injective. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → 𝐴:𝐾–1-1→𝐵) | ||
Theorem | ply1scl0 21183 | The zero scalar is zero. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑌 = (0g‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → (𝐴‘ 0 ) = 𝑌) | ||
Theorem | ply1scln0 21184 | Nonzero scalars create nonzero polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑌 = (0g‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → (𝐴‘𝑋) ≠ 𝑌) | ||
Theorem | ply1scl1 21185 | The one scalar is the unit polynomial. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (1r‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → (𝐴‘ 1 ) = 𝑁) | ||
Theorem | ply1idvr1 21186 | 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 21187* | 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 21188* | The decomposition of a univariate polynomial is finitely supported. Formerly part of proof for ply1coe 21189. (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 21189* | 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 21190* | 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 21191* | 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 21192* | 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 21193* | 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 21194* | Lemma for coe1fzgsumd 21195 (induction step). (Contributed by AV, 8-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾)))))) | ||
Theorem | coe1fzgsumd 21195* | 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 21196* | 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 21197* | 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 21198* | 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 21199* | 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 21200* | 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𝑘) · ((𝑆‘((𝑁 − 𝑘)𝐸𝐴)) × (𝑘 ↑ 𝑋)))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |