Home | Metamath
Proof Explorer Theorem List (p. 397 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 | ||
Syntax | cldgis 39601 | The leading ideal sequence used in the Hilbert Basis Theorem. |
class ldgIdlSeq | ||
Definition | df-ldgis 39602* | Define a function which carries polynomial ideals to the sequence of coefficient ideals of leading coefficients of degree- 𝑥 elements in the polynomial ideal. The proof that this map is strictly monotone is the core of the Hilbert Basis Theorem hbt 39610. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))}))) | ||
Theorem | hbtlem1 39603* | Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) = {𝑗 ∣ ∃𝑘 ∈ 𝐼 ((𝐷‘𝑘) ≤ 𝑋 ∧ 𝑗 = ((coe1‘𝑘)‘𝑋))}) | ||
Theorem | hbtlem2 39604 | Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝑇 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) ∈ 𝑇) | ||
Theorem | hbtlem7 39605 | Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝑇 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝑆‘𝐼):ℕ0⟶𝑇) | ||
Theorem | hbtlem4 39606 | The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ ℕ0) & ⊢ (𝜑 → 𝑌 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐼)‘𝑌)) | ||
Theorem | hbtlem3 39607 | The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝐽 ∈ 𝑈) & ⊢ (𝜑 → 𝐼 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐽)‘𝑋)) | ||
Theorem | hbtlem5 39608* | The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝐽 ∈ 𝑈) & ⊢ (𝜑 → 𝐼 ⊆ 𝐽) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ0 ((𝑆‘𝐽)‘𝑥) ⊆ ((𝑆‘𝐼)‘𝑥)) ⇒ ⊢ (𝜑 → 𝐼 = 𝐽) | ||
Theorem | hbtlem6 39609* | There is a finite set of polynomials matching any single stage of the image. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝑁 = (RSpan‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ LNoeR) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ ℕ0) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ (𝒫 𝐼 ∩ Fin)((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘(𝑁‘𝑘))‘𝑋)) | ||
Theorem | hbt 39610 | The Hilbert Basis Theorem - the ring of univariate polynomials over a Noetherian ring is a Noetherian ring. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ LNoeR → 𝑃 ∈ LNoeR) | ||
Syntax | cmnc 39611 | Extend class notation with the class of monic polynomials. |
class Monic | ||
Syntax | cplylt 39612 | Extend class notatin with the class of limited-degree polynomials. |
class Poly< | ||
Definition | df-mnc 39613* | Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ Monic = (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1}) | ||
Definition | df-plylt 39614* | Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.) |
⊢ Poly< = (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)}) | ||
Theorem | dgrsub2 39615 | Subtracting two polynomials with the same degree and top coefficient gives a polynomial of strictly lower degree. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ 𝑁 = (deg‘𝐹) ⇒ ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (deg‘(𝐹 ∘f − 𝐺)) < 𝑁) | ||
Theorem | elmnc 39616 | Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) ↔ (𝑃 ∈ (Poly‘𝑆) ∧ ((coeff‘𝑃)‘(deg‘𝑃)) = 1)) | ||
Theorem | mncply 39617 | A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ∈ (Poly‘𝑆)) | ||
Theorem | mnccoe 39618 | A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) → ((coeff‘𝑃)‘(deg‘𝑃)) = 1) | ||
Theorem | mncn0 39619 | A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ≠ 0𝑝) | ||
Syntax | cdgraa 39620 | Extend class notation to include the degree function for algebraic numbers. |
class degAA | ||
Syntax | cmpaa 39621 | Extend class notation to include the minimal polynomial for an algebraic number. |
class minPolyAA | ||
Definition | df-dgraa 39622* | Define the degree of an algebraic number as the smallest degree of any nonzero polynomial which has said number as a root. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Revised by AV, 29-Sep-2020.) |
⊢ degAA = (𝑥 ∈ 𝔸 ↦ inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < )) | ||
Definition | df-mpaa 39623* | Define the minimal polynomial of an algebraic number as the unique monic polynomial which achieves the minimum of degAA. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ minPolyAA = (𝑥 ∈ 𝔸 ↦ (℩𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) = (degAA‘𝑥) ∧ (𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝑥)) = 1))) | ||
Theorem | dgraaval 39624* | Value of the degree function on an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Revised by AV, 29-Sep-2020.) |
⊢ (𝐴 ∈ 𝔸 → (degAA‘𝐴) = inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝐴) = 0)}, ℝ, < )) | ||
Theorem | dgraalem 39625* | Properties of the degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.) |
⊢ (𝐴 ∈ 𝔸 → ((degAA‘𝐴) ∈ ℕ ∧ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0))) | ||
Theorem | dgraacl 39626 | Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → (degAA‘𝐴) ∈ ℕ) | ||
Theorem | dgraaf 39627 | Degree function on algebraic numbers is a function. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.) |
⊢ degAA:𝔸⟶ℕ | ||
Theorem | dgraaub 39628 | Upper bound on degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.) |
⊢ (((𝑃 ∈ (Poly‘ℚ) ∧ 𝑃 ≠ 0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → (degAA‘𝐴) ≤ (deg‘𝑃)) | ||
Theorem | dgraa0p 39629 | A rational polynomial of degree less than an algebraic number cannot be zero at that number unless it is the zero polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ ((𝐴 ∈ 𝔸 ∧ 𝑃 ∈ (Poly‘ℚ) ∧ (deg‘𝑃) < (degAA‘𝐴)) → ((𝑃‘𝐴) = 0 ↔ 𝑃 = 0𝑝)) | ||
Theorem | mpaaeu 39630* | An algebraic number has exactly one monic polynomial of the least degree. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → ∃!𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1)) | ||
Theorem | mpaaval 39631* | Value of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → (minPolyAA‘𝐴) = (℩𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) = (degAA‘𝐴) ∧ (𝑝‘𝐴) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝐴)) = 1))) | ||
Theorem | mpaalem 39632 | Properties of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → ((minPolyAA‘𝐴) ∈ (Poly‘ℚ) ∧ ((deg‘(minPolyAA‘𝐴)) = (degAA‘𝐴) ∧ ((minPolyAA‘𝐴)‘𝐴) = 0 ∧ ((coeff‘(minPolyAA‘𝐴))‘(degAA‘𝐴)) = 1))) | ||
Theorem | mpaacl 39633 | Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → (minPolyAA‘𝐴) ∈ (Poly‘ℚ)) | ||
Theorem | mpaadgr 39634 | Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → (deg‘(minPolyAA‘𝐴)) = (degAA‘𝐴)) | ||
Theorem | mpaaroot 39635 | The minimal polynomial of an algebraic number has the number as a root. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → ((minPolyAA‘𝐴)‘𝐴) = 0) | ||
Theorem | mpaamn 39636 | Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → ((coeff‘(minPolyAA‘𝐴))‘(degAA‘𝐴)) = 1) | ||
Syntax | citgo 39637 | Extend class notation with the integral-over predicate. |
class IntgOver | ||
Syntax | cza 39638 | Extend class notation with the class of algebraic integers. |
class ℤ | ||
Definition | df-itgo 39639* | A complex number is said to be integral over a subset if it is the root of a monic polynomial with coefficients from the subset. This definition is typically not used for fields but it works there, see aaitgo 39642. This definition could work for subsets of an arbitrary ring with a more general definition of polynomials. TODO: use Monic. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}) | ||
Definition | df-za 39640 | Define an algebraic integer as a complex number which is the root of a monic integer polynomial. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ ℤ = (IntgOver‘ℤ) | ||
Theorem | itgoval 39641* | Value of the integral-over function. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ (𝑆 ⊆ ℂ → (IntgOver‘𝑆) = {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑆)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}) | ||
Theorem | aaitgo 39642 | The standard algebraic numbers 𝔸 are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝔸 = (IntgOver‘ℚ) | ||
Theorem | itgoss 39643 | An integral element is integral over a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (IntgOver‘𝑆) ⊆ (IntgOver‘𝑇)) | ||
Theorem | itgocn 39644 | All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ (IntgOver‘𝑆) ⊆ ℂ | ||
Theorem | cnsrexpcl 39645 | Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑋↑𝑌) ∈ 𝑆) | ||
Theorem | fsumcnsrcl 39646* | Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) | ||
Theorem | cnsrplycl 39647 | Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝑃 ∈ (Poly‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝑃‘𝑋) ∈ 𝑆) | ||
Theorem | rgspnval 39648* | Value of the ring-span of a set of elements in a ring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅)) & ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴)) ⇒ ⊢ (𝜑 → 𝑈 = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡}) | ||
Theorem | rgspncl 39649 | The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅)) & ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴)) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑅)) | ||
Theorem | rgspnssid 39650 | The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅)) & ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝑈) | ||
Theorem | rgspnmin 39651 | The ring-span is contained in all subspaces which contain all the generators. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅)) & ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴)) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) ⇒ ⊢ (𝜑 → 𝑈 ⊆ 𝑆) | ||
Theorem | rgspnid 39652 | The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑆 = ((RingSpan‘𝑅)‘𝐴)) ⇒ ⊢ (𝜑 → 𝑆 = 𝐴) | ||
Theorem | rngunsnply 39653* | Adjoining one element to a ring results in a set of polynomial evaluations. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝐵 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑆 = ((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) ⇒ ⊢ (𝜑 → (𝑉 ∈ 𝑆 ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋))) | ||
Theorem | flcidc 39654* | Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝜑 → 𝐹 = (𝑗 ∈ 𝑆 ↦ if(𝑗 = 𝐾, 1, 0))) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑆) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑖 ∈ 𝑆 ((𝐹‘𝑖) · 𝐵) = ⦋𝐾 / 𝑖⦌𝐵) | ||
Syntax | cmend 39655 | Syntax for module endomorphism algebra. |
class MEndo | ||
Definition | df-mend 39656* | Define the endomorphism algebra of a module. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ MEndo = (𝑚 ∈ V ↦ ⦋(𝑚 LMHom 𝑚) / 𝑏⦌({〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))〉, 〈(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx), (Scalar‘𝑚)〉, 〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))〉})) | ||
Theorem | algstr 39657 | Lemma to shorten proofs of algbase 39658 through algvsca 39662. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ 𝐴 Struct 〈1, 6〉 | ||
Theorem | algbase 39658 | The base set of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐴)) | ||
Theorem | algaddg 39659 | The additive operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ ( + ∈ 𝑉 → + = (+g‘𝐴)) | ||
Theorem | algmulr 39660 | The multiplicative operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ ( × ∈ 𝑉 → × = (.r‘𝐴)) | ||
Theorem | algsca 39661 | The set of scalars of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (𝑆 ∈ 𝑉 → 𝑆 = (Scalar‘𝐴)) | ||
Theorem | algvsca 39662 | The scalar product operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ ( · ∈ 𝑉 → · = ( ·𝑠 ‘𝐴)) | ||
Theorem | mendval 39663* | Value of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐵 = (𝑀 LMHom 𝑀) & ⊢ + = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f (+g‘𝑀)𝑦)) & ⊢ × = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ · = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f ( ·𝑠 ‘𝑀)𝑦)) ⇒ ⊢ (𝑀 ∈ 𝑋 → (MEndo‘𝑀) = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉})) | ||
Theorem | mendbas 39664 | Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) ⇒ ⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) | ||
Theorem | mendplusgfval 39665* | Addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 3-Mar-2024.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ + = (+g‘𝑀) ⇒ ⊢ (+g‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦)) | ||
Theorem | mendplusg 39666 | A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ + = (+g‘𝑀) & ⊢ ✚ = (+g‘𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌)) | ||
Theorem | mendmulrfval 39667* | Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 3-Mar-2024.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (.r‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) | ||
Theorem | mendmulr 39668 | A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = (.r‘𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑋 ∘ 𝑌)) | ||
Theorem | mendsca 39669 | The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) ⇒ ⊢ 𝑆 = (Scalar‘𝐴) | ||
Theorem | mendvscafval 39670* | Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 3-Mar-2024.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐸 = (Base‘𝑀) ⇒ ⊢ ( ·𝑠 ‘𝐴) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦)) | ||
Theorem | mendvsca 39671 | A specific scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐸 = (Base‘𝑀) & ⊢ ∙ = ( ·𝑠 ‘𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∙ 𝑌) = ((𝐸 × {𝑋}) ∘f · 𝑌)) | ||
Theorem | mendring 39672 | The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) ⇒ ⊢ (𝑀 ∈ LMod → 𝐴 ∈ Ring) | ||
Theorem | mendlmod 39673 | The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ LMod) | ||
Theorem | mendassa 39674 | The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ AssAlg) | ||
Theorem | idomrootle 39675* | No element of an integral domain can have more than 𝑁 𝑁-th roots. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) ⇒ ⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (♯‘{𝑦 ∈ 𝐵 ∣ (𝑁 ↑ 𝑦) = 𝑋}) ≤ 𝑁) | ||
Theorem | idomodle 39676* | Limit on the number of 𝑁-th roots of unity in an integral domain. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) ≤ 𝑁) | ||
Theorem | fiuneneq 39677 | Two finite sets of equal size have a union of the same size iff they were equal. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin) → ((𝐴 ∪ 𝐵) ≈ 𝐴 ↔ 𝐴 = 𝐵)) | ||
Theorem | idomsubgmo 39678* | The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Revised by NM, 17-Jun-2017.) |
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) ⇒ ⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → ∃*𝑦 ∈ (SubGrp‘𝐺)(♯‘𝑦) = 𝑁) | ||
Theorem | proot1mul 39679 | Any primitive 𝑁-th root of unity is a multiple of any other. (Contributed by Stefan O'Rear, 2-Nov-2015.) |
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → 𝑋 ∈ (𝐾‘{𝑌})) | ||
Theorem | proot1hash 39680 | If an integral domain has a primitive 𝑁-th root of unity, it has exactly (ϕ‘𝑁) of them. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ (◡𝑂 “ {𝑁})) → (♯‘(◡𝑂 “ {𝑁})) = (ϕ‘𝑁)) | ||
Theorem | proot1ex 39681 | The complex field has primitive 𝑁-th roots of unity for all 𝑁. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝐺 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ → (-1↑𝑐(2 / 𝑁)) ∈ (◡𝑂 “ {𝑁})) | ||
Syntax | ccytp 39682 | Syntax for the sequence of cyclotomic polynomials. |
class CytP | ||
Definition | df-cytp 39683* | The Nth cyclotomic polynomial is the polynomial which has as its zeros precisely the primitive Nth roots of unity. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ CytP = (𝑛 ∈ ℕ ↦ ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))))) | ||
Theorem | isdomn3 39684 | Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈ (SubMnd‘𝑈))) | ||
Theorem | mon1pid 39685 | 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 | mon1psubm 39686 | Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝑈 = (mulGrp‘𝑃) ⇒ ⊢ (𝑅 ∈ NzRing → 𝑀 ∈ (SubMnd‘𝑈)) | ||
Theorem | deg1mhm 39687 | Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑌 = ((mulGrp‘𝑃) ↾s (𝐵 ∖ { 0 })) & ⊢ 𝑁 = (ℂfld ↾s ℕ0) ⇒ ⊢ (𝑅 ∈ Domn → (𝐷 ↾ (𝐵 ∖ { 0 })) ∈ (𝑌 MndHom 𝑁)) | ||
Theorem | cytpfn 39688 | Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ CytP Fn ℕ | ||
Theorem | cytpval 39689* | Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝑇 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) & ⊢ 𝑂 = (od‘𝑇) & ⊢ 𝑃 = (Poly1‘ℂfld) & ⊢ 𝑋 = (var1‘ℂfld) & ⊢ 𝑄 = (mulGrp‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ (𝑁 ∈ ℕ → (CytP‘𝑁) = (𝑄 Σg (𝑟 ∈ (◡𝑂 “ {𝑁}) ↦ (𝑋 − (𝐴‘𝑟))))) | ||
Theorem | fgraphopab 39690* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)}) | ||
Theorem | fgraphxp 39691* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {𝑥 ∈ (𝐴 × 𝐵) ∣ (𝐹‘(1st ‘𝑥)) = (2nd ‘𝑥)}) | ||
Theorem | hausgraph 39692 | The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (Clsd‘(𝐽 ×t 𝐾))) | ||
Syntax | ctopsep 39693 | The class of separable toplogies. |
class TopSep | ||
Syntax | ctoplnd 39694 | The class of Lindelöf toplogies. |
class TopLnd | ||
Definition | df-topsep 39695* | A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
⊢ TopSep = {𝑗 ∈ Top ∣ ∃𝑥 ∈ 𝒫 ∪ 𝑗(𝑥 ≼ ω ∧ ((cls‘𝑗)‘𝑥) = ∪ 𝑗)} | ||
Definition | df-toplnd 39696* | A topology is Lindelöf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
⊢ TopLnd = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧))} | ||
Theorem | iocunico 39697 | Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∪ (𝐵[,)𝐶)) = (𝐴(,)𝐶)) | ||
Theorem | iocinico 39698 | The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶)) = {𝐵}) | ||
Theorem | iocmbl 39699 | An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ∈ dom vol) | ||
Theorem | cnioobibld 39700* | A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider 𝐹 = (𝑥 ∈ (0(,)1) ↦ (1 / 𝑥)). See cniccibl 24370 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝐿1) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |