P. 401 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40001-40100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	aomclem4 40001*	Lemma for dfac11 40006. Limit case. Patch together well-orderings constructed so far using fnwe2 39997 to cover the limit rank. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))}    &   ⊢ (𝜑 → dom 𝑧 ∈ On)    &   ⊢ (𝜑 → dom 𝑧 = ∪ dom 𝑧)    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎))    ⇒   ⊢ (𝜑 → 𝐹 We (𝑅1‘dom 𝑧))
Theorem	aomclem5 40002*	Lemma for dfac11 40006. Combine the successor case with the limit case. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))}    &   ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵))    &   ⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎))))    &   ⊢ 𝐸 = {⟨𝑎, 𝑏⟩ ∣ ∩ (◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})}    &   ⊢ 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))}    &   ⊢ 𝐺 = (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)))    &   ⊢ (𝜑 → dom 𝑧 ∈ On)    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎))    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → dom 𝑧 ⊆ 𝐴)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))    ⇒   ⊢ (𝜑 → 𝐺 We (𝑅1‘dom 𝑧))
Theorem	aomclem6 40003*	Lemma for dfac11 40006. Transfinite induction, close over 𝑧. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))}    &   ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵))    &   ⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎))))    &   ⊢ 𝐸 = {⟨𝑎, 𝑏⟩ ∣ ∩ (◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})}    &   ⊢ 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))}    &   ⊢ 𝐺 = (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)))    &   ⊢ 𝐻 = recs((𝑧 ∈ V ↦ 𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))    ⇒   ⊢ (𝜑 → (𝐻‘𝐴) We (𝑅1‘𝐴))
Theorem	aomclem7 40004*	Lemma for dfac11 40006. (𝑅1‘𝐴) is well-orderable. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))}    &   ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵))    &   ⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎))))    &   ⊢ 𝐸 = {⟨𝑎, 𝑏⟩ ∣ ∩ (◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})}    &   ⊢ 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))}    &   ⊢ 𝐺 = (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)))    &   ⊢ 𝐻 = recs((𝑧 ∈ V ↦ 𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))    ⇒   ⊢ (𝜑 → ∃𝑏 𝑏 We (𝑅1‘𝐴))
Theorem	aomclem8 40005*	Lemma for dfac11 40006. Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))    ⇒   ⊢ (𝜑 → ∃𝑏 𝑏 We (𝑅1‘𝐴))
Theorem	dfac11 40006*	The right-hand side of this theorem (compare with ac4 9886), sometimes known as the "axiom of multiple choice", is a choice equivalent. Curiously, this statement cannot be proved without ax-reg 9040, despite not mentioning the cumulative hierarchy in any way as most consequences of regularity do. This is definition (MC) of [Schechter] p. 141. EDITORIAL: the proof is not original with me of course but I lost my reference sometime after writing it. A multiple choice function allows any total order to be extended to a choice function, which in turn defines a well-ordering. Since a well-ordering on a set defines a simple ordering of the power set, this allows the trivial well-ordering of the empty set to be transfinitely bootstrapped up the cumulative hierarchy to any desired level. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Stefan O'Rear, 1-Jun-2015.)
⊢ (CHOICE ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ ((𝒫 𝑧 ∩ Fin) ∖ {∅})))
Theorem	kelac1 40007*	Kelley's choice, basic form: if a collection of sets can be cast as closed sets in the factors of a topology, and there is a definable element in each topology (which need not be in the closed set - if it were this would be trivial), then compactness (via finite intersection) guarantees that the final product is nonempty. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ∈ (Clsd‘𝐽))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐵:𝑆–1-1-onto→𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑈 ∈ ∪ 𝐽)    &   ⊢ (𝜑 → (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Comp)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅)
Theorem	kelac2lem 40008	Lemma for kelac2 40009 and dfac21 40010: knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝑆 ∈ 𝑉 → (topGen‘{𝑆, {𝒫 ∪ 𝑆}}) ∈ Comp)
Theorem	kelac2 40009*	Kelley's choice, most common form: compactness of a product of knob topologies recovers choice. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅)    &   ⊢ (𝜑 → (∏t‘(𝑥 ∈ 𝐼 ↦ (topGen‘{𝑆, {𝒫 ∪ 𝑆}}))) ∈ Comp)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅)
Theorem	dfac21 40010	Tychonoff's theorem is a choice equivalent. Definition AC21 of Schechter p. 461. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Revised by Mario Carneiro, 27-Aug-2015.)
⊢ (CHOICE ↔ ∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp))
20.29.37  Finitely generated left modules
Syntax	clfig 40011	Extend class notation with the class of finitely generated left modules.
class LFinGen
Definition	df-lfig 40012	Define the class of finitely generated left modules. Finite generation of subspaces can be intepreted using ↾s. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ LFinGen = {𝑤 ∈ LMod ∣ (Base‘𝑤) ∈ ((LSpan‘𝑤) “ (𝒫 (Base‘𝑤) ∩ Fin))}
Theorem	islmodfg 40013*	Property of a finitely generated left module. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑊 ∈ LFinGen ↔ ∃𝑏 ∈ 𝒫 𝐵(𝑏 ∈ Fin ∧ (𝑁‘𝑏) = 𝐵)))
Theorem	islssfg 40014*	Property of a finitely generated left (sub)module. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑋 ∈ LFinGen ↔ ∃𝑏 ∈ 𝒫 𝑈(𝑏 ∈ Fin ∧ (𝑁‘𝑏) = 𝑈)))
Theorem	islssfg2 40015*	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 40016	Finitely spanned subspaces are finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑋 = (𝑊 ↾s (𝑁‘𝐵))    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin) → 𝑋 ∈ LFinGen)
Theorem	fglmod 40017	Finitely generated left modules are left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝑀 ∈ LFinGen → 𝑀 ∈ LMod)
Theorem	lsmfgcl 40018	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 40019	Extend class notation with the class of Noetherian left modules.
class LNoeM
Definition	df-lnm 40020*	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 40021*	Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ 𝑆 = (LSubSp‘𝑀)    ⇒   ⊢ (𝑀 ∈ LNoeM ↔ (𝑀 ∈ LMod ∧ ∀𝑖 ∈ 𝑆 (𝑀 ↾s 𝑖) ∈ LFinGen))
Theorem	islnm2 40022*	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 40023	A Noetherian left module is a left module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ (𝑀 ∈ LNoeM → 𝑀 ∈ LMod)
Theorem	lnmlssfg 40024	A submodule of Noetherian module is finitely generated. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑀)    &   ⊢ 𝑅 = (𝑀 ↾s 𝑈)    ⇒   ⊢ ((𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆) → 𝑅 ∈ LFinGen)
Theorem	lnmlsslnm 40025	All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑀)    &   ⊢ 𝑅 = (𝑀 ↾s 𝑈)    ⇒   ⊢ ((𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆) → 𝑅 ∈ LNoeM)
Theorem	lnmfg 40026	A Noetherian left module is finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ (𝑀 ∈ LNoeM → 𝑀 ∈ LFinGen)
Theorem	kercvrlsm 40027	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 40028	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 40029	Epimorphic images of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐵 = (Base‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵) → 𝑇 ∈ LNoeM)
Theorem	lmhmfgsplit 40030	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 40031	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 40032	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 40033*	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 40034	Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ Fin) → 𝑊 ∈ LNoeM)
Theorem	pwslnmlem0 40035	Zeroeth powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s ∅)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑌 ∈ LNoeM)
Theorem	pwslnmlem1 40036*	First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s {𝑖})    ⇒   ⊢ (𝑊 ∈ LNoeM → 𝑌 ∈ LNoeM)
Theorem	pwslnmlem2 40037	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 40038	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 40039*	Weaker version of unxpwdom 9037 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 40040*	The pw2f1o 8605 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 40041*	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 40042	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 40043	Being Abelian is a group invariant. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.)
⊢ (𝐺 ≃𝑔 𝐻 → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))
Theorem	imasgim 40044	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 40045	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 40046	The Hartogs number of a set is never zero. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.)
⊢ (𝑆 ∈ 𝑉 → (har‘𝑆) ≠ ∅)
Theorem	numinfctb 40047	A numerable infinite set contains a countable subset. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.)
⊢ ((𝑆 ∈ dom card ∧ ¬ 𝑆 ∈ Fin) → ω ≼ 𝑆)
Theorem	isnumbasgrplem2 40048	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 40049	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 40050	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 40051	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 40052	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 40053	Extend class notation with the class of left Noetherian rings.
class LNoeR
Definition	df-lnr 40054	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 40055	Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ LNoeR ↔ (𝐴 ∈ Ring ∧ (ringLMod‘𝐴) ∈ LNoeM))
Theorem	lnrring 40056	Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ LNoeR → 𝐴 ∈ Ring)
Theorem	lnrlnm 40057	Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ LNoeR → (ringLMod‘𝐴) ∈ LNoeM)
Theorem	islnr2 40058*	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 40059	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 40060*	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 40061	Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ LNoeR)
Theorem	lnrfrlm 40062	Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015.)
⊢ 𝑌 = (𝑅 freeLMod 𝐼)    ⇒   ⊢ ((𝑅 ∈ LNoeR ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM)
Theorem	lnrfg 40063	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 40064	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 40065	The leading ideal sequence used in the Hilbert Basis Theorem.
class ldgIdlSeq
Definition	df-ldgis 40066*	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 40074. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))})))
Theorem	hbtlem1 40067*	Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ 𝐷 = ( deg1 ‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) = {𝑗 ∣ ∃𝑘 ∈ 𝐼 ((𝐷‘𝑘) ≤ 𝑋 ∧ 𝑗 = ((coe1‘𝑘)‘𝑋))})
Theorem	hbtlem2 40068	Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ 𝑇 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) ∈ 𝑇)
Theorem	hbtlem7 40069	Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ 𝑇 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝑆‘𝐼):ℕ0⟶𝑇)
Theorem	hbtlem4 40070	The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑌 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐼)‘𝑌))
Theorem	hbtlem3 40071	The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐼 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐽)‘𝑋))
Theorem	hbtlem5 40072*	The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐼 ⊆ 𝐽)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ0 ((𝑆‘𝐽)‘𝑥) ⊆ ((𝑆‘𝐼)‘𝑥))    ⇒   ⊢ (𝜑 → 𝐼 = 𝐽)
Theorem	hbtlem6 40073*	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 40074	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 40075	Extend class notation with the class of monic polynomials.
class Monic
Syntax	cplylt 40076	Extend class notatin with the class of limited-degree polynomials.
class Poly<
Definition	df-mnc 40077*	Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ Monic = (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1})
Definition	df-plylt 40078*	Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.)
⊢ Poly< = (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)})
Theorem	dgrsub2 40079	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 40080	Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) ↔ (𝑃 ∈ (Poly‘𝑆) ∧ ((coeff‘𝑃)‘(deg‘𝑃)) = 1))
Theorem	mncply 40081	A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ∈ (Poly‘𝑆))
Theorem	mnccoe 40082	A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) → ((coeff‘𝑃)‘(deg‘𝑃)) = 1)
Theorem	mncn0 40083	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 40084	Extend class notation to include the degree function for algebraic numbers.
class degAA
Syntax	cmpaa 40085	Extend class notation to include the minimal polynomial for an algebraic number.
class minPolyAA
Definition	df-dgraa 40086*	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 40087*	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 40088*	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 40089*	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 40090	Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → (degAA‘𝐴) ∈ ℕ)
Theorem	dgraaf 40091	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 40092	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 40093	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 40094*	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 40095*	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 40096	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 40097	Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → (minPolyAA‘𝐴) ∈ (Poly‘ℚ))
Theorem	mpaadgr 40098	Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → (deg‘(minPolyAA‘𝐴)) = (degAA‘𝐴))
Theorem	mpaaroot 40099	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 40100	Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → ((coeff‘(minPolyAA‘𝐴))‘(degAA‘𝐴)) = 1)