P. 410 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40901-41000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	islmodfg 40901*	Property of a finitely generated left module. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑊 ∈ LFinGen ↔ ∃𝑏 ∈ 𝒫 𝐵(𝑏 ∈ Fin ∧ (𝑁‘𝑏) = 𝐵)))
Theorem	islssfg 40902*	Property of a finitely generated left (sub)module. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑋 ∈ LFinGen ↔ ∃𝑏 ∈ 𝒫 𝑈(𝑏 ∈ Fin ∧ (𝑁‘𝑏) = 𝑈)))
Theorem	islssfg2 40903*	Property of a finitely generated left (sub)module, with a relaxed constraint on the spanning vectors. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑋 ∈ LFinGen ↔ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑁‘𝑏) = 𝑈))
Theorem	islssfgi 40904	Finitely spanned subspaces are finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑋 = (𝑊 ↾s (𝑁‘𝐵))    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin) → 𝑋 ∈ LFinGen)
Theorem	fglmod 40905	Finitely generated left modules are left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝑀 ∈ LFinGen → 𝑀 ∈ LMod)
Theorem	lsmfgcl 40906	The sum of two finitely generated submodules is finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑈 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐷 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐸 = (𝑊 ↾s 𝐵)    &   ⊢ 𝐹 = (𝑊 ↾s (𝐴 ⊕ 𝐵))    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ LFinGen)    &   ⊢ (𝜑 → 𝐸 ∈ LFinGen)    ⇒   ⊢ (𝜑 → 𝐹 ∈ LFinGen)
20.29.38  Noetherian left modules I
Syntax	clnm 40907	Extend class notation with the class of Noetherian left modules.
class LNoeM
Definition	df-lnm 40908*	A left-module is Noetherian iff it is hereditarily finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ LNoeM = {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤 ↾s 𝑖) ∈ LFinGen}
Theorem	islnm 40909*	Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ 𝑆 = (LSubSp‘𝑀)    ⇒   ⊢ (𝑀 ∈ LNoeM ↔ (𝑀 ∈ LMod ∧ ∀𝑖 ∈ 𝑆 (𝑀 ↾s 𝑖) ∈ LFinGen))
Theorem	islnm2 40910*	Property of being a Noetherian left module with finite generation expanded in terms of spans. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑆 = (LSubSp‘𝑀)    &   ⊢ 𝑁 = (LSpan‘𝑀)    ⇒   ⊢ (𝑀 ∈ LNoeM ↔ (𝑀 ∈ LMod ∧ ∀𝑖 ∈ 𝑆 ∃𝑔 ∈ (𝒫 𝐵 ∩ Fin)𝑖 = (𝑁‘𝑔)))
Theorem	lnmlmod 40911	A Noetherian left module is a left module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ (𝑀 ∈ LNoeM → 𝑀 ∈ LMod)
Theorem	lnmlssfg 40912	A submodule of Noetherian module is finitely generated. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑀)    &   ⊢ 𝑅 = (𝑀 ↾s 𝑈)    ⇒   ⊢ ((𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆) → 𝑅 ∈ LFinGen)
Theorem	lnmlsslnm 40913	All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑀)    &   ⊢ 𝑅 = (𝑀 ↾s 𝑈)    ⇒   ⊢ ((𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆) → 𝑅 ∈ LNoeM)
Theorem	lnmfg 40914	A Noetherian left module is finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ (𝑀 ∈ LNoeM → 𝑀 ∈ LFinGen)
Theorem	kercvrlsm 40915	The domain of a linear function is the subspace sum of the kernel and any subspace which covers the range. (Contributed by Stefan O'Rear, 24-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ 𝑈 = (LSubSp‘𝑆)    &   ⊢ ⊕ = (LSSum‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇))    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐹 “ 𝐷) = ran 𝐹)    ⇒   ⊢ (𝜑 → (𝐾 ⊕ 𝐷) = 𝐵)
Theorem	lmhmfgima 40916	A homomorphism maps finitely generated submodules to finitely generated submodules. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑇 ↾s (𝐹 “ 𝐴))    &   ⊢ 𝑋 = (𝑆 ↾s 𝐴)    &   ⊢ 𝑈 = (LSubSp‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ LFinGen)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇))    ⇒   ⊢ (𝜑 → 𝑌 ∈ LFinGen)
Theorem	lnmepi 40917	Epimorphic images of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐵 = (Base‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵) → 𝑇 ∈ LNoeM)
Theorem	lmhmfgsplit 40918	If the kernel and range of a homomorphism of left modules are finitely generated, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑈 = (𝑆 ↾s 𝐾)    &   ⊢ 𝑉 = (𝑇 ↾s ran 𝐹)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen) → 𝑆 ∈ LFinGen)
Theorem	lmhmlnmsplit 40919	If the kernel and range of a homomorphism of left modules are Noetherian, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Revised by Stefan O'Rear, 12-Jun-2015.)
⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑈 = (𝑆 ↾s 𝐾)    &   ⊢ 𝑉 = (𝑇 ↾s ran 𝐹)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) → 𝑆 ∈ LNoeM)
Theorem	lnmlmic 40920	Noetherian is an invariant property of modules. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝑅 ≃𝑚 𝑆 → (𝑅 ∈ LNoeM ↔ 𝑆 ∈ LNoeM))
20.29.39  Addenda for structure powers
Theorem	pwssplit4 40921*	Splitting for structure powers 4: maps isomorphically onto the other half. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐸 = (𝑅 ↑s (𝐴 ∪ 𝐵))    &   ⊢ 𝐺 = (Base‘𝐸)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐾 = {𝑦 ∈ 𝐺 ∣ (𝑦 ↾ 𝐴) = (𝐴 × { 0 })}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ↾ 𝐵))    &   ⊢ 𝐶 = (𝑅 ↑s 𝐴)    &   ⊢ 𝐷 = (𝑅 ↑s 𝐵)    &   ⊢ 𝐿 = (𝐸 ↾s 𝐾)    ⇒   ⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐹 ∈ (𝐿 LMIso 𝐷))
Theorem	filnm 40922	Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ Fin) → 𝑊 ∈ LNoeM)
Theorem	pwslnmlem0 40923	Zeroeth powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s ∅)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑌 ∈ LNoeM)
Theorem	pwslnmlem1 40924*	First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s {𝑖})    ⇒   ⊢ (𝑊 ∈ LNoeM → 𝑌 ∈ LNoeM)
Theorem	pwslnmlem2 40925	A sum of powers is Noetherian. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 = (𝑊 ↑s 𝐴)    &   ⊢ 𝑌 = (𝑊 ↑s 𝐵)    &   ⊢ 𝑍 = (𝑊 ↑s (𝐴 ∪ 𝐵))    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑋 ∈ LNoeM)    &   ⊢ (𝜑 → 𝑌 ∈ LNoeM)    ⇒   ⊢ (𝜑 → 𝑍 ∈ LNoeM)
Theorem	pwslnm 40926	Finite powers of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s 𝐼)    ⇒   ⊢ ((𝑊 ∈ LNoeM ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM)
20.29.40  Every set admits a group structure iff choice
Theorem	unxpwdom3 40927*	Weaker version of unxpwdom 9357 where a function is required only to be cancellative, not an injection. 𝐷 and 𝐵 are to be thought of as "large" "horizonal" sets, the others as "small". Because the operator is row-wise injective, but the whole row cannot inject into 𝐴, each row must hit an element of 𝐵; by column injectivity, each row can be identified in at least one way by the 𝐵 element that it hits and the column in which it is hit. (Contributed by Stefan O'Rear, 8-Jul-2015.) MOVABLE
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵))    &   ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐))    &   ⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ (𝑎 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))    &   ⊢ (𝜑 → ¬ 𝐷 ≼ 𝐴)    ⇒   ⊢ (𝜑 → 𝐶 ≼* (𝐷 × 𝐵))
Theorem	pwfi2f1o 40928*	The pw2f1o 8873 bijection relates finitely supported indicator functions on a two-element set to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Revised by AV, 14-Jun-2020.)
⊢ 𝑆 = {𝑦 ∈ (2o ↑m 𝐴) ∣ 𝑦 finSupp ∅}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ (◡𝑥 “ {1o}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹:𝑆–1-1-onto→(𝒫 𝐴 ∩ Fin))
Theorem	pwfi2en 40929*	Finitely supported indicator functions are equinumerous to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Revised by AV, 14-Jun-2020.)
⊢ 𝑆 = {𝑦 ∈ (2o ↑m 𝐴) ∣ 𝑦 finSupp ∅}    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝑆 ≈ (𝒫 𝐴 ∩ Fin))
Theorem	frlmpwfi 40930	Formal linear combinations over Z/2Z are equivalent to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Proof shortened by AV, 14-Jun-2020.)
⊢ 𝑅 = (ℤ/nℤ‘2)    &   ⊢ 𝑌 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐵 ≈ (𝒫 𝐼 ∩ Fin))
Theorem	gicabl 40931	Being Abelian is a group invariant. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.)
⊢ (𝐺 ≃𝑔 𝐻 → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))
Theorem	imasgim 40932	A relabeling of the elements of a group induces an isomorphism to the relabeled group. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) (Revised by Mario Carneiro, 11-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpIso 𝑈))
Theorem	isnumbasgrplem1 40933	A set which is equipollent to the base set of a definable Abelian group is the base set of some (relabeled) Abelian group. (Contributed by Stefan O'Rear, 8-Jul-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Abel ∧ 𝐶 ≈ 𝐵) → 𝐶 ∈ (Base “ Abel))
Theorem	harn0 40934	The Hartogs number of a set is never zero. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.)
⊢ (𝑆 ∈ 𝑉 → (har‘𝑆) ≠ ∅)
Theorem	numinfctb 40935	A numerable infinite set contains a countable subset. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.)
⊢ ((𝑆 ∈ dom card ∧ ¬ 𝑆 ∈ Fin) → ω ≼ 𝑆)
Theorem	isnumbasgrplem2 40936	If the (to be thought of as disjoint, although the proof does not require this) union of a set and its Hartogs number supports a group structure (more generally, a cancellative magma), then the set must be numerable. (Contributed by Stefan O'Rear, 9-Jul-2015.)
⊢ ((𝑆 ∪ (har‘𝑆)) ∈ (Base “ Grp) → 𝑆 ∈ dom card)
Theorem	isnumbasgrplem3 40937	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 40938	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 40939	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 40940	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 ∖ {∅}))
20.29.41  Noetherian rings and left modules II
Syntax	clnr 40941	Extend class notation with the class of left Noetherian rings.
class LNoeR
Definition	df-lnr 40942	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 40943	Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ LNoeR ↔ (𝐴 ∈ Ring ∧ (ringLMod‘𝐴) ∈ LNoeM))
Theorem	lnrring 40944	Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ LNoeR → 𝐴 ∈ Ring)
Theorem	lnrlnm 40945	Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ LNoeR → (ringLMod‘𝐴) ∈ LNoeM)
Theorem	islnr2 40946*	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 40947	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 40948*	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 40949	Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ LNoeR)
Theorem	lnrfrlm 40950	Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015.)
⊢ 𝑌 = (𝑅 freeLMod 𝐼)    ⇒   ⊢ ((𝑅 ∈ LNoeR ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM)
Theorem	lnrfg 40951	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 40952	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)
20.29.42  Hilbert's Basis Theorem
Syntax	cldgis 40953	The leading ideal sequence used in the Hilbert Basis Theorem.
class ldgIdlSeq
Definition	df-ldgis 40954*	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 40962. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))})))
Theorem	hbtlem1 40955*	Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ 𝐷 = ( deg1 ‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) = {𝑗 ∣ ∃𝑘 ∈ 𝐼 ((𝐷‘𝑘) ≤ 𝑋 ∧ 𝑗 = ((coe1‘𝑘)‘𝑋))})
Theorem	hbtlem2 40956	Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ 𝑇 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) ∈ 𝑇)
Theorem	hbtlem7 40957	Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ 𝑇 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝑆‘𝐼):ℕ0⟶𝑇)
Theorem	hbtlem4 40958	The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑌 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐼)‘𝑌))
Theorem	hbtlem3 40959	The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐼 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐽)‘𝑋))
Theorem	hbtlem5 40960*	The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐼 ⊆ 𝐽)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ0 ((𝑆‘𝐽)‘𝑥) ⊆ ((𝑆‘𝐼)‘𝑥))    ⇒   ⊢ (𝜑 → 𝐼 = 𝐽)
Theorem	hbtlem6 40961*	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 40962	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)
20.29.43  Additional material on polynomials [DEPRECATED]
Syntax	cmnc 40963	Extend class notation with the class of monic polynomials.
class Monic
Syntax	cplylt 40964	Extend class notatin with the class of limited-degree polynomials.
class Poly<
Definition	df-mnc 40965*	Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ Monic = (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1})
Definition	df-plylt 40966*	Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.)
⊢ Poly< = (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)})
Theorem	dgrsub2 40967	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 40968	Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) ↔ (𝑃 ∈ (Poly‘𝑆) ∧ ((coeff‘𝑃)‘(deg‘𝑃)) = 1))
Theorem	mncply 40969	A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ∈ (Poly‘𝑆))
Theorem	mnccoe 40970	A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) → ((coeff‘𝑃)‘(deg‘𝑃)) = 1)
Theorem	mncn0 40971	A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ≠ 0𝑝)
20.29.44  Degree and minimal polynomial of algebraic numbers
Syntax	cdgraa 40972	Extend class notation to include the degree function for algebraic numbers.
class degAA
Syntax	cmpaa 40973	Extend class notation to include the minimal polynomial for an algebraic number.
class minPolyAA
Definition	df-dgraa 40974*	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 40975*	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 40976*	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 40977*	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 40978	Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → (degAA‘𝐴) ∈ ℕ)
Theorem	dgraaf 40979	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 40980	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 40981	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 40982*	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 40983*	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 40984	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 40985	Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → (minPolyAA‘𝐴) ∈ (Poly‘ℚ))
Theorem	mpaadgr 40986	Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → (deg‘(minPolyAA‘𝐴)) = (degAA‘𝐴))
Theorem	mpaaroot 40987	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 40988	Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → ((coeff‘(minPolyAA‘𝐴))‘(degAA‘𝐴)) = 1)
20.29.45  Algebraic integers I
Syntax	citgo 40989	Extend class notation with the integral-over predicate.
class IntgOver
Syntax	cza 40990	Extend class notation with the class of algebraic integers.
class ℤ
Definition	df-itgo 40991*	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 40994. 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 40992	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 40993*	Value of the integral-over function. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ (𝑆 ⊆ ℂ → (IntgOver‘𝑆) = {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑆)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
Theorem	aaitgo 40994	The standard algebraic numbers 𝔸 are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝔸 = (IntgOver‘ℚ)
Theorem	itgoss 40995	An integral element is integral over a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (IntgOver‘𝑆) ⊆ (IntgOver‘𝑇))
Theorem	itgocn 40996	All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ (IntgOver‘𝑆) ⊆ ℂ
Theorem	cnsrexpcl 40997	Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑋↑𝑌) ∈ 𝑆)
Theorem	fsumcnsrcl 40998*	Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)
Theorem	cnsrplycl 40999	Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld))    &   ⊢ (𝜑 → 𝑃 ∈ (Poly‘𝐶))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → (𝑃‘𝑋) ∈ 𝑆)
Theorem	rgspnval 41000*	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‘𝑅) ∣ 𝐴 ⊆ 𝑡})