Home | Metamath
Proof Explorer Theorem List (p. 247 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mdegmullem 24601* | Lemma for mdegmulle2 24602. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = (.r‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐽) & ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐾) & ⊢ 𝐴 = {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (𝑏 ∈ 𝐴 ↦ (ℂfld Σg 𝑏)) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾)) | ||
Theorem | mdegmulle2 24602 | 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 24603 | 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 24604 | Functionality of univariate polynomial degree, weak range. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ 𝐷:𝐵⟶ℝ* | ||
Theorem | deg1xrcl 24605 | Closure of univariate polynomial degree in extended reals. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ ℝ*) | ||
Theorem | deg1cl 24606 | Sharp closure of univariate polynomial degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ (ℕ0 ∪ {-∞})) | ||
Theorem | mdegpropd 24607* | 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 24608 | Univariate polynomial degree respects protection. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ ( deg1 ‘𝑅) = ( deg1 ‘( I ‘𝑅)) | ||
Theorem | deg1propd 24609* | Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → ( deg1 ‘𝑅) = ( deg1 ‘𝑆)) | ||
Theorem | deg1z 24610 | Degree of the zero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → (𝐷‘ 0 ) = -∞) | ||
Theorem | deg1nn0cl 24611 | 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 24612 | 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 24613 | 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 24614 | 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 24615 | 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 24616 | 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 24617 | 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 24618* | Property of being of limited degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ ∀𝑥 ∈ ℕ0 (𝐺 < 𝑥 → (𝐴‘𝑥) = 0 ))) | ||
Theorem | deg1val 24619 | 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 24620 | 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 24621 | 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 24622 | 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 24623 | 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 24624 | 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 24625 | 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 24626 | 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 24627 | 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 24628 | 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 24629 | 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 24630 | 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 24631 | 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 24632 | 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 24633 | 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 24634 | 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 24635 | A scalar polynomial has nonpositive degree. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾) → (𝐷‘(𝐴‘𝐹)) ≤ 0) | ||
Theorem | deg1scl 24636 | 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 24637 | 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 | deg1mul3 24638 | 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 24639 | 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 24640 | Limiting degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐶 · (𝐹 ↑ 𝑋))) ≤ 𝐹) | ||
Theorem | deg1tm 24641 | 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 24642 | Limiting degree of a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐹 ↑ 𝑋)) ≤ 𝐹) | ||
Theorem | deg1pw 24643 | 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 24644 | Univariate polynomials over a nonzero ring are a nonzero ring. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → 𝑃 ∈ NzRing) | ||
Theorem | ply1nzb 24645 | 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 24646 | Corollary of deg1mul2 24637: 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 24647 | 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 24648 | Monic polynomials. |
class Monic1p | ||
Syntax | cuc1p 24649 | Unitic polynomials. |
class Unic1p | ||
Syntax | cq1p 24650 | Univariate polynomial quotient. |
class quot1p | ||
Syntax | cr1p 24651 | Univariate polynomial remainder. |
class rem1p | ||
Syntax | cig1p 24652 | Univariate polynomial ideal generator. |
class idlGen1p | ||
Definition | df-mon1 24653* | 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 24654* | 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 24660. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}) | ||
Definition | df-q1p 24655* | Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 24660. We actually use the reversed version for better harmony with our divisibility df-dvdsr 19322. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ quot1p = (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))) | ||
Definition | df-r1p 24656* | 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 24657* | 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 24658* | 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 24659* | Lemma for ply1divalg 24660: 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 24660* | 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 24661* | Reverse the order of multiplication in ply1divalg 24660 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 24662* | 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 24663 | Being a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 ↔ (𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ∧ ((coe1‘𝐹)‘(𝐷‘𝐹)) ∈ 𝑈)) | ||
Theorem | mon1pval 24664* | 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 24665 | 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 24666 | Unitic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 → 𝐹 ∈ 𝐵) | ||
Theorem | mon1pcl 24667 | Monic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑀 → 𝐹 ∈ 𝐵) | ||
Theorem | uc1pn0 24668 | Unitic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 → 𝐹 ≠ 0 ) | ||
Theorem | mon1pn0 24669 | Monic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑀 → 𝐹 ≠ 0 ) | ||
Theorem | uc1pdeg 24670 | Unitic polynomials have nonnegative degrees. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐶) → (𝐷‘𝐹) ∈ ℕ0) | ||
Theorem | uc1pldg 24671 | Unitic polynomials have unit leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 → ((coe1‘𝐹)‘(𝐷‘𝐹)) ∈ 𝑈) | ||
Theorem | mon1pldg 24672 | Unitic polynomials have one leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑀 → ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1 ) | ||
Theorem | mon1puc1p 24673 | Monic polynomials are unitic. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑀) → 𝑋 ∈ 𝐶) | ||
Theorem | uc1pmon1p 24674 | 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 24675 | 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 | q1pval 24676* | Value of the univariate polynomial quotient function. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ · = (.r‘𝑃) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝑄𝐺) = (℩𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝑞 · 𝐺))) < (𝐷‘𝐺))) | ||
Theorem | q1peqb 24677 | Characterizing property of the polynomial quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → ((𝑋 ∈ 𝐵 ∧ (𝐷‘(𝐹 − (𝑋 · 𝐺))) < (𝐷‘𝐺)) ↔ (𝐹𝑄𝐺) = 𝑋)) | ||
Theorem | q1pcl 24678 | Closure of the quotient by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝑄𝐺) ∈ 𝐵) | ||
Theorem | r1pval 24679 | Value of the polynomial remainder function. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑄 = (quot1p‘𝑅) & ⊢ · = (.r‘𝑃) & ⊢ − = (-g‘𝑃) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝐸𝐺) = (𝐹 − ((𝐹𝑄𝐺) · 𝐺))) | ||
Theorem | r1pcl 24680 | Closure of remainder following division by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝐸𝐺) ∈ 𝐵) | ||
Theorem | r1pdeglt 24681 | 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 24682 | 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 ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → 𝐹 = (((𝐹𝑄𝐺) · 𝐺) + (𝐹𝐸𝐺))) | ||
Theorem | dvdsq1p 24683 | Divisibility in a polynomial ring is witnessed by the quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ ∥ = (∥r‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ · = (.r‘𝑃) & ⊢ 𝑄 = (quot1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 ↔ 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) | ||
Theorem | dvdsr1p 24684 | Divisibility in a polynomial ring in terms of the remainder. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ ∥ = (∥r‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐸 = (rem1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 ↔ (𝐹𝐸𝐺) = 0 )) | ||
Theorem | ply1remlem 24685 | A term of the form 𝑥 − 𝑁 is linear, monic, and has exactly one zero. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝑁)) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ 𝐾) & ⊢ 𝑈 = (Monic1p‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝑈 ∧ (𝐷‘𝐺) = 1 ∧ (◡(𝑂‘𝐺) “ { 0 }) = {𝑁})) | ||
Theorem | ply1rem 24686 | The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout 15881). If a polynomial 𝐹 is divided by the linear factor 𝑥 − 𝐴, the remainder is equal to 𝐹(𝐴), the evaluation of the polynomial at 𝐴 (interpreted as a constant polynomial). (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝑁)) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ 𝐸 = (rem1p‘𝑅) ⇒ ⊢ (𝜑 → (𝐹𝐸𝐺) = (𝐴‘((𝑂‘𝐹)‘𝑁))) | ||
Theorem | facth1 24687 | The factor theorem and its converse. A polynomial 𝐹 has a root at 𝐴 iff 𝐺 = 𝑥 − 𝐴 is a factor of 𝐹. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝑁)) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ 0 = (0g‘𝑅) & ⊢ ∥ = (∥r‘𝑃) ⇒ ⊢ (𝜑 → (𝐺 ∥ 𝐹 ↔ ((𝑂‘𝐹)‘𝑁) = 0 )) | ||
Theorem | fta1glem1 24688 | Lemma for fta1g 24690. (Contributed by Mario Carneiro, 7-Jun-2016.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝑇)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1)) & ⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊})) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁) | ||
Theorem | fta1glem2 24689* | Lemma for fta1g 24690. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝑇)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1)) & ⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊})) & ⊢ (𝜑 → ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑁 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔))) ⇒ ⊢ (𝜑 → (♯‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹)) | ||
Theorem | fta1g 24690 | The one-sided fundamental theorem of algebra. A polynomial of degree 𝑛 has at most 𝑛 roots. Unlike the real fundamental theorem fta 25585, which is only true in ℂ and other algebraically closed fields, this is true in any integral domain. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ≠ 0 ) ⇒ ⊢ (𝜑 → (♯‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹)) | ||
Theorem | fta1blem 24691 | Lemma for fta1b 24692. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑀 ∈ 𝐾) & ⊢ (𝜑 → 𝑁 ∈ 𝐾) & ⊢ (𝜑 → (𝑀 × 𝑁) = 𝑊) & ⊢ (𝜑 → 𝑀 ≠ 𝑊) & ⊢ (𝜑 → ((𝑀 · 𝑋) ∈ (𝐵 ∖ { 0 }) → (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ (𝐷‘(𝑀 · 𝑋)))) ⇒ ⊢ (𝜑 → 𝑁 = 𝑊) | ||
Theorem | fta1b 24692* | The assumption that 𝑅 be a domain in fta1g 24690 is necessary. Here we show that the statement is strong enough to prove that 𝑅 is a domain. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) ⇒ ⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀𝑓 ∈ (𝐵 ∖ { 0 })(♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) | ||
Theorem | drnguc1p 24693 | Over a division ring, all nonzero polynomials are unitic. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → 𝐹 ∈ 𝐶) | ||
Theorem | ig1peu 24694* | There is a unique monic polynomial of minimal degree in any nonzero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∃!𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )) | ||
Theorem | ig1pval 24695* | Substitutions for the polynomial ideal generator function. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈) → (𝐺‘𝐼) = if(𝐼 = { 0 }, 0 , (℩𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))) | ||
Theorem | ig1pval2 24696 | Generator of the zero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Sep-2020.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 0 = (0g‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → (𝐺‘{ 0 }) = 0 ) | ||
Theorem | ig1pval3 24697 | Characterizing properties of the monic generator of a nonzero ideal of polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ((𝐺‘𝐼) ∈ 𝐼 ∧ (𝐺‘𝐼) ∈ 𝑀 ∧ (𝐷‘(𝐺‘𝐼)) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))) | ||
Theorem | ig1pcl 24698 | The monic generator of an ideal is always in the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Sep-2020.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈) → (𝐺‘𝐼) ∈ 𝐼) | ||
Theorem | ig1pdvds 24699 | The monic generator of an ideal divides all elements of the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Sep-2020.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ ∥ = (∥r‘𝑃) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼) → (𝐺‘𝐼) ∥ 𝑋) | ||
Theorem | ig1prsp 24700 | Any ideal of polynomials over a division ring is generated by the ideal's canonical generator. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝐾 = (RSpan‘𝑃) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈) → 𝐼 = (𝐾‘{(𝐺‘𝐼)})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |