P. 425 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42401-42500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	aomclem2 42401*	Lemma for dfac11 42408. Successor case 2, a choice function for subsets of (𝑅1‘dom 𝑧). (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))}    &   ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵))    &   ⊢ (𝜑 → dom 𝑧 ∈ On)    &   ⊢ (𝜑 → dom 𝑧 = suc ∪ dom 𝑧)    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎))    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → dom 𝑧 ⊆ 𝐴)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))    ⇒   ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘dom 𝑧)(𝑎 ≠ ∅ → (𝐶‘𝑎) ∈ 𝑎))
Theorem	aomclem3 42402*	Lemma for dfac11 42408. Successor case 3, our required well-ordering. (Contributed by Stefan O'Rear, 19-Jan-2015.)
⊢ 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))}    &   ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵))    &   ⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎))))    &   ⊢ 𝐸 = {⟨𝑎, 𝑏⟩ ∣ ∩ (◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})}    &   ⊢ (𝜑 → dom 𝑧 ∈ On)    &   ⊢ (𝜑 → dom 𝑧 = suc ∪ dom 𝑧)    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎))    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → dom 𝑧 ⊆ 𝐴)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))    ⇒   ⊢ (𝜑 → 𝐸 We (𝑅1‘dom 𝑧))
Theorem	aomclem4 42403*	Lemma for dfac11 42408. Limit case. Patch together well-orderings constructed so far using fnwe2 42399 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 42404*	Lemma for dfac11 42408. 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 42405*	Lemma for dfac11 42408. 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 42406*	Lemma for dfac11 42408. (𝑅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 42407*	Lemma for dfac11 42408. 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 42408*	The right-hand side of this theorem (compare with ac4 10490), sometimes known as the "axiom of multiple choice", is a choice equivalent. Curiously, this statement cannot be proved without ax-reg 9607, 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 42409*	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 42410	Lemma for kelac2 42411 and dfac21 42412: knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝑆 ∈ 𝑉 → (topGen‘{𝑆, {𝒫 ∪ 𝑆}}) ∈ Comp)
Theorem	kelac2 42411*	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 42412	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))
21.31.37  Finitely generated left modules
Syntax	clfig 42413	Extend class notation with the class of finitely generated left modules.
class LFinGen
Definition	df-lfig 42414	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 42415*	Property of a finitely generated left module. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑊 ∈ LFinGen ↔ ∃𝑏 ∈ 𝒫 𝐵(𝑏 ∈ Fin ∧ (𝑁‘𝑏) = 𝐵)))
Theorem	islssfg 42416*	Property of a finitely generated left (sub)module. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑋 ∈ LFinGen ↔ ∃𝑏 ∈ 𝒫 𝑈(𝑏 ∈ Fin ∧ (𝑁‘𝑏) = 𝑈)))
Theorem	islssfg2 42417*	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 42418	Finitely spanned subspaces are finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑋 = (𝑊 ↾s (𝑁‘𝐵))    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin) → 𝑋 ∈ LFinGen)
Theorem	fglmod 42419	Finitely generated left modules are left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝑀 ∈ LFinGen → 𝑀 ∈ LMod)
Theorem	lsmfgcl 42420	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)
21.31.38  Noetherian left modules I
Syntax	clnm 42421	Extend class notation with the class of Noetherian left modules.
class LNoeM
Definition	df-lnm 42422*	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 42423*	Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ 𝑆 = (LSubSp‘𝑀)    ⇒   ⊢ (𝑀 ∈ LNoeM ↔ (𝑀 ∈ LMod ∧ ∀𝑖 ∈ 𝑆 (𝑀 ↾s 𝑖) ∈ LFinGen))
Theorem	islnm2 42424*	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 42425	A Noetherian left module is a left module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ (𝑀 ∈ LNoeM → 𝑀 ∈ LMod)
Theorem	lnmlssfg 42426	A submodule of Noetherian module is finitely generated. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑀)    &   ⊢ 𝑅 = (𝑀 ↾s 𝑈)    ⇒   ⊢ ((𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆) → 𝑅 ∈ LFinGen)
Theorem	lnmlsslnm 42427	All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑀)    &   ⊢ 𝑅 = (𝑀 ↾s 𝑈)    ⇒   ⊢ ((𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆) → 𝑅 ∈ LNoeM)
Theorem	lnmfg 42428	A Noetherian left module is finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ (𝑀 ∈ LNoeM → 𝑀 ∈ LFinGen)
Theorem	kercvrlsm 42429	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 42430	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 42431	Epimorphic images of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐵 = (Base‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵) → 𝑇 ∈ LNoeM)
Theorem	lmhmfgsplit 42432	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 42433	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 42434	Noetherian is an invariant property of modules. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝑅 ≃𝑚 𝑆 → (𝑅 ∈ LNoeM ↔ 𝑆 ∈ LNoeM))
21.31.39  Addenda for structure powers
Theorem	pwssplit4 42435*	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 42436	Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ Fin) → 𝑊 ∈ LNoeM)
Theorem	pwslnmlem0 42437	Zeroeth powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s ∅)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑌 ∈ LNoeM)
Theorem	pwslnmlem1 42438*	First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s {𝑖})    ⇒   ⊢ (𝑊 ∈ LNoeM → 𝑌 ∈ LNoeM)
Theorem	pwslnmlem2 42439	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 42440	Finite powers of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s 𝐼)    ⇒   ⊢ ((𝑊 ∈ LNoeM ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM)
21.31.40  Every set admits a group structure iff choice
Theorem	unxpwdom3 42441*	Weaker version of unxpwdom 9604 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 42442*	The pw2f1o 9093 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 42443*	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 42444	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 42445	Being Abelian is a group invariant. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.)
⊢ (𝐺 ≃𝑔 𝐻 → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))
Theorem	imasgim 42446	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 42447	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 42448	The Hartogs number of a set is never zero. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.)
⊢ (𝑆 ∈ 𝑉 → (har‘𝑆) ≠ ∅)
Theorem	numinfctb 42449	A numerable infinite set contains a countable subset. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.)
⊢ ((𝑆 ∈ dom card ∧ ¬ 𝑆 ∈ Fin) → ω ≼ 𝑆)
Theorem	isnumbasgrplem2 42450	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 42451	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 42452	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 42453	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 42454	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.31.41  Noetherian rings and left modules II
Syntax	clnr 42455	Extend class notation with the class of left Noetherian rings.
class LNoeR
Definition	df-lnr 42456	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 42457	Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ LNoeR ↔ (𝐴 ∈ Ring ∧ (ringLMod‘𝐴) ∈ LNoeM))
Theorem	lnrring 42458	Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ LNoeR → 𝐴 ∈ Ring)
Theorem	lnrlnm 42459	Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ LNoeR → (ringLMod‘𝐴) ∈ LNoeM)
Theorem	islnr2 42460*	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 42461	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 42462*	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 42463	Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ LNoeR)
Theorem	lnrfrlm 42464	Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015.)
⊢ 𝑌 = (𝑅 freeLMod 𝐼)    ⇒   ⊢ ((𝑅 ∈ LNoeR ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM)
Theorem	lnrfg 42465	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 42466	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.31.42  Hilbert's Basis Theorem
Syntax	cldgis 42467	The leading ideal sequence used in the Hilbert Basis Theorem.
class ldgIdlSeq
Definition	df-ldgis 42468*	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 42476. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))})))
Theorem	hbtlem1 42469*	Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ 𝐷 = ( deg1 ‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) = {𝑗 ∣ ∃𝑘 ∈ 𝐼 ((𝐷‘𝑘) ≤ 𝑋 ∧ 𝑗 = ((coe1‘𝑘)‘𝑋))})
Theorem	hbtlem2 42470	Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ 𝑇 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) ∈ 𝑇)
Theorem	hbtlem7 42471	Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ 𝑇 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝑆‘𝐼):ℕ0⟶𝑇)
Theorem	hbtlem4 42472	The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑌 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐼)‘𝑌))
Theorem	hbtlem3 42473	The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐼 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐽)‘𝑋))
Theorem	hbtlem5 42474*	The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (LIdeal‘𝑃)    &   ⊢ 𝑆 = (ldgIdlSeq‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐼 ⊆ 𝐽)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ0 ((𝑆‘𝐽)‘𝑥) ⊆ ((𝑆‘𝐼)‘𝑥))    ⇒   ⊢ (𝜑 → 𝐼 = 𝐽)
Theorem	hbtlem6 42475*	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 42476	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.31.43  Additional material on polynomials [DEPRECATED]
Syntax	cmnc 42477	Extend class notation with the class of monic polynomials.
class Monic
Syntax	cplylt 42478	Extend class notatin with the class of limited-degree polynomials.
class Poly<
Definition	df-mnc 42479*	Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ Monic = (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1})
Definition	df-plylt 42480*	Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.)
⊢ Poly< = (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)})
Theorem	dgrsub2 42481	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 42482	Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) ↔ (𝑃 ∈ (Poly‘𝑆) ∧ ((coeff‘𝑃)‘(deg‘𝑃)) = 1))
Theorem	mncply 42483	A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ∈ (Poly‘𝑆))
Theorem	mnccoe 42484	A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) → ((coeff‘𝑃)‘(deg‘𝑃)) = 1)
Theorem	mncn0 42485	A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ≠ 0𝑝)
21.31.44  Degree and minimal polynomial of algebraic numbers
Syntax	cdgraa 42486	Extend class notation to include the degree function for algebraic numbers.
class degAA
Syntax	cmpaa 42487	Extend class notation to include the minimal polynomial for an algebraic number.
class minPolyAA
Definition	df-dgraa 42488*	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 42489*	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 42490*	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 42491*	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 42492	Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → (degAA‘𝐴) ∈ ℕ)
Theorem	dgraaf 42493	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 42494	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 42495	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 42496*	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 42497*	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 42498	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 42499	Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → (minPolyAA‘𝐴) ∈ (Poly‘ℚ))
Theorem	mpaadgr 42500	Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → (deg‘(minPolyAA‘𝐴)) = (degAA‘𝐴))