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	dpjrid 20001	The 𝑌-th index projection annihilates elements of other factors. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ 𝑃 = (𝐺dProj𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑆‘𝑋))    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑌 ≠ 𝑋)    ⇒   ⊢ (𝜑 → ((𝑃‘𝑌)‘𝐴) = 0 )
Theorem	dpjghm 20002	The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ 𝑃 = (𝐺dProj𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑃‘𝑋) ∈ ((𝐺 ↾s (𝐺 DProd 𝑆)) GrpHom 𝐺))
Theorem	dpjghm2 20003	The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ 𝑃 = (𝐺dProj𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑃‘𝑋) ∈ ((𝐺 ↾s (𝐺 DProd 𝑆)) GrpHom (𝐺 ↾s (𝑆‘𝑋))))
10.2.14.6  The Fundamental Theorem of Abelian Groups
Theorem	ablfacrplem 20004*	Lemma for ablfacrp2 20006. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀}    &   ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    &   ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁))    ⇒   ⊢ (𝜑 → ((♯‘𝐾) gcd 𝑁) = 1)
Theorem	ablfacrp 20005*	A finite abelian group whose order factors into relatively prime integers, itself "factors" into two subgroups 𝐾, 𝐿 that have trivial intersection and whose product is the whole group. Lemma 6.1C.2 of [Shapiro], p. 199. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀}    &   ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    &   ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁))    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (𝜑 → ((𝐾 ∩ 𝐿) = { 0 } ∧ (𝐾 ⊕ 𝐿) = 𝐵))
Theorem	ablfacrp2 20006*	The factors 𝐾, 𝐿 of ablfacrp 20005 have the expected orders (which allows for repeated application to decompose 𝐺 into subgroups of prime-power order). Lemma 6.1C.2 of [Shapiro], p. 199. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀}    &   ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    &   ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁))    ⇒   ⊢ (𝜑 → ((♯‘𝐾) = 𝑀 ∧ (♯‘𝐿) = 𝑁))
Theorem	ablfac1lem 20007*	Lemma for ablfac1b 20009. Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    &   ⊢ 𝑀 = (𝑃↑(𝑃 pCnt (♯‘𝐵)))    &   ⊢ 𝑁 = ((♯‘𝐵) / 𝑀)    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑀 gcd 𝑁) = 1 ∧ (♯‘𝐵) = (𝑀 · 𝑁)))
Theorem	ablfac1a 20008*	The factors of ablfac1b 20009 are of prime power order. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → (♯‘(𝑆‘𝑃)) = (𝑃↑(𝑃 pCnt (♯‘𝐵))))
Theorem	ablfac1b 20009*	Any abelian group is the direct product of factors of prime power order (with the exact order further matching the prime factorization of the group order). (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    ⇒   ⊢ (𝜑 → 𝐺dom DProd 𝑆)
Theorem	ablfac1c 20010*	The factors of ablfac1b 20009 cover the entire group. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    &   ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝐵)
Theorem	ablfac1eulem 20011*	Lemma for ablfac1eu 20012. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    &   ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    &   ⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵))    &   ⊢ (𝜑 → dom 𝑇 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → ¬ 𝑃 ∥ (♯‘(𝐺 DProd (𝑇 ↾ (𝐴 ∖ {𝑃})))))
Theorem	ablfac1eu 20012*	The factorization of ablfac1b 20009 is unique, in that any other factorization into prime power factors (even if the exponents are different) must be equal to 𝑆. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    &   ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    &   ⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵))    &   ⊢ (𝜑 → dom 𝑇 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶))    ⇒   ⊢ (𝜑 → 𝑇 = 𝑆)
Theorem	pgpfac1lem1 20013*	Lemma for pgpfac1 20019. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    &   ⊢ 𝑆 = (𝐾‘{𝐴})    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸)    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 })    &   ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈)    &   ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤))    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) = 𝑈)
Theorem	pgpfac1lem2 20014*	Lemma for pgpfac1 20019. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    &   ⊢ 𝑆 = (𝐾‘{𝐴})    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸)    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 })    &   ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈)    &   ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊)))    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝜑 → (𝑃 · 𝐶) ∈ (𝑆 ⊕ 𝑊))
Theorem	pgpfac1lem3a 20015*	Lemma for pgpfac1 20019. (Contributed by Mario Carneiro, 4-Jun-2016.)
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    &   ⊢ 𝑆 = (𝐾‘{𝐴})    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸)    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 })    &   ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈)    &   ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊)))    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → ((𝑃 · 𝐶)(+g‘𝐺)(𝑀 · 𝐴)) ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑃 ∥ 𝐸 ∧ 𝑃 ∥ 𝑀))
Theorem	pgpfac1lem3 20016*	Lemma for pgpfac1 20019. (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 20017*	Lemma for pgpfac1 20019. (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 20018*	Lemma for pgpfac1 20019. (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 20019*	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 20020*	Lemma for pgpfac 20023. (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 20021*	Lemma for pgpfac 20023. (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 20022*	Lemma for pgpfac 20023. (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 20023*	Full factorization of a finite abelian p-group, by iterating pgpfac1 20019. 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 20024*	Lemma for ablfac 20027. (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 20025*	Lemma for ablfac 20027. (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 20026*	Lemma for ablfac 20027. (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 20027*	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 20028*	Choose generators for each cyclic group in ablfac 20027. (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 20029	Extend class notation with the class of simple groups.
class SimpGrp
Definition	df-simpg 20030	Define class of all simple groups. A simple group is a group (df-grp 18875) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity (simpgnsgbid 20042). (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o}
Theorem	issimpg 20031	The predicate "is a simple group". (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝐺 ∈ SimpGrp ↔ (𝐺 ∈ Grp ∧ (NrmSGrp‘𝐺) ≈ 2o))
Theorem	issimpgd 20032	Deduce a simple group from its properties. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 2o)    ⇒   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)
Theorem	simpggrp 20033	A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝐺 ∈ SimpGrp → 𝐺 ∈ Grp)
Theorem	simpggrpd 20034	A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	simpg2nsg 20035	A simple group has two normal subgroups. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝐺 ∈ SimpGrp → (NrmSGrp‘𝐺) ≈ 2o)
Theorem	trivnsimpgd 20036	Trivial groups are not simple. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    ⇒   ⊢ (𝜑 → ¬ 𝐺 ∈ SimpGrp)
Theorem	simpgntrivd 20037	Simple groups are nontrivial. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → ¬ 𝐵 = { 0 })
Theorem	simpgnideld 20038*	A simple group contains a nonidentity element. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ¬ 𝑥 = 0 )
Theorem	simpgnsgd 20039	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 20040	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 20041*	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 20042	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 20043	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 20044*	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 20045	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 20046*	Lemma for ablsimpgfind 20049. 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 20047*	Lemma for ablsimpgfind 20049. 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 20048*	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 20049	An abelian simple group is finite. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → 𝐵 ∈ Fin)
Theorem	fincygsubgd 20050*	The subgroup referenced in fincygsubgodd 20051 is a subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐻 = (𝑛 ∈ ℤ ↦ (𝑛 · (𝐶 · 𝐴)))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    ⇒   ⊢ (𝜑 → ran 𝐻 ∈ (SubGrp‘𝐺))
Theorem	fincygsubgodd 20051*	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 20052*	A finite cyclic group has subgroups of every possible order. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CycGrp)    &   ⊢ (𝜑 → 𝐶 ∥ (♯‘𝐵))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (SubGrp‘𝐺)(♯‘𝑥) = 𝐶)
Theorem	prmgrpsimpgd 20053	A group of prime order is simple. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → (♯‘𝐵) ∈ ℙ)    ⇒   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)
Theorem	ablsimpgprmd 20054	An abelian simple group has prime order. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → (♯‘𝐵) ∈ ℙ)
Theorem	ablsimpgd 20055	An abelian group is simple if and only if its order is prime. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    ⇒   ⊢ (𝜑 → (𝐺 ∈ SimpGrp ↔ (♯‘𝐵) ∈ ℙ))
10.3  Rings
10.3.1  Multiplicative Group
Syntax	cmgp 20056	Multiplicative group.
class mulGrp
Definition	df-mgp 20057	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 20299 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 20155) or "the multiplicative identity" in terms of the identity of a monoid (df-ur 20098). (Contributed by Mario Carneiro, 21-Dec-2014.)
⊢ mulGrp = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(+g‘ndx), (.r‘𝑤)⟩))
Theorem	fnmgp 20058	The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.)
⊢ mulGrp Fn V
Theorem	mgpval 20059	Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
Theorem	mgpplusg 20060	Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ · = (+g‘𝑀)
Theorem	mgpbas 20061	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 20062	The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp 20243. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑆 = (Scalar‘𝑅)    ⇒   ⊢ 𝑆 = (Scalar‘𝑀)
Theorem	mgptset 20063	Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (TopSet‘𝑅) = (TopSet‘𝑀)
Theorem	mgptopn 20064	Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑅)    ⇒   ⊢ 𝐽 = (TopOpen‘𝑀)
Theorem	mgpds 20065	Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝐵 = (dist‘𝑅)    ⇒   ⊢ 𝐵 = (dist‘𝑀)
Theorem	mgpress 20066	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 20067	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 20068	Extend class notation with class of all non-unital rings.
class Rng
Definition	df-rng 20069*	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 20070*	The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧ 𝐺 ∈ Smgrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
Theorem	rngabl 20071	A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel)
Theorem	rngmgp 20072	A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020.)
⊢ 𝐺 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → 𝐺 ∈ Smgrp)
Theorem	rngmgpf 20073	Restricted functionality of the multiplicative group on non-unital rings (mgpf 20164 analog). (Contributed by AV, 22-Feb-2025.)
⊢ (mulGrp ↾ Rng):Rng⟶Smgrp
Theorem	rnggrp 20074	A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.)
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp)
Theorem	rngass 20075	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 20076	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 20077	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 20078	Closure of the addition operation of a non-unital ring. (Contributed by AV, 16-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	rng0cl 20079	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 20080	Closure of the multiplication operation of a non-unital ring. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
Theorem	rnglz 20081	The zero of a non-unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringlz 20209. (Revised by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = 0 )
Theorem	rngrz 20082	The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringrz 20210. (Revised by AV, 16-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵) → (𝑋 · 0 ) = 0 )
Theorem	rngmneg1 20083	Negation of a product in a non-unital ring (mulneg1 11621 analog). In contrast to ringmneg1 20220, 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 20084	Negation of a product in a non-unital ring (mulneg2 11622 analog). In contrast to ringmneg2 20221, 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 20085	Double negation of a product in a non-unital ring (mul2neg 11624 analog). (Contributed by Mario Carneiro, 4-Dec-2014.) Generalization of ringm2neg 20222. (Revised by AV, 17-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘𝑋) · (𝑁‘𝑌)) = (𝑋 · 𝑌))
Theorem	rngansg 20086	Every additive subgroup of a non-unital ring is normal. (Contributed by AV, 25-Feb-2025.)
⊢ (𝑅 ∈ Rng → (NrmSGrp‘𝑅) = (SubGrp‘𝑅))
Theorem	rngsubdi 20087	Ring multiplication distributes over subtraction. (subdi 11618 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdi 20223. (Revised by AV, 23-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑌 − 𝑍)) = ((𝑋 · 𝑌) − (𝑋 · 𝑍)))
Theorem	rngsubdir 20088	Ring multiplication distributes over subtraction. (subdir 11619 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdir 20224. (Revised by AV, 23-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 − 𝑌) · 𝑍) = ((𝑋 · 𝑍) − (𝑌 · 𝑍)))
Theorem	isrngd 20089*	Properties that determine a non-unital ring. (Contributed by AV, 14-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Abel)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))    ⇒   ⊢ (𝜑 → 𝑅 ∈ Rng)
Theorem	rngpropd 20090*	If two structures have the same base set, and the values of their group (addition) and ring (multiplication) operations are equal for all pairs of elements of the base set, one is a non-unital ring iff the other one is. (Contributed by AV, 15-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ Rng ↔ 𝐿 ∈ Rng))
Theorem	prdsmulrngcl 20091	Closure of the multiplication in a structure product of non-unital rings. (Contributed by Mario Carneiro, 11-Mar-2015.) Generalization of prdsmulrcl 20236. (Revised by AV, 21-Feb-2025.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ · = (.r‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Rng)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 · 𝐺) ∈ 𝐵)
Theorem	prdsrngd 20092	A product of non-unital rings is a non-unital ring. (Contributed by AV, 22-Feb-2025.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Rng)    ⇒   ⊢ (𝜑 → 𝑌 ∈ Rng)
Theorem	imasrng 20093*	The image structure of a non-unital ring is a non-unital ring (imasring 20246 analog). (Contributed by AV, 22-Feb-2025.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    ⇒   ⊢ (𝜑 → 𝑈 ∈ Rng)
Theorem	imasrngf1 20094	The image of a non-unital ring under an injection is a non-unital ring (imasmndf1 18710 analog). (Contributed by AV, 22-Feb-2025.)
⊢ 𝑈 = (𝐹 “s 𝑅)    &   ⊢ 𝑉 = (Base‘𝑅)    ⇒   ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ 𝑅 ∈ Rng) → 𝑈 ∈ Rng)
Theorem	xpsrngd 20095	A product of two non-unital rings is a non-unital ring (xpsmnd 18711 analog). (Contributed by AV, 22-Feb-2025.)
⊢ 𝑌 = (𝑆 ×s 𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ Rng)    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    ⇒   ⊢ (𝜑 → 𝑌 ∈ Rng)
Theorem	qusrng 20096*	The quotient structure of a non-unital ring is a non-unital ring (qusring2 20250 analog). (Contributed by AV, 23-Feb-2025.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 + 𝑏) ∼ (𝑝 + 𝑞)))    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))    &   ⊢ (𝜑 → 𝑅 ∈ Rng)    ⇒   ⊢ (𝜑 → 𝑈 ∈ Rng)
10.3.3  Ring unity (multiplicative identity) In Wikipedia "Identity element", see https://en.wikipedia.org/wiki/Identity_element (18-Jan-2025): "... an identity with respect to multiplication is called a multiplicative identity (often denoted as 1). ... The distinction between additive and multiplicative identity is used most often for sets that support both binary operations, such as rings, integral domains, and fields. The multiplicative identity is often called unity in the latter context (a ring with unity). This should not be confused with a unit in ring theory, which is any element having a multiplicative inverse. By its own definition, unity itself is necessarily a unit." Calling the multiplicative identity of a ring a unity is taken from the definition of a ring with unity in section 17.3 of [BeauregardFraleigh] p. 135, "A ring ( R , + , . ) is a ring with unity if R is not the zero ring and ( R , . ) is a monoid. In this case, the identity element of ( R , . ) is denoted by 1 and is called the unity of R." This definition of a "ring with unity" corresponds to our definition of a unital ring (see df-ring 20151). Some authors call the multiplicative identity "unit" or "unit element" (for example in section I, 2.2 of [BourbakiAlg1] p. 14, definition in section 1.3 of [Hall] p. 4, or in section I, 1 of [Lang] p. 3), whereas other authors use the term "unit" for an element having a multiplicative inverse (for example in section 17.3 of [BeauregardFraleigh] p. 135, in definition in [Roman] p. 26, or even in section II, 1 of [Lang] p. 84). Sometimes, the multiplicative identity is simply called "one" (see, for example, chapter 8 in [Schechter] p. 180). To avoid this ambiguity of the term "unit", also mentioned in Wikipedia, we call the multiplicative identity of a structure with a multiplication (usually a ring) a "ring unity", or straightly "multiplicative identity". The term "unit" will be used for an element having a multiplicative inverse (see df-unit 20274), and we have "the ring unity is a unit", see 1unit 20290.
Syntax	cur 20097	Extend class notation with ring unity.
class 1r
Definition	df-ur 20098	Define the multiplicative identity, i.e., the monoid identity (df-0g 17411) of the multiplicative monoid (df-mgp 20057) of a ring-like structure. This multiplicative identity is also called "ring unity" or "unity element". This definition works by transferring the multiplicative operation from the .r slot to the +g slot and then looking at the element which is then the 0g element, that is an identity with respect to the operation which started out in the .r slot. See also dfur2 20100, which derives the "traditional" definition as the unique element of a ring which is left- and right-neutral under multiplication. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ 1r = (0g ∘ mulGrp)
Theorem	ringidval 20099	The value of the unity element of a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ 1 = (0g‘𝐺)
Theorem	dfur2 20100*	The multiplicative identity is the unique element of the ring that is left- and right-neutral on all elements under multiplication. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ 1 = (℩𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 · 𝑥) = 𝑥 ∧ (𝑥 · 𝑒) = 𝑥)))