Home | Metamath
Proof Explorer Theorem List (p. 398 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfacbasgrp 39701 | A choice equivalent in abstract algebra: All nonempty sets admit a group structure. From http://mathoverflow.net/a/12988. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
⊢ (CHOICE ↔ (Base “ Grp) = (V ∖ {∅})) | ||
Syntax | clnr 39702 | Extend class notation with the class of left Noetherian rings. |
class LNoeR | ||
Definition | df-lnr 39703 | A ring is left-Noetherian iff it is Noetherian as a left module over itself. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ LNoeR = {𝑎 ∈ Ring ∣ (ringLMod‘𝑎) ∈ LNoeM} | ||
Theorem | islnr 39704 | Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝐴 ∈ LNoeR ↔ (𝐴 ∈ Ring ∧ (ringLMod‘𝐴) ∈ LNoeM)) | ||
Theorem | lnrring 39705 | Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝐴 ∈ LNoeR → 𝐴 ∈ Ring) | ||
Theorem | lnrlnm 39706 | Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝐴 ∈ LNoeR → (ringLMod‘𝐴) ∈ LNoeM) | ||
Theorem | islnr2 39707* | 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 39708 | 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 39709* | 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 39710 | Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ LNoeR) | ||
Theorem | lnrfrlm 39711 | Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015.) |
⊢ 𝑌 = (𝑅 freeLMod 𝐼) ⇒ ⊢ ((𝑅 ∈ LNoeR ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM) | ||
Theorem | lnrfg 39712 | 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 39713 | 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 39714 | The leading ideal sequence used in the Hilbert Basis Theorem. |
class ldgIdlSeq | ||
Definition | df-ldgis 39715* | 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 39723. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))}))) | ||
Theorem | hbtlem1 39716* | Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) = {𝑗 ∣ ∃𝑘 ∈ 𝐼 ((𝐷‘𝑘) ≤ 𝑋 ∧ 𝑗 = ((coe1‘𝑘)‘𝑋))}) | ||
Theorem | hbtlem2 39717 | Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝑇 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) ∈ 𝑇) | ||
Theorem | hbtlem7 39718 | Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝑇 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝑆‘𝐼):ℕ0⟶𝑇) | ||
Theorem | hbtlem4 39719 | The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ ℕ0) & ⊢ (𝜑 → 𝑌 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐼)‘𝑌)) | ||
Theorem | hbtlem3 39720 | The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝐽 ∈ 𝑈) & ⊢ (𝜑 → 𝐼 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐽)‘𝑋)) | ||
Theorem | hbtlem5 39721* | The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝐽 ∈ 𝑈) & ⊢ (𝜑 → 𝐼 ⊆ 𝐽) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ0 ((𝑆‘𝐽)‘𝑥) ⊆ ((𝑆‘𝐼)‘𝑥)) ⇒ ⊢ (𝜑 → 𝐼 = 𝐽) | ||
Theorem | hbtlem6 39722* | 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 39723 | 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 39724 | Extend class notation with the class of monic polynomials. |
class Monic | ||
Syntax | cplylt 39725 | Extend class notatin with the class of limited-degree polynomials. |
class Poly< | ||
Definition | df-mnc 39726* | Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ Monic = (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1}) | ||
Definition | df-plylt 39727* | Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.) |
⊢ Poly< = (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)}) | ||
Theorem | dgrsub2 39728 | 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 39729 | Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) ↔ (𝑃 ∈ (Poly‘𝑆) ∧ ((coeff‘𝑃)‘(deg‘𝑃)) = 1)) | ||
Theorem | mncply 39730 | A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ∈ (Poly‘𝑆)) | ||
Theorem | mnccoe 39731 | A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) → ((coeff‘𝑃)‘(deg‘𝑃)) = 1) | ||
Theorem | mncn0 39732 | A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ≠ 0𝑝) | ||
Syntax | cdgraa 39733 | Extend class notation to include the degree function for algebraic numbers. |
class degAA | ||
Syntax | cmpaa 39734 | Extend class notation to include the minimal polynomial for an algebraic number. |
class minPolyAA | ||
Definition | df-dgraa 39735* | 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 39736* | 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 39737* | 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 39738* | 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 39739 | Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → (degAA‘𝐴) ∈ ℕ) | ||
Theorem | dgraaf 39740 | 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 39741 | 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 39742 | 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 39743* | 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 39744* | 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 39745 | 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 39746 | Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → (minPolyAA‘𝐴) ∈ (Poly‘ℚ)) | ||
Theorem | mpaadgr 39747 | Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → (deg‘(minPolyAA‘𝐴)) = (degAA‘𝐴)) | ||
Theorem | mpaaroot 39748 | 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 39749 | Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → ((coeff‘(minPolyAA‘𝐴))‘(degAA‘𝐴)) = 1) | ||
Syntax | citgo 39750 | Extend class notation with the integral-over predicate. |
class IntgOver | ||
Syntax | cza 39751 | Extend class notation with the class of algebraic integers. |
class ℤ | ||
Definition | df-itgo 39752* | 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 39755. 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 39753 | 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 39754* | Value of the integral-over function. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ (𝑆 ⊆ ℂ → (IntgOver‘𝑆) = {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑆)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}) | ||
Theorem | aaitgo 39755 | The standard algebraic numbers 𝔸 are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝔸 = (IntgOver‘ℚ) | ||
Theorem | itgoss 39756 | An integral element is integral over a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (IntgOver‘𝑆) ⊆ (IntgOver‘𝑇)) | ||
Theorem | itgocn 39757 | All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ (IntgOver‘𝑆) ⊆ ℂ | ||
Theorem | cnsrexpcl 39758 | Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑋↑𝑌) ∈ 𝑆) | ||
Theorem | fsumcnsrcl 39759* | Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) | ||
Theorem | cnsrplycl 39760 | Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝑃 ∈ (Poly‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝑃‘𝑋) ∈ 𝑆) | ||
Theorem | rgspnval 39761* | 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 39762 | The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅)) & ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴)) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑅)) | ||
Theorem | rgspnssid 39763 | The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅)) & ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝑈) | ||
Theorem | rgspnmin 39764 | 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 39765 | The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑆 = ((RingSpan‘𝑅)‘𝐴)) ⇒ ⊢ (𝜑 → 𝑆 = 𝐴) | ||
Theorem | rngunsnply 39766* | 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 39767* | Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝜑 → 𝐹 = (𝑗 ∈ 𝑆 ↦ if(𝑗 = 𝐾, 1, 0))) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑆) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑖 ∈ 𝑆 ((𝐹‘𝑖) · 𝐵) = ⦋𝐾 / 𝑖⦌𝐵) | ||
Syntax | cmend 39768 | Syntax for module endomorphism algebra. |
class MEndo | ||
Definition | df-mend 39769* | 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 39770 | Lemma to shorten proofs of algbase 39771 through algvsca 39775. (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 39771 | 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 39772 | 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 39773 | 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 39774 | 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 39775 | 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 39776* | 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 39777 | Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) ⇒ ⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) | ||
Theorem | mendplusgfval 39778* | 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 39779 | A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ + = (+g‘𝑀) & ⊢ ✚ = (+g‘𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌)) | ||
Theorem | mendmulrfval 39780* | 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 39781 | A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = (.r‘𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑋 ∘ 𝑌)) | ||
Theorem | mendsca 39782 | 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 39783* | 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 39784 | 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 39785 | The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) ⇒ ⊢ (𝑀 ∈ LMod → 𝐴 ∈ Ring) | ||
Theorem | mendlmod 39786 | The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ LMod) | ||
Theorem | mendassa 39787 | The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ AssAlg) | ||
Theorem | idomrootle 39788* | 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 39789* | 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 39790 | 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 39791* | 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 39792 | 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 39793 | 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 39794 | 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 39795 | Syntax for the sequence of cyclotomic polynomials. |
class CytP | ||
Definition | df-cytp 39796* | 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 39797 | 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 39798 | 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 39799 | Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝑈 = (mulGrp‘𝑃) ⇒ ⊢ (𝑅 ∈ NzRing → 𝑀 ∈ (SubMnd‘𝑈)) | ||
Theorem | deg1mhm 39800 | 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 𝑁)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |