| Metamath
Proof Explorer Theorem List (p. 262 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mdegfval 26101* | Value of the multivariate degree function. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
| ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ)) ⇒ ⊢ 𝐷 = (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*, < )) | ||
| Theorem | mdegval 26102* | Value of the multivariate degree function at some particular polynomial. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
| ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ)) ⇒ ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) = sup((𝐻 “ (𝐹 supp 0 )), ℝ*, < )) | ||
| Theorem | mdegleb 26103* | Property of being of limited degree. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
| ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ)) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) | ||
| Theorem | mdeglt 26104* | If there is an upper limit on the degree of a polynomial that is lower than the degree of some exponent bag, then that exponent bag is unrepresented in the polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
| ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → (𝐷‘𝐹) < (𝐻‘𝑋)) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) = 0 ) | ||
| Theorem | mdegldg 26105* | A nonzero polynomial has some coefficient which witnesses its degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ)) & ⊢ 𝑌 = (0g‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 0 ∧ (𝐻‘𝑥) = (𝐷‘𝐹))) | ||
| Theorem | mdegxrcl 26106 | Closure of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
| ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ ℝ*) | ||
| Theorem | mdegxrf 26107 | Functionality of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
| ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ 𝐷:𝐵⟶ℝ* | ||
| Theorem | mdegcl 26108 | Sharp closure for multivariate polynomials. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ (ℕ0 ∪ {-∞})) | ||
| Theorem | mdeg0 26109 | Degree of the zero polynomial. (Contributed by Stefan O'Rear, 20-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
| ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 0 = (0g‘𝑃) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → (𝐷‘ 0 ) = -∞) | ||
| Theorem | mdegnn0cl 26110 | Degree of a nonzero polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐷‘𝐹) ∈ ℕ0) | ||
| Theorem | degltlem1 26111 | Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ ((𝑋 ∈ (ℕ0 ∪ {-∞}) ∧ 𝑌 ∈ ℤ) → (𝑋 < 𝑌 ↔ 𝑋 ≤ (𝑌 − 1))) | ||
| Theorem | degltp1le 26112 | Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
| ⊢ ((𝑋 ∈ (ℕ0 ∪ {-∞}) ∧ 𝑌 ∈ ℤ) → (𝑋 < (𝑌 + 1) ↔ 𝑋 ≤ 𝑌)) | ||
| Theorem | mdegaddle 26113 | The degree of a sum is at most the maximum of the degrees of the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
| ⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) | ||
| Theorem | mdegvscale 26114 | The degree of a scalar multiple of a polynomial is at most the degree of the original polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
| ⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐷‘𝐺)) | ||
| Theorem | mdegvsca 26115 | The degree of a scalar multiple of a polynomial is exactly the degree of the original polynomial when the multiple is a nonzero-divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
| ⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐸) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) = (𝐷‘𝐺)) | ||
| Theorem | mdegle0 26116 | A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
| ⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐴 = (algSc‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐷‘𝐹) ≤ 0 ↔ 𝐹 = (𝐴‘(𝐹‘(𝐼 × {0}))))) | ||
| Theorem | mdegmullem 26117* | Lemma for mdegmulle2 26118. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
| ⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = (.r‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐽) & ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐾) & ⊢ 𝐴 = {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (𝑏 ∈ 𝐴 ↦ (ℂfld Σg 𝑏)) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾)) | ||
| Theorem | mdegmulle2 26118 | The multivariate degree of a product of polynomials is at most the sum of the degrees of the polynomials. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
| ⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = (.r‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐽) & ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐾) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾)) | ||
| Theorem | deg1fval 26119 | Relate univariate polynomial degree to multivariate. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 7-Oct-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) ⇒ ⊢ 𝐷 = (1o mDeg 𝑅) | ||
| Theorem | deg1xrf 26120 | Functionality of univariate polynomial degree, weak range. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ 𝐷:𝐵⟶ℝ* | ||
| Theorem | deg1xrcl 26121 | Closure of univariate polynomial degree in extended reals. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ ℝ*) | ||
| Theorem | deg1cl 26122 | Sharp closure of univariate polynomial degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ (ℕ0 ∪ {-∞})) | ||
| Theorem | mdegpropd 26123* | Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (𝐼 mDeg 𝑅) = (𝐼 mDeg 𝑆)) | ||
| Theorem | deg1fvi 26124 | Univariate polynomial degree respects protection. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ (deg1‘𝑅) = (deg1‘( I ‘𝑅)) | ||
| Theorem | deg1propd 26125* | Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (deg1‘𝑅) = (deg1‘𝑆)) | ||
| Theorem | deg1z 26126 | Degree of the zero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → (𝐷‘ 0 ) = -∞) | ||
| Theorem | deg1nn0cl 26127 | Degree of a nonzero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 7-Oct-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐷‘𝐹) ∈ ℕ0) | ||
| Theorem | deg1n0ima 26128 | Degree image of a set of polynomials which does not include zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → (𝐷 “ (𝐵 ∖ { 0 })) ⊆ ℕ0) | ||
| Theorem | deg1nn0clb 26129 | A polynomial is nonzero iff it has definite degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵) → (𝐹 ≠ 0 ↔ (𝐷‘𝐹) ∈ ℕ0)) | ||
| Theorem | deg1lt0 26130 | A polynomial is zero iff it has negative degree. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵) → ((𝐷‘𝐹) < 0 ↔ 𝐹 = 0 )) | ||
| Theorem | deg1ldg 26131 | A nonzero univariate polynomial always has a nonzero leading coefficient. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑌 = (0g‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐴‘(𝐷‘𝐹)) ≠ 𝑌) | ||
| Theorem | deg1ldgn 26132 | An index at which a polynomial is zero, cannot be its degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑌 = (0g‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℕ0) & ⊢ (𝜑 → (𝐴‘𝑋) = 𝑌) ⇒ ⊢ (𝜑 → (𝐷‘𝐹) ≠ 𝑋) | ||
| Theorem | deg1ldgdomn 26133 | A nonzero univariate polynomial over a domain always has a nonzero-divisor leading coefficient. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ ((𝑅 ∈ Domn ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐴‘(𝐷‘𝐹)) ∈ 𝐸) | ||
| Theorem | deg1leb 26134* | Property of being of limited degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ ∀𝑥 ∈ ℕ0 (𝐺 < 𝑥 → (𝐴‘𝑥) = 0 ))) | ||
| Theorem | deg1val 26135 | Value of the univariate degree as a supremum. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Jul-2019.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) = sup((𝐴 supp 0 ), ℝ*, < )) | ||
| Theorem | deg1lt 26136 | If the degree of a univariate polynomial is less than some index, then that coefficient must be zero. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ (𝐷‘𝐹) < 𝐺) → (𝐴‘𝐺) = 0 ) | ||
| Theorem | deg1ge 26137 | Conversely, a nonzero coefficient sets a lower bound on the degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ (𝐴‘𝐺) ≠ 0 ) → 𝐺 ≤ (𝐷‘𝐹)) | ||
| Theorem | coe1mul3 26138 | The coefficient vector of multiplication in the univariate polynomial ring, at indices high enough that at most one component can be active in the sum. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
| ⊢ 𝑌 = (Poly1‘𝑅) & ⊢ ∙ = (.r‘𝑌) & ⊢ · = (.r‘𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐼) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐽) ⇒ ⊢ (𝜑 → ((coe1‘(𝐹 ∙ 𝐺))‘(𝐼 + 𝐽)) = (((coe1‘𝐹)‘𝐼) · ((coe1‘𝐺)‘𝐽))) | ||
| Theorem | coe1mul4 26139 | Value of the "leading" coefficient of a product of two nonzero polynomials. This will fail to actually be the leading coefficient only if it is zero (requiring the basic ring to contain zero divisors). (Contributed by Stefan O'Rear, 25-Mar-2015.) |
| ⊢ 𝑌 = (Poly1‘𝑅) & ⊢ ∙ = (.r‘𝑌) & ⊢ · = (.r‘𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 0 = (0g‘𝑌) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ≠ 0 ) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ≠ 0 ) ⇒ ⊢ (𝜑 → ((coe1‘(𝐹 ∙ 𝐺))‘((𝐷‘𝐹) + (𝐷‘𝐺))) = (((coe1‘𝐹)‘(𝐷‘𝐹)) · ((coe1‘𝐺)‘(𝐷‘𝐺)))) | ||
| Theorem | deg1addle 26140 | The degree of a sum is at most the maximum of the degrees of the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
| ⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) | ||
| Theorem | deg1addle2 26141 | If both factors have degree bounded by 𝐿, then the sum of the polynomials also has degree bounded by 𝐿. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
| ⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐿 ∈ ℝ*) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐿) & ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐿) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) ≤ 𝐿) | ||
| Theorem | deg1add 26142 | Exact degree of a sum of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → (𝐷‘𝐺) < (𝐷‘𝐹)) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) = (𝐷‘𝐹)) | ||
| Theorem | deg1vscale 26143 | The degree of a scalar times a polynomial is at most the degree of the original polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
| ⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐷‘𝐺)) | ||
| Theorem | deg1vsca 26144 | The degree of a scalar times a polynomial is exactly the degree of the original polynomial when the scalar is not a zero divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐸) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) = (𝐷‘𝐺)) | ||
| Theorem | deg1invg 26145 | The degree of the negated polynomial is the same as the original. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑁 = (invg‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝑁‘𝐹)) = (𝐷‘𝐹)) | ||
| Theorem | deg1suble 26146 | The degree of a difference of polynomials is bounded by the maximum of degrees. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
| ⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 − 𝐺)) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) | ||
| Theorem | deg1sub 26147 | Exact degree of a difference of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → (𝐷‘𝐺) < (𝐷‘𝐹)) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 − 𝐺)) = (𝐷‘𝐹)) | ||
| Theorem | deg1mulle2 26148 | Produce a bound on the product of two univariate polynomials given bounds on the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
| ⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = (.r‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐽) & ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐾) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾)) | ||
| Theorem | deg1sublt 26149 | Subtraction of two polynomials limited to the same degree with the same leading coefficient gives a polynomial with a smaller degree. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ (𝜑 → 𝐿 ∈ ℕ0) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐿) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐿) & ⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐶 = (coe1‘𝐺) & ⊢ (𝜑 → ((coe1‘𝐹)‘𝐿) = ((coe1‘𝐺)‘𝐿)) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 − 𝐺)) < 𝐿) | ||
| Theorem | deg1le0 26150 | A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵) → ((𝐷‘𝐹) ≤ 0 ↔ 𝐹 = (𝐴‘((coe1‘𝐹)‘0)))) | ||
| Theorem | deg1sclle 26151 | A scalar polynomial has nonpositive degree. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾) → (𝐷‘(𝐴‘𝐹)) ≤ 0) | ||
| Theorem | deg1scl 26152 | A nonzero scalar polynomial has zero degree. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → (𝐷‘(𝐴‘𝐹)) = 0) | ||
| Theorem | deg1mul2 26153 | Degree of multiplication of two nonzero polynomials when the first leads with a nonzero-divisor coefficient. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ≠ 0 ) & ⊢ (𝜑 → ((coe1‘𝐹)‘(𝐷‘𝐹)) ∈ 𝐸) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) = ((𝐷‘𝐹) + (𝐷‘𝐺))) | ||
| Theorem | deg1mul 26154 | Degree of multiplication of two nonzero polynomials in a domain. (Contributed by metakunt, 6-May-2025.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ≠ 0 ) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) = ((𝐷‘𝐹) + (𝐷‘𝐺))) | ||
| Theorem | deg1mul3 26155 | Degree of multiplication of a polynomial on the left by a nonzero-dividing scalar. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Jul-2019.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((𝐴‘𝐹) · 𝐺)) = (𝐷‘𝐺)) | ||
| Theorem | deg1mul3le 26156 | Degree of multiplication of a polynomial on the left by a scalar. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((𝐴‘𝐹) · 𝐺)) ≤ (𝐷‘𝐺)) | ||
| Theorem | deg1tmle 26157 | Limiting degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐶 · (𝐹 ↑ 𝑋))) ≤ 𝐹) | ||
| Theorem | deg1tm 26158 | Exact degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝐶 ∈ 𝐾 ∧ 𝐶 ≠ 0 ) ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐶 · (𝐹 ↑ 𝑋))) = 𝐹) | ||
| Theorem | deg1pwle 26159 | Limiting degree of a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐹 ↑ 𝑋)) ≤ 𝐹) | ||
| Theorem | deg1pw 26160 | Exact degree of a variable power over a nontrivial ring. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐹 ↑ 𝑋)) = 𝐹) | ||
| Theorem | ply1nz 26161 | Univariate polynomials over a nonzero ring are a nonzero ring. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → 𝑃 ∈ NzRing) | ||
| Theorem | ply1nzb 26162 | Univariate polynomials are nonzero iff the base is nonzero. Or in contraposition, the univariate polynomials over the zero ring are also zero. (Contributed by Mario Carneiro, 13-Jun-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ 𝑃 ∈ NzRing)) | ||
| Theorem | ply1domn 26163 | Corollary of deg1mul2 26153: the univariate polynomials over a domain are a domain. This is true for multivariate but with a much more complicated proof. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn → 𝑃 ∈ Domn) | ||
| Theorem | ply1idom 26164 | The ring of univariate polynomials over an integral domain is itself an integral domain. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ IDomn → 𝑃 ∈ IDomn) | ||
| Syntax | cmn1 26165 | Monic polynomials. |
| class Monic1p | ||
| Syntax | cuc1p 26166 | Unitic polynomials. |
| class Unic1p | ||
| Syntax | cq1p 26167 | Univariate polynomial quotient. |
| class quot1p | ||
| Syntax | cr1p 26168 | Univariate polynomial remainder. |
| class rem1p | ||
| Syntax | cig1p 26169 | Univariate polynomial ideal generator. |
| class idlGen1p | ||
| Definition | df-mon1 26170* | Define the set of monic univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ Monic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) = (1r‘𝑟))}) | ||
| Definition | df-uc1p 26171* | Define the set of unitic univariate polynomials, as the polynomials with an invertible leading coefficient. This is not a standard concept but is useful to us as the set of polynomials which can be used as the divisor in the polynomial division theorem ply1divalg 26177. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}) | ||
| Definition | df-q1p 26172* | Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 26177. We actually use the reversed version for better harmony with our divisibility df-dvdsr 20357. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ quot1p = (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))) | ||
| Definition | df-r1p 26173* | Define the remainder after dividing two univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ rem1p = (𝑟 ∈ V ↦ ⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)))) | ||
| Definition | df-ig1p 26174* | Define a choice function for generators of ideals over a division ring; this is the unique monic polynomial of minimal degree in the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.) |
| ⊢ idlGen1p = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ if(𝑖 = {(0g‘(Poly1‘𝑟))}, (0g‘(Poly1‘𝑟)), (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))((deg1‘𝑟)‘𝑔) = inf(((deg1‘𝑟) “ (𝑖 ∖ {(0g‘(Poly1‘𝑟))})), ℝ, < ))))) | ||
| Theorem | ply1divmo 26175* | Uniqueness of a quotient in a polynomial division. For polynomials 𝐹, 𝐺 such that 𝐺 ≠ 0 and the leading coefficient of 𝐺 is not a zero divisor, there is at most one polynomial 𝑞 which satisfies 𝐹 = (𝐺 · 𝑞) + 𝑟 where the degree of 𝑟 is less than the degree of 𝐺. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Revised by NM, 17-Jun-2017.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ≠ 0 ) & ⊢ (𝜑 → ((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ 𝐸) & ⊢ 𝐸 = (RLReg‘𝑅) ⇒ ⊢ (𝜑 → ∃*𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) | ||
| Theorem | ply1divex 26176* | Lemma for ply1divalg 26177: existence part. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ≠ 0 ) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝐾) & ⊢ (𝜑 → (((coe1‘𝐺)‘(𝐷‘𝐺)) · 𝐼) = 1 ) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) | ||
| Theorem | ply1divalg 26177* | The division algorithm for univariate polynomials over a ring. For polynomials 𝐹, 𝐺 such that 𝐺 ≠ 0 and the leading coefficient of 𝐺 is a unit, there are unique polynomials 𝑞 and 𝑟 = 𝐹 − (𝐺 · 𝑞) such that the degree of 𝑟 is less than the degree of 𝐺. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ≠ 0 ) & ⊢ (𝜑 → ((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ 𝑈) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝜑 → ∃!𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) | ||
| Theorem | ply1divalg2 26178* | Reverse the order of multiplication in ply1divalg 26177 via the opposite ring. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ≠ 0 ) & ⊢ (𝜑 → ((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ 𝑈) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝜑 → ∃!𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝑞 ∙ 𝐺))) < (𝐷‘𝐺)) | ||
| Theorem | uc1pval 26179* | Value of the set of unitic polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ 𝐶 = {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧ ((coe1‘𝑓)‘(𝐷‘𝑓)) ∈ 𝑈)} | ||
| Theorem | isuc1p 26180 | Being a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 ↔ (𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ∧ ((coe1‘𝐹)‘(𝐷‘𝐹)) ∈ 𝑈)) | ||
| Theorem | mon1pval 26181* | Value of the set of monic polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ 𝑀 = {𝑓 ∈ 𝐵 ∣ (𝑓 ≠ 0 ∧ ((coe1‘𝑓)‘(𝐷‘𝑓)) = 1 )} | ||
| Theorem | ismon1p 26182 | Being a monic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑀 ↔ (𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ∧ ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1 )) | ||
| Theorem | uc1pcl 26183 | Unitic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 → 𝐹 ∈ 𝐵) | ||
| Theorem | mon1pcl 26184 | Monic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑀 → 𝐹 ∈ 𝐵) | ||
| Theorem | uc1pn0 26185 | Unitic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 → 𝐹 ≠ 0 ) | ||
| Theorem | mon1pn0 26186 | Monic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑀 → 𝐹 ≠ 0 ) | ||
| Theorem | uc1pdeg 26187 | Unitic polynomials have nonnegative degrees. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐶) → (𝐷‘𝐹) ∈ ℕ0) | ||
| Theorem | uc1pldg 26188 | Unitic polynomials have unit leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 → ((coe1‘𝐹)‘(𝐷‘𝐹)) ∈ 𝑈) | ||
| Theorem | mon1pldg 26189 | Unitic polynomials have one leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑀 → ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1 ) | ||
| Theorem | mon1puc1p 26190 | Monic polynomials are unitic. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑀) → 𝑋 ∈ 𝐶) | ||
| Theorem | uc1pmon1p 26191 | Make a unitic polynomial monic by multiplying a factor to normalize the leading coefficient. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
| ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ · = (.r‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶) → ((𝐴‘(𝐼‘((coe1‘𝑋)‘(𝐷‘𝑋)))) · 𝑋) ∈ 𝑀) | ||
| Theorem | deg1submon1p 26192 | The difference of two monic polynomials of the same degree is a polynomial of lesser degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑂 = (Monic1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝑂) & ⊢ (𝜑 → (𝐷‘𝐹) = 𝑋) & ⊢ (𝜑 → 𝐺 ∈ 𝑂) & ⊢ (𝜑 → (𝐷‘𝐺) = 𝑋) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 − 𝐺)) < 𝑋) | ||
| Theorem | mon1pid 26193 | Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 1 = (1r‘𝑃) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → ( 1 ∈ 𝑀 ∧ (𝐷‘ 1 ) = 0)) | ||
| Theorem | q1pval 26194* | Value of the univariate polynomial quotient function. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ · = (.r‘𝑃) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝑄𝐺) = (℩𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝑞 · 𝐺))) < (𝐷‘𝐺))) | ||
| Theorem | q1peqb 26195 | Characterizing property of the polynomial quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → ((𝑋 ∈ 𝐵 ∧ (𝐷‘(𝐹 − (𝑋 · 𝐺))) < (𝐷‘𝐺)) ↔ (𝐹𝑄𝐺) = 𝑋)) | ||
| Theorem | q1pcl 26196 | Closure of the quotient by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝑄𝐺) ∈ 𝐵) | ||
| Theorem | r1pval 26197 | Value of the polynomial remainder function. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑄 = (quot1p‘𝑅) & ⊢ · = (.r‘𝑃) & ⊢ − = (-g‘𝑃) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝐸𝐺) = (𝐹 − ((𝐹𝑄𝐺) · 𝐺))) | ||
| Theorem | r1pcl 26198 | Closure of remainder following division by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝐸𝐺) ∈ 𝐵) | ||
| Theorem | r1pdeglt 26199 | The remainder has a degree smaller than the divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
| ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐷‘(𝐹𝐸𝐺)) < (𝐷‘𝐺)) | ||
| Theorem | r1pid 26200 | Express the original polynomial 𝐹 as 𝐹 = (𝑞 · 𝐺) + 𝑟 using the quotient and remainder functions for 𝑞 and 𝑟. (Contributed by Mario Carneiro, 5-Jun-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ · = (.r‘𝑃) & ⊢ + = (+g‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → 𝐹 = (((𝐹𝑄𝐺) · 𝐺) + (𝐹𝐸𝐺))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |