Home | Metamath
Proof Explorer Theorem List (p. 368 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lnrring 36701 | Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝐴 ∈ LNoeR → 𝐴 ∈ Ring) | ||
Theorem | lnrlnm 36702 | Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝐴 ∈ LNoeR → (ringLMod‘𝐴) ∈ LNoeM) | ||
Theorem | islnr2 36703* | Property of being a left-Noetherian ring in terms of finite generation of ideals (the usual "pure ring theory" definition). (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝑁 = (RSpan‘𝑅) ⇒ ⊢ (𝑅 ∈ LNoeR ↔ (𝑅 ∈ Ring ∧ ∀𝑖 ∈ 𝑈 ∃𝑔 ∈ (𝒫 𝐵 ∩ Fin)𝑖 = (𝑁‘𝑔))) | ||
Theorem | islnr3 36704 | Relate left-Noetherian rings to Noetherian-type closure property of the left ideal system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ LNoeR ↔ (𝑅 ∈ Ring ∧ 𝑈 ∈ (NoeACS‘𝐵))) | ||
Theorem | lnr2i 36705* | Given an ideal in a left-Noetherian ring, there is a finite subset which generates it. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝑁 = (RSpan‘𝑅) ⇒ ⊢ ((𝑅 ∈ LNoeR ∧ 𝐼 ∈ 𝑈) → ∃𝑔 ∈ (𝒫 𝐼 ∩ Fin)𝐼 = (𝑁‘𝑔)) | ||
Theorem | lpirlnr 36706 | Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ LNoeR) | ||
Theorem | lnrfrlm 36707 | Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015.) |
⊢ 𝑌 = (𝑅 freeLMod 𝐼) ⇒ ⊢ ((𝑅 ∈ LNoeR ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM) | ||
Theorem | lnrfg 36708 | Finitely-generated modules over a Noetherian ring, being homomorphic images of free modules, are Noetherian. (Contributed by Stefan O'Rear, 7-Feb-2015.) |
⊢ 𝑆 = (Scalar‘𝑀) ⇒ ⊢ ((𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR) → 𝑀 ∈ LNoeM) | ||
Theorem | lnrfgtr 36709 | A submodule of a finitely generated module over a Noetherian ring is finitely generated. Often taken as the definition of Noetherian ring. (Contributed by Stefan O'Rear, 7-Feb-2015.) |
⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑈 = (LSubSp‘𝑀) & ⊢ 𝑁 = (𝑀 ↾s 𝑃) ⇒ ⊢ ((𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ∧ 𝑃 ∈ 𝑈) → 𝑁 ∈ LFinGen) | ||
Syntax | cldgis 36710 | The leading ideal sequence used in the Hilbert Basis Theorem. |
class ldgIdlSeq | ||
Definition | df-ldgis 36711* | 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 36719. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))}))) | ||
Theorem | hbtlem1 36712* | Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) = {𝑗 ∣ ∃𝑘 ∈ 𝐼 ((𝐷‘𝑘) ≤ 𝑋 ∧ 𝑗 = ((coe1‘𝑘)‘𝑋))}) | ||
Theorem | hbtlem2 36713 | Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝑇 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) ∈ 𝑇) | ||
Theorem | hbtlem7 36714 | Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝑇 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝑆‘𝐼):ℕ0⟶𝑇) | ||
Theorem | hbtlem4 36715 | The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ ℕ0) & ⊢ (𝜑 → 𝑌 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐼)‘𝑌)) | ||
Theorem | hbtlem3 36716 | The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝐽 ∈ 𝑈) & ⊢ (𝜑 → 𝐼 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐽)‘𝑋)) | ||
Theorem | hbtlem5 36717* | The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝐽 ∈ 𝑈) & ⊢ (𝜑 → 𝐼 ⊆ 𝐽) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ0 ((𝑆‘𝐽)‘𝑥) ⊆ ((𝑆‘𝐼)‘𝑥)) ⇒ ⊢ (𝜑 → 𝐼 = 𝐽) | ||
Theorem | hbtlem6 36718* | 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 36719 | 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 36720 | Extend class notation with the class of monic polynomials. |
class Monic | ||
Syntax | cplylt 36721 | Extend class notatin with the class of limited-degree polynomials. |
class Poly< | ||
Definition | df-mnc 36722* | Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ Monic = (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1}) | ||
Definition | df-plylt 36723* | Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.) |
⊢ Poly< = (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)}) | ||
Theorem | dgrsub2 36724 | 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‘(𝐹 ∘𝑓 − 𝐺)) < 𝑁) | ||
Theorem | elmnc 36725 | Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) ↔ (𝑃 ∈ (Poly‘𝑆) ∧ ((coeff‘𝑃)‘(deg‘𝑃)) = 1)) | ||
Theorem | mncply 36726 | A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ∈ (Poly‘𝑆)) | ||
Theorem | mnccoe 36727 | A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) → ((coeff‘𝑃)‘(deg‘𝑃)) = 1) | ||
Theorem | mncn0 36728 | A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ≠ 0𝑝) | ||
Syntax | cdgraa 36729 | Extend class notation to include the degree function for algebraic numbers. |
class degAA | ||
Syntax | cmpaa 36730 | Extend class notation to include the minimal polynomial for an algebraic number. |
class minPolyAA | ||
Definition | df-dgraa 36731* | 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 36732* | 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 36733* | 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 36734* | 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 36735 | Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → (degAA‘𝐴) ∈ ℕ) | ||
Theorem | dgraaf 36736 | 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 36737 | 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 36738 | 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 36739* | 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 36740* | 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 36741 | 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 36742 | Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → (minPolyAA‘𝐴) ∈ (Poly‘ℚ)) | ||
Theorem | mpaadgr 36743 | Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → (deg‘(minPolyAA‘𝐴)) = (degAA‘𝐴)) | ||
Theorem | mpaaroot 36744 | 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 36745 | Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → ((coeff‘(minPolyAA‘𝐴))‘(degAA‘𝐴)) = 1) | ||
Syntax | citgo 36746 | Extend class notation with the integral-over predicate. |
class IntgOver | ||
Syntax | cza 36747 | Extend class notation with the class of algebraic integers. |
class ℤ | ||
Definition | df-itgo 36748* | 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 36751. 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 36749 | 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 36750* | Value of the integral-over function. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ (𝑆 ⊆ ℂ → (IntgOver‘𝑆) = {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑆)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}) | ||
Theorem | aaitgo 36751 | The standard algebraic numbers 𝔸 are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝔸 = (IntgOver‘ℚ) | ||
Theorem | itgoss 36752 | An integral element is integral over a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (IntgOver‘𝑆) ⊆ (IntgOver‘𝑇)) | ||
Theorem | itgocn 36753 | All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ (IntgOver‘𝑆) ⊆ ℂ | ||
Theorem | cnsrexpcl 36754 | Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑋↑𝑌) ∈ 𝑆) | ||
Theorem | fsumcnsrcl 36755* | Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) | ||
Theorem | cnsrplycl 36756 | Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝑃 ∈ (Poly‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝑃‘𝑋) ∈ 𝑆) | ||
Theorem | rgspnval 36757* | 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 36758 | The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅)) & ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴)) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑅)) | ||
Theorem | rgspnssid 36759 | The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅)) & ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝑈) | ||
Theorem | rgspnmin 36760 | 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 36761 | The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑆 = ((RingSpan‘𝑅)‘𝐴)) ⇒ ⊢ (𝜑 → 𝑆 = 𝐴) | ||
Theorem | rngunsnply 36762* | 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 36763* | Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝜑 → 𝐹 = (𝑗 ∈ 𝑆 ↦ if(𝑗 = 𝐾, 1, 0))) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑆) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑖 ∈ 𝑆 ((𝐹‘𝑖) · 𝐵) = ⦋𝐾 / 𝑖⦌𝐵) | ||
Syntax | cmend 36764 | Syntax for module endomorphism algebra. |
class MEndo | ||
Definition | df-mend 36765* | Define the endomorphism algebra of a module. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ MEndo = (𝑚 ∈ V ↦ ⦋(𝑚 LMHom 𝑚) / 𝑏⦌({〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘𝑓 (+g‘𝑚)𝑦))〉, 〈(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx), (Scalar‘𝑚)〉, 〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑚)𝑦))〉})) | ||
Theorem | algstr 36766 | Lemma to shorten proofs of algbase 36767 through algvsca 36771. (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 36767 | 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 36768 | 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 36769 | 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 36770 | 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 36771 | 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 36772* | Value of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐵 = (𝑀 LMHom 𝑀) & ⊢ + = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 (+g‘𝑀)𝑦)) & ⊢ × = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ · = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑀)𝑦)) ⇒ ⊢ (𝑀 ∈ 𝑋 → (MEndo‘𝑀) = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉})) | ||
Theorem | mendbas 36773 | Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) ⇒ ⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) | ||
Theorem | mendplusgfval 36774* | Addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ + = (+g‘𝑀) ⇒ ⊢ (+g‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦)) | ||
Theorem | mendplusg 36775 | A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ + = (+g‘𝑀) & ⊢ ✚ = (+g‘𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ✚ 𝑌) = (𝑋 ∘𝑓 + 𝑌)) | ||
Theorem | mendmulrfval 36776* | Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (.r‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) | ||
Theorem | mendmulr 36777 | A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = (.r‘𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑋 ∘ 𝑌)) | ||
Theorem | mendsca 36778 | 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 36779* | Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐸 = (Base‘𝑀) ⇒ ⊢ ( ·𝑠 ‘𝐴) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦)) | ||
Theorem | mendvsca 36780 | A specific scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐸 = (Base‘𝑀) & ⊢ ∙ = ( ·𝑠 ‘𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∙ 𝑌) = ((𝐸 × {𝑋}) ∘𝑓 · 𝑌)) | ||
Theorem | mendring 36781 | The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) ⇒ ⊢ (𝑀 ∈ LMod → 𝐴 ∈ Ring) | ||
Theorem | mendlmod 36782 | The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ LMod) | ||
Theorem | mendassa 36783 | The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ AssAlg) | ||
Syntax | csdrg 36784 | Syntax for subfields (sub-division-rings). |
class SubDRing | ||
Definition | df-sdrg 36785* | A sub-division-ring is a subset of a division ring's set which is a division ring under the induced operation. If the overring is commutative this is a field; no special consideration is made of the fields in the center of a skew field. (Contributed by Stefan O'Rear, 3-Oct-2015.) |
⊢ SubDRing = (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing}) | ||
Theorem | issdrg 36786 | Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015.) |
⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing)) | ||
Theorem | issdrg2 36787* | Property of a division subring (closure version). (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐼 = (invr‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑆 ∖ { 0 })(𝐼‘𝑥) ∈ 𝑆)) | ||
Theorem | acsfn1p 36788* | Construction of a closure rule from a one-parameter partial operation. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎} ∈ (ACS‘𝑋)) | ||
Theorem | subrgacs 36789 | Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (SubRing‘𝑅) ∈ (ACS‘𝐵)) | ||
Theorem | sdrgacs 36790 | Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → (SubDRing‘𝑅) ∈ (ACS‘𝐵)) | ||
Theorem | cntzsdrg 36791 | Centralizers in division rings/fields are subfields. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubDRing‘𝑅)) | ||
Theorem | idomrootle 36792* | 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 36793* | 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 36794 | 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 36795* | 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 36796 | 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 36797 | 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 36798 | 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 36799 | Syntax for the sequence of cyclotomic polynomials. |
class CytP | ||
Definition | df-cytp 36800* | 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))‘𝑟))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |