P. 201 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20001-20100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pgpfac1lem3 20001*	Lemma for pgpfac1 20004. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    &   ⊢ 𝑆 = (𝐾‘{𝐴})    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸)    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 })    &   ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈)    &   ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊)))    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → ((𝑃 · 𝐶)(+g‘𝐺)(𝑀 · 𝐴)) ∈ 𝑊)    &   ⊢ 𝐷 = (𝐶(+g‘𝐺)((𝑀 / 𝑃) · 𝐴))    ⇒   ⊢ (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝑈))
Theorem	pgpfac1lem4 20002*	Lemma for pgpfac1 20004. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    &   ⊢ 𝑆 = (𝐾‘{𝐴})    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸)    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 })    &   ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈)    &   ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊)))    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝑈))
Theorem	pgpfac1lem5 20003*	Lemma for pgpfac1 20004. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    &   ⊢ 𝑆 = (𝐾‘{𝐴})    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸)    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑠 ∈ (SubGrp‘𝐺)((𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝑠)))    ⇒   ⊢ (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝑈))
Theorem	pgpfac1 20004*	Factorization of a finite abelian p-group. There is a direct product decomposition of any abelian group of prime-power order where one of the factors is cyclic and generated by an element of maximal order. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    &   ⊢ 𝑆 = (𝐾‘{𝐴})    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝐵))
Theorem	pgpfaclem1 20005*	Lemma for pgpfac 20008. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)))    &   ⊢ 𝐻 = (𝐺 ↾s 𝑈)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻))    &   ⊢ 𝑂 = (od‘𝐻)    &   ⊢ 𝐸 = (gEx‘𝐻)    &   ⊢ 0 = (0g‘𝐻)    &   ⊢ ⊕ = (LSSum‘𝐻)    &   ⊢ (𝜑 → 𝐸 ≠ 1)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → (𝑂‘𝑋) = 𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻))    &   ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })    &   ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈)    &   ⊢ (𝜑 → 𝑆 ∈ Word 𝐶)    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝑊)    &   ⊢ 𝑇 = (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
Theorem	pgpfaclem2 20006*	Lemma for pgpfac 20008. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)))    &   ⊢ 𝐻 = (𝐺 ↾s 𝑈)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻))    &   ⊢ 𝑂 = (od‘𝐻)    &   ⊢ 𝐸 = (gEx‘𝐻)    &   ⊢ 0 = (0g‘𝐻)    &   ⊢ ⊕ = (LSSum‘𝐻)    &   ⊢ (𝜑 → 𝐸 ≠ 1)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → (𝑂‘𝑋) = 𝐸)    &   ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻))    &   ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })    &   ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
Theorem	pgpfaclem3 20007*	Lemma for pgpfac 20008. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)))    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
Theorem	pgpfac 20008*	Full factorization of a finite abelian p-group, by iterating pgpfac1 20004. There is a direct product decomposition of any abelian group of prime-power order into cyclic subgroups. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵))
Theorem	ablfaclem1 20009*	Lemma for ablfac 20012. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)})    ⇒   ⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝑊‘𝑈) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)})
Theorem	ablfaclem2 20010*	Lemma for ablfac 20012. (Contributed by Mario Carneiro, 27-Apr-2016.) (Proof shortened by Mario Carneiro, 3-May-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)})    &   ⊢ (𝜑 → 𝐹:𝐴⟶Word 𝐶)    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) ∈ (𝑊‘(𝑆‘𝑦)))    &   ⊢ 𝐿 = ∪ 𝑦 ∈ 𝐴 ({𝑦} × dom (𝐹‘𝑦))    &   ⊢ (𝜑 → 𝐻:(0..^(♯‘𝐿))–1-1-onto→𝐿)    ⇒   ⊢ (𝜑 → (𝑊‘𝐵) ≠ ∅)
Theorem	ablfaclem3 20011*	Lemma for ablfac 20012. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)})    ⇒   ⊢ (𝜑 → (𝑊‘𝐵) ≠ ∅)
Theorem	ablfac 20012*	The Fundamental Theorem of (finite) Abelian Groups. Any finite abelian group is a direct product of cyclic p-groups. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵))
Theorem	ablfac2 20013*	Choose generators for each cyclic group in ablfac 20012. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝑆 = (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤‘𝑘))))    ⇒   ⊢ (𝜑 → ∃𝑤 ∈ Word 𝐵(𝑆:dom 𝑤⟶𝐶 ∧ 𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵))
10.2.15  Simple groups
10.2.15.1  Definition and basic properties
Syntax	csimpg 20014	Extend class notation with the class of simple groups.
class SimpGrp
Definition	df-simpg 20015	Define class of all simple groups. A simple group is a group (df-grp 18859) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity (simpgnsgbid 20027). (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o}
Theorem	issimpg 20016	The predicate "is a simple group". (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝐺 ∈ SimpGrp ↔ (𝐺 ∈ Grp ∧ (NrmSGrp‘𝐺) ≈ 2o))
Theorem	issimpgd 20017	Deduce a simple group from its properties. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 2o)    ⇒   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)
Theorem	simpggrp 20018	A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝐺 ∈ SimpGrp → 𝐺 ∈ Grp)
Theorem	simpggrpd 20019	A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	simpg2nsg 20020	A simple group has two normal subgroups. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝐺 ∈ SimpGrp → (NrmSGrp‘𝐺) ≈ 2o)
Theorem	trivnsimpgd 20021	Trivial groups are not simple. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    ⇒   ⊢ (𝜑 → ¬ 𝐺 ∈ SimpGrp)
Theorem	simpgntrivd 20022	Simple groups are nontrivial. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → ¬ 𝐵 = { 0 })
Theorem	simpgnideld 20023*	A simple group contains a nonidentity element. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ¬ 𝑥 = 0 )
Theorem	simpgnsgd 20024	The only normal subgroups of a simple group are the group itself and the trivial group. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → (NrmSGrp‘𝐺) = {{ 0 }, 𝐵})
Theorem	simpgnsgeqd 20025	A normal subgroup of a simple group is either the whole group or the trivial subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    &   ⊢ (𝜑 → 𝐴 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → (𝐴 = { 0 } ∨ 𝐴 = 𝐵))
Theorem	2nsgsimpgd 20026*	If any normal subgroup of a nontrivial group is either the trivial subgroup or the whole group, the group is simple. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → ¬ { 0 } = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (NrmSGrp‘𝐺)) → (𝑥 = { 0 } ∨ 𝑥 = 𝐵))    ⇒   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)
Theorem	simpgnsgbid 20027	A nontrivial group is simple if and only if its normal subgroups are exactly the group itself and the trivial subgroup. (Contributed by Rohan Ridenour, 4-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → ¬ { 0 } = 𝐵)    ⇒   ⊢ (𝜑 → (𝐺 ∈ SimpGrp ↔ (NrmSGrp‘𝐺) = {{ 0 }, 𝐵}))
10.2.15.2  Classification of abelian simple groups
Theorem	ablsimpnosubgd 20028	A subgroup of an abelian simple group containing a nonidentity element is the whole group. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → ¬ 𝐴 = 0 )    ⇒   ⊢ (𝜑 → 𝑆 = 𝐵)
Theorem	ablsimpg1gend 20029*	An abelian simple group is generated by any non-identity element. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐴 = 0 )    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℤ 𝐶 = (𝑛 · 𝐴))
Theorem	ablsimpgcygd 20030	An abelian simple group is cyclic. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof shortened by Rohan Ridenour, 31-Oct-2023.)
⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → 𝐺 ∈ CycGrp)
Theorem	ablsimpgfindlem1 20031*	Lemma for ablsimpgfind 20034. An element of an abelian finite simple group which doesn't square to the identity has finite order. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof shortened by Rohan Ridenour, 31-Oct-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (2 · 𝑥) ≠ 0 ) → (𝑂‘𝑥) ≠ 0)
Theorem	ablsimpgfindlem2 20032*	Lemma for ablsimpgfind 20034. An element of an abelian finite simple group which squares to the identity has finite order. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (2 · 𝑥) = 0 ) → (𝑂‘𝑥) ≠ 0)
Theorem	cycsubggenodd 20033*	Relationship between the order of a subgroup and the order of a generator of the subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 = ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴)))    ⇒   ⊢ (𝜑 → (𝑂‘𝐴) = if(𝐶 ∈ Fin, (♯‘𝐶), 0))
Theorem	ablsimpgfind 20034	An abelian simple group is finite. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → 𝐵 ∈ Fin)
Theorem	fincygsubgd 20035*	The subgroup referenced in fincygsubgodd 20036 is a subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐻 = (𝑛 ∈ ℤ ↦ (𝑛 · (𝐶 · 𝐴)))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    ⇒   ⊢ (𝜑 → ran 𝐻 ∈ (SubGrp‘𝐺))
Theorem	fincygsubgodd 20036*	Calculate the order of a subgroup of a finite cyclic group. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐷 = ((♯‘𝐵) / 𝐶)    &   ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴))    &   ⊢ 𝐻 = (𝑛 ∈ ℤ ↦ (𝑛 · (𝐶 · 𝐴)))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → ran 𝐹 = 𝐵)    &   ⊢ (𝜑 → 𝐶 ∥ (♯‘𝐵))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    ⇒   ⊢ (𝜑 → (♯‘ran 𝐻) = 𝐷)
Theorem	fincygsubgodexd 20037*	A finite cyclic group has subgroups of every possible order. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CycGrp)    &   ⊢ (𝜑 → 𝐶 ∥ (♯‘𝐵))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (SubGrp‘𝐺)(♯‘𝑥) = 𝐶)
Theorem	prmgrpsimpgd 20038	A group of prime order is simple. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → (♯‘𝐵) ∈ ℙ)    ⇒   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)
Theorem	ablsimpgprmd 20039	An abelian simple group has prime order. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → (♯‘𝐵) ∈ ℙ)
Theorem	ablsimpgd 20040	An abelian group is simple if and only if its order is prime. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    ⇒   ⊢ (𝜑 → (𝐺 ∈ SimpGrp ↔ (♯‘𝐵) ∈ ℙ))
10.2.16  Totally ordered monoids and groups
Syntax	comnd 20041	Extend class notation with the class of all right ordered monoids.
class oMnd
Syntax	cogrp 20042	Extend class notation with the class of all right ordered groups.
class oGrp
Definition	df-omnd 20043*	Define class of all right ordered monoids. An ordered monoid is a monoid with a total ordering compatible with its operation. It is possible to use this definition also for left ordered monoids, by applying it to (oppg‘𝑀). (Contributed by Thierry Arnoux, 13-Mar-2018.)
⊢ oMnd = {𝑔 ∈ Mnd ∣ [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑝][(le‘𝑔) / 𝑙](𝑔 ∈ Toset ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ∀𝑐 ∈ 𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))}
Definition	df-ogrp 20044	Define class of all ordered groups. An ordered group is a group with a total ordering compatible with its operation. (Contributed by Thierry Arnoux, 13-Mar-2018.)
⊢ oGrp = (Grp ∩ oMnd)
Theorem	isomnd 20045*	A (left) ordered monoid is a monoid with a total ordering compatible with its operation. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ ≤ = (le‘𝑀)    ⇒   ⊢ (𝑀 ∈ oMnd ↔ (𝑀 ∈ Mnd ∧ 𝑀 ∈ Toset ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝑎 ≤ 𝑏 → (𝑎 + 𝑐) ≤ (𝑏 + 𝑐))))
Theorem	isogrp 20046	A (left-)ordered group is a group with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
Theorem	ogrpgrp 20047	A left-ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018.)
⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp)
Theorem	omndmnd 20048	A left-ordered monoid is a monoid. (Contributed by Thierry Arnoux, 13-Mar-2018.)
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Mnd)
Theorem	omndtos 20049	A left-ordered monoid is a totally ordered set. (Contributed by Thierry Arnoux, 13-Mar-2018.)
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset)
Theorem	omndadd 20050	In an ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ≤ = (le‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 + 𝑍) ≤ (𝑌 + 𝑍))
Theorem	omndaddr 20051	In a right ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ≤ = (le‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ (((oppg‘𝑀) ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑍 + 𝑋) ≤ (𝑍 + 𝑌))
Theorem	omndadd2d 20052	In a commutative left ordered monoid, the ordering is compatible with monoid addition. Double addition version. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ≤ = (le‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ oMnd)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑍)    &   ⊢ (𝜑 → 𝑌 ≤ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ CMnd)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ≤ (𝑍 + 𝑊))
Theorem	omndadd2rd 20053	In a left- and right- ordered monoid, the ordering is compatible with monoid addition. Double addition version. (Contributed by Thierry Arnoux, 2-May-2018.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ≤ = (le‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ oMnd)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑍)    &   ⊢ (𝜑 → 𝑌 ≤ 𝑊)    &   ⊢ (𝜑 → (oppg‘𝑀) ∈ oMnd)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ≤ (𝑍 + 𝑊))
Theorem	submomnd 20054	A submonoid of an ordered monoid is also ordered. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ oMnd)
Theorem	omndmul2 20055	In an ordered monoid, the ordering is compatible with group power. This version does not require the monoid to be commutative. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ≤ = (le‘𝑀)    &   ⊢ · = (.g‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) → 0 ≤ (𝑁 · 𝑋))
Theorem	omndmul3 20056	In an ordered monoid, the ordering is compatible with group power. This version does not require the monoid to be commutative. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ≤ = (le‘𝑀)    &   ⊢ · = (.g‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ oMnd)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ≤ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 0 ≤ 𝑋)    ⇒   ⊢ (𝜑 → (𝑁 · 𝑋) ≤ (𝑃 · 𝑋))
Theorem	omndmul 20057	In a commutative ordered monoid, the ordering is compatible with group power. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ≤ = (le‘𝑀)    &   ⊢ · = (.g‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ oMnd)    &   ⊢ (𝜑 → 𝑀 ∈ CMnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → (𝑁 · 𝑋) ≤ (𝑁 · 𝑌))
Theorem	ogrpinv0le 20058	In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ≤ = (le‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) → ( 0 ≤ 𝑋 ↔ (𝐼‘𝑋) ≤ 0 ))
Theorem	ogrpsub 20059	In an ordered group, the ordering is compatible with group subtraction. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ≤ = (le‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 − 𝑍) ≤ (𝑌 − 𝑍))
Theorem	ogrpaddlt 20060	In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ < = (lt‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 + 𝑍) < (𝑌 + 𝑍))
Theorem	ogrpaddltbi 20061	In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ < = (lt‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 < 𝑌 ↔ (𝑋 + 𝑍) < (𝑌 + 𝑍)))
Theorem	ogrpaddltrd 20062	In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ < = (lt‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → (oppg‘𝐺) ∈ oGrp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 < 𝑌)    ⇒   ⊢ (𝜑 → (𝑍 + 𝑋) < (𝑍 + 𝑌))
Theorem	ogrpaddltrbid 20063	In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 4-Sep-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ < = (lt‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → (oppg‘𝐺) ∈ oGrp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 < 𝑌 ↔ (𝑍 + 𝑋) < (𝑍 + 𝑌)))
Theorem	ogrpsublt 20064	In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ < = (lt‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 − 𝑍) < (𝑌 − 𝑍))
Theorem	ogrpinv0lt 20065	In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ < = (lt‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ (𝐼‘𝑋) < 0 ))
Theorem	ogrpinvlt 20066	In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ < = (lt‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ oGrp ∧ (oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝐼‘𝑌) < (𝐼‘𝑋)))
Theorem	gsumle 20067	A finite sum in an ordered monoid is monotonic. This proof would be much easier in an ordered group, where an inverse element would be available. (Contributed by Thierry Arnoux, 13-Mar-2018.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ≤ = (le‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ oMnd)    &   ⊢ (𝜑 → 𝑀 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 ∘r ≤ 𝐺)    ⇒   ⊢ (𝜑 → (𝑀 Σg 𝐹) ≤ (𝑀 Σg 𝐺))
10.3  Rings
10.3.1  Multiplicative Group
Syntax	cmgp 20068	Multiplicative group.
class mulGrp
Definition	df-mgp 20069	Define a structure that puts the multiplication operation of a ring in the addition slot. Note that this will not actually be a group for the average ring, or even for a field, but it will be a monoid, and unitgrp 20311 shows that we get a group if we restrict to the elements that have inverses. This allows to formalize such notions as "the multiplication operation of a ring is a monoid" (ringmgp 20167) or "the multiplicative identity" in terms of the identity of a monoid (df-ur 20110). (Contributed by Mario Carneiro, 21-Dec-2014.)
⊢ mulGrp = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(+g‘ndx), (.r‘𝑤)⟩))
Theorem	fnmgp 20070	The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ mulGrp Fn V
Theorem	mgpval 20071	Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
Theorem	mgpplusg 20072	Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ · = (+g‘𝑀)
Theorem	mgpbas 20073	Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝐵 = (Base‘𝑀)
Theorem	mgpsca 20074	The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp 20255. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑆 = (Scalar‘𝑅)    ⇒   ⊢ 𝑆 = (Scalar‘𝑀)
Theorem	mgptset 20075	Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (TopSet‘𝑅) = (TopSet‘𝑀)
Theorem	mgptopn 20076	Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑅)    ⇒   ⊢ 𝐽 = (TopOpen‘𝑀)
Theorem	mgpds 20077	Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝐵 = (dist‘𝑅)    ⇒   ⊢ 𝐵 = (dist‘𝑀)
Theorem	mgpress 20078	Subgroup commutes with the multiplicative group operator. (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof shortened by AV, 18-Oct-2024.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑀 ↾s 𝐴) = (mulGrp‘𝑆))
Theorem	prdsmgp 20079	The multiplicative monoid of a product is the product of the multiplicative monoids of the factors. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑌)    &   ⊢ 𝑍 = (𝑆Xs(mulGrp ∘ 𝑅))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    ⇒   ⊢ (𝜑 → ((Base‘𝑀) = (Base‘𝑍) ∧ (+g‘𝑀) = (+g‘𝑍)))
10.3.2  Non-unital rings ("rngs") According to Wikipedia, "... in abstract algebra, a rng (or non-unital ring or pseudo-ring) is an algebraic structure satisfying the same properties as a [unital] ring, without assuming the existence of a multiplicative identity. The term "rng" (pronounced rung) is meant to suggest that it is a "ring" without "i", i.e. without the requirement for an "identity element"." (see https://en.wikipedia.org/wiki/Rng_(algebra), 28-Mar-2025).
Syntax	crng 20080	Extend class notation with class of all non-unital rings.
class Rng
Definition	df-rng 20081*	Define the class of all non-unital rings. A non-unital ring (or rng, or pseudoring) is a set equipped with two everywhere-defined internal operations, whose first one is an additive abelian group operation and the second one is a multiplicative semigroup operation, and where the addition is left- and right-distributive for the multiplication. Definition of a pseudo-ring in section I.8.1 of [BourbakiAlg1] p. 93 or the definition of a ring in part Preliminaries of [Roman] p. 18. As almost always in mathematics, "non-unital" means "not necessarily unital". Therefore, by talking about a ring (in general) or a non-unital ring the "unital" case is always included. In contrast to a unital ring, the commutativity of addition must be postulated and cannot be proven from the other conditions. (Contributed by AV, 6-Jan-2020.)
⊢ Rng = {𝑓 ∈ Abel ∣ ((mulGrp‘𝑓) ∈ Smgrp ∧ [(Base‘𝑓) / 𝑏][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
Theorem	isrng 20082*	The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧ 𝐺 ∈ Smgrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
Theorem	rngabl 20083	A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel)
Theorem	rngmgp 20084	A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐺 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → 𝐺 ∈ Smgrp)
Theorem	rngmgpf 20085	Restricted functionality of the multiplicative group on non-unital rings (mgpf 20176 analog). (Contributed by AV, 22-Feb-2025.)
⊢ (mulGrp ↾ Rng):Rng⟶Smgrp
Theorem	rnggrp 20086	A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.)
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp)
Theorem	rngass 20087	Associative law for the multiplication operation of a non-unital ring. (Contributed by NM, 27-Aug-2011.) (Revised by AV, 13-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 · 𝑌) · 𝑍) = (𝑋 · (𝑌 · 𝑍)))
Theorem	rngdi 20088	Distributive law for the multiplication operation of a non-unital ring (left-distributivity). (Contributed by AV, 14-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)))
Theorem	rngdir 20089	Distributive law for the multiplication operation of a non-unital ring (right-distributivity). (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))
Theorem	rngacl 20090	Closure of the addition operation of a non-unital ring. (Contributed by AV, 16-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	rng0cl 20091	The zero element of a non-unital ring belongs to its base set. (Contributed by AV, 16-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → 0 ∈ 𝐵)
Theorem	rngcl 20092	Closure of the multiplication operation of a non-unital ring. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
Theorem	rnglz 20093	The zero of a non-unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringlz 20221. (Revised by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = 0 )
Theorem	rngrz 20094	The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringrz 20222. (Revised by AV, 16-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵) → (𝑋 · 0 ) = 0 )
Theorem	rngmneg1 20095	Negation of a product in a non-unital ring (mulneg1 11563 analog). In contrast to ringmneg1 20232, the proof does not (and cannot) make use of the existence of a ring unity. (Contributed by AV, 17-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘𝑋) · 𝑌) = (𝑁‘(𝑋 · 𝑌)))
Theorem	rngmneg2 20096	Negation of a product in a non-unital ring (mulneg2 11564 analog). In contrast to ringmneg2 20233, the proof does not (and cannot) make use of the existence of a ring unity. (Contributed by AV, 17-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑁‘𝑌)) = (𝑁‘(𝑋 · 𝑌)))
Theorem	rngm2neg 20097	Double negation of a product in a non-unital ring (mul2neg 11566 analog). (Contributed by Mario Carneiro, 4-Dec-2014.) Generalization of ringm2neg 20234. (Revised by AV, 17-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘𝑋) · (𝑁‘𝑌)) = (𝑋 · 𝑌))
Theorem	rngansg 20098	Every additive subgroup of a non-unital ring is normal. (Contributed by AV, 25-Feb-2025.)
⊢ (𝑅 ∈ Rng → (NrmSGrp‘𝑅) = (SubGrp‘𝑅))
Theorem	rngsubdi 20099	Ring multiplication distributes over subtraction. (subdi 11560 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdi 20235. (Revised by AV, 23-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑌 − 𝑍)) = ((𝑋 · 𝑌) − (𝑋 · 𝑍)))
Theorem	rngsubdir 20100	Ring multiplication distributes over subtraction. (subdir 11561 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdir 20236. (Revised by AV, 23-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 − 𝑌) · 𝑍) = ((𝑋 · 𝑍) − (𝑌 · 𝑍)))