P. 432 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43101-43200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isnumbasgrplem3 43101	Every nonempty numerable set can be given the structure of an Abelian group, either a finite cyclic group or a vector space over Z/2Z. (Contributed by Stefan O'Rear, 10-Jul-2015.)
⊢ ((𝑆 ∈ dom card ∧ 𝑆 ≠ ∅) → 𝑆 ∈ (Base “ Abel))
Theorem	isnumbasabl 43102	A set is numerable iff it and its Hartogs number can be jointly given the structure of an Abelian group. (Contributed by Stefan O'Rear, 9-Jul-2015.)
⊢ (𝑆 ∈ dom card ↔ (𝑆 ∪ (har‘𝑆)) ∈ (Base “ Abel))
Theorem	isnumbasgrp 43103	A set is numerable iff it and its Hartogs number can be jointly given the structure of a group. (Contributed by Stefan O'Rear, 9-Jul-2015.)
⊢ (𝑆 ∈ dom card ↔ (𝑆 ∪ (har‘𝑆)) ∈ (Base “ Grp))
Theorem	dfacbasgrp 43104	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 ∖ {∅}))
21.33.41  Noetherian rings and left modules II
Syntax	clnr 43105	Extend class notation with the class of left Noetherian rings.
class LNoeR
Definition	df-lnr 43106	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 43107	Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ LNoeR ↔ (𝐴 ∈ Ring ∧ (ringLMod‘𝐴) ∈ LNoeM))
Theorem	lnrring 43108	Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ LNoeR → 𝐴 ∈ Ring)
Theorem	lnrlnm 43109	Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ LNoeR → (ringLMod‘𝐴) ∈ LNoeM)
Theorem	islnr2 43110*	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 43111	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 43112*	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 43113	Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ LNoeR)
Theorem	lnrfrlm 43114	Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015.)
⊢ 𝑌 = (𝑅 freeLMod 𝐼)    ⇒   ⊢ ((𝑅 ∈ LNoeR ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM)
Theorem	lnrfg 43115	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 43116	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)
21.33.42  Hilbert's Basis Theorem
Syntax	cldgis 43117	The leading ideal sequence used in the Hilbert Basis Theorem.
class ldgIdlSeq
Definition	df-ldgis 43118*	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 43126. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 (((deg1‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))})))
Theorem	hbtlem1 43119*	Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) = {𝑗 ∣ ∃𝑘 ∈ 𝐼 ((𝐷‘𝑘) ≤ 𝑋 ∧ 𝑗 = ((coe1‘𝑘)‘𝑋))})
Theorem	hbtlem2 43120	Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ 𝑇 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) ∈ 𝑇)
Theorem	hbtlem7 43121	Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ 𝑇 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝑆‘𝐼):ℕ0⟶𝑇)
Theorem	hbtlem4 43122	The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑌 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐼)‘𝑌))
Theorem	hbtlem3 43123	The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐼 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐽)‘𝑋))
Theorem	hbtlem5 43124*	The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐼 ⊆ 𝐽)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ0 ((𝑆‘𝐽)‘𝑥) ⊆ ((𝑆‘𝐼)‘𝑥))    ⇒   ⊢ (𝜑 → 𝐼 = 𝐽)
Theorem	hbtlem6 43125*	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 43126	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)
21.33.43  Additional material on polynomials [DEPRECATED]
Syntax	cmnc 43127	Extend class notation with the class of monic polynomials.
class Monic
Syntax	cplylt 43128	Extend class notation with the class of limited-degree polynomials.
class Poly<
Definition	df-mnc 43129*	Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ Monic = (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1})
Definition	df-plylt 43130*	Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.)
⊢ Poly< = (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)})
Theorem	dgrsub2 43131	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 43132	Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) ↔ (𝑃 ∈ (Poly‘𝑆) ∧ ((coeff‘𝑃)‘(deg‘𝑃)) = 1))
Theorem	mncply 43133	A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ∈ (Poly‘𝑆))
Theorem	mnccoe 43134	A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) → ((coeff‘𝑃)‘(deg‘𝑃)) = 1)
Theorem	mncn0 43135	A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ≠ 0𝑝)
21.33.44  Degree and minimal polynomial of algebraic numbers
Syntax	cdgraa 43136	Extend class notation to include the degree function for algebraic numbers.
class degAA
Syntax	cmpaa 43137	Extend class notation to include the minimal polynomial for an algebraic number.
class minPolyAA
Definition	df-dgraa 43138*	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 43139*	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 43140*	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 43141*	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 43142	Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → (degAA‘𝐴) ∈ ℕ)
Theorem	dgraaf 43143	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 43144	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 43145	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 43146*	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 43147*	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 43148	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 43149	Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → (minPolyAA‘𝐴) ∈ (Poly‘ℚ))
Theorem	mpaadgr 43150	Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → (deg‘(minPolyAA‘𝐴)) = (degAA‘𝐴))
Theorem	mpaaroot 43151	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 43152	Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → ((coeff‘(minPolyAA‘𝐴))‘(degAA‘𝐴)) = 1)
21.33.45  Algebraic integers I
Syntax	citgo 43153	Extend class notation with the integral-over predicate.
class IntgOver
Syntax	cza 43154	Extend class notation with the class of algebraic integers.
class ℤ
Definition	df-itgo 43155*	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 43158. 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 43156	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 43157*	Value of the integral-over function. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ (𝑆 ⊆ ℂ → (IntgOver‘𝑆) = {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑆)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
Theorem	aaitgo 43158	The standard algebraic numbers 𝔸 are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝔸 = (IntgOver‘ℚ)
Theorem	itgoss 43159	An integral element is integral over a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (IntgOver‘𝑆) ⊆ (IntgOver‘𝑇))
Theorem	itgocn 43160	All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ (IntgOver‘𝑆) ⊆ ℂ
Theorem	cnsrexpcl 43161	Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑋↑𝑌) ∈ 𝑆)
Theorem	fsumcnsrcl 43162*	Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)
Theorem	cnsrplycl 43163	Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld))    &   ⊢ (𝜑 → 𝑃 ∈ (Poly‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → (𝑃‘𝑋) ∈ 𝑆)
Theorem	rgspnid 43164	The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑆 = ((RingSpan‘𝑅)‘𝐴))    ⇒   ⊢ (𝜑 → 𝑆 = 𝐴)
Theorem	rngunsnply 43165*	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 43166*	Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝜑 → 𝐹 = (𝑗 ∈ 𝑆 ↦ if(𝑗 = 𝐾, 1, 0)))    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑆) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑖 ∈ 𝑆 ((𝐹‘𝑖) · 𝐵) = ⦋𝐾 / 𝑖⦌𝐵)
21.33.46  Endomorphism algebra
Syntax	cmend 43167	Syntax for module endomorphism algebra.
class MEndo
Definition	df-mend 43168*	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 43169	Lemma to shorten proofs of algbase 43170 through algvsca 43174. (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 43170	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 43171	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 43172	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 43173	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 43174	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 43175*	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 43176	Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    ⇒   ⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴)
Theorem	mendplusgfval 43177*	Addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ (+g‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦))
Theorem	mendplusg 43178	A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ + = (+g‘𝑀)    &   ⊢ ✚ = (+g‘𝐴)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌))
Theorem	mendmulrfval 43179*	Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (.r‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))
Theorem	mendmulr 43180	A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = (.r‘𝐴)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑋 ∘ 𝑌))
Theorem	mendsca 43181	The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    ⇒   ⊢ 𝑆 = (Scalar‘𝐴)
Theorem	mendvscafval 43182*	Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐸 = (Base‘𝑀)    ⇒   ⊢ ( ·𝑠 ‘𝐴) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦))
Theorem	mendvsca 43183	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 43184	The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    ⇒   ⊢ (𝑀 ∈ LMod → 𝐴 ∈ Ring)
Theorem	mendlmod 43185	The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ LMod)
Theorem	mendassa 43186	The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ AssAlg)
21.33.47  Cyclic groups and order
Theorem	idomodle 43187*	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 43188	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 43189*	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 43190	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 43191	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 43192	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 / 𝑁)) ∈ (◡𝑂 “ {𝑁}))
21.33.48  Cyclotomic polynomials
Syntax	ccytp 43193	Syntax for the sequence of cyclotomic polynomials.
class CytP
Definition	df-cytp 43194*	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	mon1psubm 43195	Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 𝑈 = (mulGrp‘𝑃)    ⇒   ⊢ (𝑅 ∈ NzRing → 𝑀 ∈ (SubMnd‘𝑈))
Theorem	deg1mhm 43196	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 43197	Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ CytP Fn ℕ
Theorem	cytpval 43198*	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 (𝑟 ∈ (◡𝑂 “ {𝑁}) ↦ (𝑋 − (𝐴‘𝑟)))))
21.33.49  Miscellaneous topology
Theorem	fgraphopab 43199*	Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)})
Theorem	fgraphxp 43200*	Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {𝑥 ∈ (𝐴 × 𝐵) ∣ (𝐹‘(1st ‘𝑥)) = (2nd ‘𝑥)})