![]() |
Metamath
Proof Explorer Theorem List (p. 244 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43661) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | deg1vscale 24301 | 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 24302 | 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 24303 | 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 24304 | 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 24305 | 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 24306 | 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 24307 | 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 24308 | 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 24309 | A scalar polynomial has nonpositive degree. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾) → (𝐷‘(𝐴‘𝐹)) ≤ 0) | ||
Theorem | deg1scl 24310 | 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 24311 | 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 24312 | 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 24313 | 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 24314 | Limiting degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐶 · (𝐹 ↑ 𝑋))) ≤ 𝐹) | ||
Theorem | deg1tm 24315 | 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 24316 | Limiting degree of a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐹 ↑ 𝑋)) ≤ 𝐹) | ||
Theorem | deg1pw 24317 | 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 24318 | Univariate polynomials over a nonzero ring are a nonzero ring. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → 𝑃 ∈ NzRing) | ||
Theorem | ply1nzb 24319 | 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 24320 | Corollary of deg1mul2 24311: 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 24321 | 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 24322 | Monic polynomials. |
class Monic1p | ||
Syntax | cuc1p 24323 | Unitic polynomials. |
class Unic1p | ||
Syntax | cq1p 24324 | Univariate polynomial quotient. |
class quot1p | ||
Syntax | cr1p 24325 | Univariate polynomial remainder. |
class rem1p | ||
Syntax | cig1p 24326 | Univariate polynomial ideal generator. |
class idlGen1p | ||
Definition | df-mon1 24327* | 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 24328* | 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 24334. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}) | ||
Definition | df-q1p 24329* | Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 24334. We actually use the reversed version for better harmony with our divisibility df-dvdsr 19028. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ quot1p = (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))) | ||
Definition | df-r1p 24330* | 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 24331* | 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 24332* | 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 24333* | Lemma for ply1divalg 24334: 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 24334* | 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 24335* | Reverse the order of multiplication in ply1divalg 24334 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 24336* | 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 24337 | Being a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 ↔ (𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ∧ ((coe1‘𝐹)‘(𝐷‘𝐹)) ∈ 𝑈)) | ||
Theorem | mon1pval 24338* | 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 24339 | 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 24340 | Unitic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 → 𝐹 ∈ 𝐵) | ||
Theorem | mon1pcl 24341 | Monic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑀 → 𝐹 ∈ 𝐵) | ||
Theorem | uc1pn0 24342 | Unitic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 → 𝐹 ≠ 0 ) | ||
Theorem | mon1pn0 24343 | Monic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑀 → 𝐹 ≠ 0 ) | ||
Theorem | uc1pdeg 24344 | Unitic polynomials have nonnegative degrees. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐶) → (𝐷‘𝐹) ∈ ℕ0) | ||
Theorem | uc1pldg 24345 | Unitic polynomials have unit leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 → ((coe1‘𝐹)‘(𝐷‘𝐹)) ∈ 𝑈) | ||
Theorem | mon1pldg 24346 | Unitic polynomials have one leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑀 → ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1 ) | ||
Theorem | mon1puc1p 24347 | Monic polynomials are unitic. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑀) → 𝑋 ∈ 𝐶) | ||
Theorem | uc1pmon1p 24348 | 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 24349 | 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 24350* | Value of the univariate polynomial quotient function. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ · = (.r‘𝑃) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝑄𝐺) = (℩𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝑞 · 𝐺))) < (𝐷‘𝐺))) | ||
Theorem | q1peqb 24351 | Characterizing property of the polynomial quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → ((𝑋 ∈ 𝐵 ∧ (𝐷‘(𝐹 − (𝑋 · 𝐺))) < (𝐷‘𝐺)) ↔ (𝐹𝑄𝐺) = 𝑋)) | ||
Theorem | q1pcl 24352 | Closure of the quotient by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝑄𝐺) ∈ 𝐵) | ||
Theorem | r1pval 24353 | Value of the polynomial remainder function. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑄 = (quot1p‘𝑅) & ⊢ · = (.r‘𝑃) & ⊢ − = (-g‘𝑃) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝐸𝐺) = (𝐹 − ((𝐹𝑄𝐺) · 𝐺))) | ||
Theorem | r1pcl 24354 | Closure of remainder following division by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝐸𝐺) ∈ 𝐵) | ||
Theorem | r1pdeglt 24355 | 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 24356 | 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 24357 | 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 24358 | 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 24359 | 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 24360 | The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout 15666). 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 24361 | 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 24362 | Lemma for fta1g 24364. (Contributed by Mario Carneiro, 7-Jun-2016.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝑇)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1)) & ⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊})) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁) | ||
Theorem | fta1glem2 24363* | Lemma for fta1g 24364. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝑇)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1)) & ⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊})) & ⊢ (𝜑 → ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑁 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔))) ⇒ ⊢ (𝜑 → (♯‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹)) | ||
Theorem | fta1g 24364 | The one-sided fundamental theorem of algebra. A polynomial of degree 𝑛 has at most 𝑛 roots. Unlike the real fundamental theorem fta 25258, 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 24365 | Lemma for fta1b 24366. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑀 ∈ 𝐾) & ⊢ (𝜑 → 𝑁 ∈ 𝐾) & ⊢ (𝜑 → (𝑀 × 𝑁) = 𝑊) & ⊢ (𝜑 → 𝑀 ≠ 𝑊) & ⊢ (𝜑 → ((𝑀 · 𝑋) ∈ (𝐵 ∖ { 0 }) → (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ (𝐷‘(𝑀 · 𝑋)))) ⇒ ⊢ (𝜑 → 𝑁 = 𝑊) | ||
Theorem | fta1b 24366* | The assumption that 𝑅 be a domain in fta1g 24364 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 24367 | 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 24368* | 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 24369* | 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 24370 | 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 24371 | 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 24372 | 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 24373 | 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 24374 | 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 ∧ 𝐼 ∈ 𝑈) → 𝐼 = (𝐾‘{(𝐺‘𝐼)})) | ||
Theorem | ply1lpir 24375 | The ring of polynomials over a division ring has the principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → 𝑃 ∈ LPIR) | ||
Theorem | ply1pid 24376 | The polynomials over a field are a PID. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ Field → 𝑃 ∈ PID) | ||
Syntax | cply 24377 | Extend class notation to include the set of complex polynomials. |
class Poly | ||
Syntax | cidp 24378 | Extend class notation to include the identity polynomial. |
class Xp | ||
Syntax | ccoe 24379 | Extend class notation to include the coefficient function on polynomials. |
class coeff | ||
Syntax | cdgr 24380 | Extend class notation to include the degree function on polynomials. |
class deg | ||
Definition | df-ply 24381* | Define the set of polynomials on the complex numbers with coefficients in the given subset. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ Poly = (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑𝑚 ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))}) | ||
Definition | df-idp 24382 | Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ Xp = ( I ↾ ℂ) | ||
Definition | df-coe 24383* | Define the coefficient function for a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ coeff = (𝑓 ∈ (Poly‘ℂ) ↦ (℩𝑎 ∈ (ℂ ↑𝑚 ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) | ||
Definition | df-dgr 24384 | Define the degree of a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ deg = (𝑓 ∈ (Poly‘ℂ) ↦ sup((◡(coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < )) | ||
Theorem | plyco0 24385* | Two ways to say that a function on the nonnegative integers has finite support. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴:ℕ0⟶ℂ) → ((𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) | ||
Theorem | plyval 24386* | Value of the polynomial set function. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (𝑆 ⊆ ℂ → (Poly‘𝑆) = {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚 ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))}) | ||
Theorem | plybss 24387 | Reverse closure of the parameter 𝑆 of the polynomial set function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ) | ||
Theorem | elply 24388* | Definition of a polynomial with coefficients in 𝑆. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚 ℕ0)𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) | ||
Theorem | elply2 24389* | The coefficient function can be assumed to have zeroes outside 0...𝑛. (Contributed by Mario Carneiro, 20-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) | ||
Theorem | plyun0 24390 | The set of polynomials is unaffected by the addition of zero. (This is built into the definition because all higher powers of a polynomial are effectively zero, so we require that the coefficient field contain zero to simplify some of our closure theorems.) (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (Poly‘(𝑆 ∪ {0})) = (Poly‘𝑆) | ||
Theorem | plyf 24391 | The polynomial is a function on the complex numbers. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) | ||
Theorem | plyss 24392 | The polynomial set function preserves the subset relation. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (Poly‘𝑆) ⊆ (Poly‘𝑇)) | ||
Theorem | plyssc 24393 | Every polynomial ring is contained in the ring of polynomials over ℂ. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (Poly‘𝑆) ⊆ (Poly‘ℂ) | ||
Theorem | elplyr 24394* | Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴:ℕ0⟶𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) | ||
Theorem | elplyd 24395* | Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) | ||
Theorem | ply1termlem 24396* | Lemma for ply1term 24397. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)))) | ||
Theorem | ply1term 24397* | A one-term polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁))) ⇒ ⊢ ((𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → 𝐹 ∈ (Poly‘𝑆)) | ||
Theorem | plypow 24398* | A power is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ ((𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑁)) ∈ (Poly‘𝑆)) | ||
Theorem | plyconst 24399 | A constant function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ ((𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆) → (ℂ × {𝐴}) ∈ (Poly‘𝑆)) | ||
Theorem | ne0p 24400 | A test to show that a polynomial is nonzero. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ (𝐹‘𝐴) ≠ 0) → 𝐹 ≠ 0𝑝) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |