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	dprdsubg 20001	The internal direct product of a family of subgroups is a subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺))
Theorem	dprdub 20002	Each factor is a subset of the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝐺 DProd 𝑆))
Theorem	dprdlub 20003*	The direct product is smaller than any subgroup which contains the factors. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑆‘𝑘) ⊆ 𝑇)    ⇒   ⊢ (𝜑 → (𝐺 DProd 𝑆) ⊆ 𝑇)
Theorem	dprdspan 20004	The direct product is the span of the union of the factors. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) = (𝐾‘∪ ran 𝑆))
Theorem	dprdres 20005	Restriction of a direct product (dropping factors). (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐴) ∧ (𝐺 DProd (𝑆 ↾ 𝐴)) ⊆ (𝐺 DProd 𝑆)))
Theorem	dprdss 20006*	Create a direct product by finding subgroups inside each factor of another direct product. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑇)    &   ⊢ (𝜑 → dom 𝑇 = 𝐼)    &   ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑆‘𝑘) ⊆ (𝑇‘𝑘))    ⇒   ⊢ (𝜑 → (𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) ⊆ (𝐺 DProd 𝑇)))
Theorem	dprdz 20007*	A family consisting entirely of trivial groups is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → (𝐺dom DProd (𝑥 ∈ 𝐼 ↦ { 0 }) ∧ (𝐺 DProd (𝑥 ∈ 𝐼 ↦ { 0 })) = { 0 }))
Theorem	dprd0 20008	The empty family is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = { 0 }))
Theorem	dprdf1o 20009	Rearrange the index set of a direct product family. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐹:𝐽–1-1-onto→𝐼)    ⇒   ⊢ (𝜑 → (𝐺dom DProd (𝑆 ∘ 𝐹) ∧ (𝐺 DProd (𝑆 ∘ 𝐹)) = (𝐺 DProd 𝑆)))
Theorem	dprdf1 20010	Rearrange the index set of a direct product family. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐹:𝐽–1-1→𝐼)    ⇒   ⊢ (𝜑 → (𝐺dom DProd (𝑆 ∘ 𝐹) ∧ (𝐺 DProd (𝑆 ∘ 𝐹)) ⊆ (𝐺 DProd 𝑆)))
Theorem	subgdmdprd 20011	A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubGrp‘𝐺) → (𝐻dom DProd 𝑆 ↔ (𝐺dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴)))
Theorem	subgdprd 20012	A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 𝐴)    ⇒   ⊢ (𝜑 → (𝐻 DProd 𝑆) = (𝐺 DProd 𝑆))
Theorem	dprdsn 20013	A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {⟨𝐴, 𝑆⟩} ∧ (𝐺 DProd {⟨𝐴, 𝑆⟩}) = 𝑆))
Theorem	dmdprdsplitlem 20014*	Lemma for dmdprdsplit 20024. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    &   ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ (𝐺 DProd (𝑆 ↾ 𝐴)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐼 ∖ 𝐴)) → (𝐹‘𝑋) = 0 )
Theorem	dprdcntz2 20015	The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐼)    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))))
Theorem	dprddisj2 20016	The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐼)    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 })
Theorem	dprd2dlem2 20017*	The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → Rel 𝐴)    &   ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))    &   ⊢ (𝜑 → dom 𝐴 ⊆ 𝐼)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))    &   ⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝑆‘𝑋) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑋)}) ↦ ((1st ‘𝑋)𝑆𝑗))))
Theorem	dprd2dlem1 20018*	The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → Rel 𝐴)    &   ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))    &   ⊢ (𝜑 → dom 𝐴 ⊆ 𝐼)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))    &   ⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) = (𝐺 DProd (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))
Theorem	dprd2da 20019*	The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → Rel 𝐴)    &   ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))    &   ⊢ (𝜑 → dom 𝐴 ⊆ 𝐼)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))    &   ⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ (𝜑 → 𝐺dom DProd 𝑆)
Theorem	dprd2db 20020*	The direct product of a collection of direct products. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → Rel 𝐴)    &   ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))    &   ⊢ (𝜑 → dom 𝐴 ⊆ 𝐼)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))    &   ⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ (𝜑 → (𝐺 DProd 𝑆) = (𝐺 DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))
Theorem	dprd2d2 20021*	The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ 𝐽 ↦ 𝑆))    &   ⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ 𝐽 ↦ 𝑆))))    ⇒   ⊢ (𝜑 → (𝐺dom DProd (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐽 ↦ 𝑆) ∧ (𝐺 DProd (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐽 ↦ 𝑆)) = (𝐺 DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ 𝐽 ↦ 𝑆))))))
Theorem	dmdprdsplit2lem 20022	Lemma for dmdprdsplit 20024. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷))    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐶))    &   ⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐷))    &   ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))))    &   ⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 })    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑌 ∈ 𝐼 → (𝑋 ≠ 𝑌 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))) ∧ ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ { 0 }))
Theorem	dmdprdsplit2 20023	The direct product splits into the direct product of any partition of the index set. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷))    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐶))    &   ⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐷))    &   ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))))    &   ⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 })    ⇒   ⊢ (𝜑 → 𝐺dom DProd 𝑆)
Theorem	dmdprdsplit 20024	The direct product splits into the direct product of any partition of the index set. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷))    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝜑 → (𝐺dom DProd 𝑆 ↔ ((𝐺dom DProd (𝑆 ↾ 𝐶) ∧ 𝐺dom DProd (𝑆 ↾ 𝐷)) ∧ (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))) ∧ ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 })))
Theorem	dprdsplit 20025	The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    ⇒   ⊢ (𝜑 → (𝐺 DProd 𝑆) = ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷))))
Theorem	dmdprdpr 20026	A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    ⇒   ⊢ (𝜑 → (𝐺dom DProd {⟨∅, 𝑆⟩, ⟨1o, 𝑇⟩} ↔ (𝑆 ⊆ (𝑍‘𝑇) ∧ (𝑆 ∩ 𝑇) = { 0 })))
Theorem	dprdpr 20027	A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ⊆ (𝑍‘𝑇))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = { 0 })    ⇒   ⊢ (𝜑 → (𝐺 DProd {⟨∅, 𝑆⟩, ⟨1o, 𝑇⟩}) = (𝑆 ⊕ 𝑇))
Theorem	dpjlem 20028	Lemma for theorems about direct product projection. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ {𝑋})) = (𝑆‘𝑋))
Theorem	dpjcntz 20029	The two subgroups that appear in dpjval 20033 commute. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))))
Theorem	dpjdisj 20030	The two subgroups that appear in dpjval 20033 are disjoint. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑋) ∩ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))) = { 0 })
Theorem	dpjlsm 20031	The two subgroups that appear in dpjval 20033 add to the full direct product. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (𝜑 → (𝐺 DProd 𝑆) = ((𝑆‘𝑋) ⊕ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))))
Theorem	dpjfval 20032*	Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ 𝑃 = (𝐺dProj𝑆)    &   ⊢ 𝑄 = (proj1‘𝐺)    ⇒   ⊢ (𝜑 → 𝑃 = (𝑖 ∈ 𝐼 ↦ ((𝑆‘𝑖)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖}))))))
Theorem	dpjval 20033	Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ 𝑃 = (𝐺dProj𝑆)    &   ⊢ 𝑄 = (proj1‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑃‘𝑋) = ((𝑆‘𝑋)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))))
Theorem	dpjf 20034	The 𝑋-th index projection is a function from the direct product to the 𝑋-th factor. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ 𝑃 = (𝐺dProj𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑃‘𝑋):(𝐺 DProd 𝑆)⟶(𝑆‘𝑋))
Theorem	dpjidcl 20035*	The key property of projections: the sum of all the projections of 𝐴 is 𝐴. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ 𝑃 = (𝐺dProj𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐺 DProd 𝑆))    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ ((𝑃‘𝑥)‘𝐴)) ∈ 𝑊 ∧ 𝐴 = (𝐺 Σg (𝑥 ∈ 𝐼 ↦ ((𝑃‘𝑥)‘𝐴)))))
Theorem	dpjeq 20036*	Decompose a group sum into projections. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ 𝑃 = (𝐺dProj𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐺 DProd 𝑆))    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐶) ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 = (𝐺 Σg (𝑥 ∈ 𝐼 ↦ 𝐶)) ↔ ∀𝑥 ∈ 𝐼 ((𝑃‘𝑥)‘𝐴) = 𝐶))
Theorem	dpjid 20037*	The key property of projections: the sum of all the projections of 𝐴 is 𝐴. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ 𝑃 = (𝐺dProj𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐺 DProd 𝑆))    ⇒   ⊢ (𝜑 → 𝐴 = (𝐺 Σg (𝑥 ∈ 𝐼 ↦ ((𝑃‘𝑥)‘𝐴))))
Theorem	dpjlid 20038	The 𝑋-th index projection acts as the identity on elements of the 𝑋-th factor. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ 𝑃 = (𝐺dProj𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑆‘𝑋))    ⇒   ⊢ (𝜑 → ((𝑃‘𝑋)‘𝐴) = 𝐴)
Theorem	dpjrid 20039	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 20040	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 20041	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 20042*	Lemma for ablfacrp2 20044. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀}    &   ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    &   ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁))    ⇒   ⊢ (𝜑 → ((♯‘𝐾) gcd 𝑁) = 1)
Theorem	ablfacrp 20043*	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 20044*	The factors 𝐾, 𝐿 of ablfacrp 20043 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 20045*	Lemma for ablfac1b 20047. Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    &   ⊢ 𝑀 = (𝑃↑(𝑃 pCnt (♯‘𝐵)))    &   ⊢ 𝑁 = ((♯‘𝐵) / 𝑀)    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑀 gcd 𝑁) = 1 ∧ (♯‘𝐵) = (𝑀 · 𝑁)))
Theorem	ablfac1a 20046*	The factors of ablfac1b 20047 are of prime power order. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → (♯‘(𝑆‘𝑃)) = (𝑃↑(𝑃 pCnt (♯‘𝐵))))
Theorem	ablfac1b 20047*	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 20048*	The factors of ablfac1b 20047 cover the entire group. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    &   ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝐵)
Theorem	ablfac1eulem 20049*	Lemma for ablfac1eu 20050. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    &   ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    &   ⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵))    &   ⊢ (𝜑 → dom 𝑇 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → ¬ 𝑃 ∥ (♯‘(𝐺 DProd (𝑇 ↾ (𝐴 ∖ {𝑃})))))
Theorem	ablfac1eu 20050*	The factorization of ablfac1b 20047 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 20051*	Lemma for pgpfac1 20057. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    &   ⊢ 𝑆 = (𝐾‘{𝐴})    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸)    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 })    &   ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈)    &   ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤))    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) = 𝑈)
Theorem	pgpfac1lem2 20052*	Lemma for pgpfac1 20057. (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 20053*	Lemma for pgpfac1 20057. (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 20054*	Lemma for pgpfac1 20057. (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 20055*	Lemma for pgpfac1 20057. (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 20056*	Lemma for pgpfac1 20057. (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 20057*	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 20058*	Lemma for pgpfac 20061. (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 20059*	Lemma for pgpfac 20061. (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 20060*	Lemma for pgpfac 20061. (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 20061*	Full factorization of a finite abelian p-group, by iterating pgpfac1 20057. 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 20062*	Lemma for ablfac 20065. (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 20063*	Lemma for ablfac 20065. (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 20064*	Lemma for ablfac 20065. (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 20065*	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 20066*	Choose generators for each cyclic group in ablfac 20065. (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 20067	Extend class notation with the class of simple groups.
class SimpGrp
Definition	df-simpg 20068	Define class of all simple groups. A simple group is a group (df-grp 18912) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity (simpgnsgbid 20080). (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o}
Theorem	issimpg 20069	The predicate "is a simple group". (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝐺 ∈ SimpGrp ↔ (𝐺 ∈ Grp ∧ (NrmSGrp‘𝐺) ≈ 2o))
Theorem	issimpgd 20070	Deduce a simple group from its properties. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 2o)    ⇒   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)
Theorem	simpggrp 20071	A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝐺 ∈ SimpGrp → 𝐺 ∈ Grp)
Theorem	simpggrpd 20072	A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	simpg2nsg 20073	A simple group has two normal subgroups. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝐺 ∈ SimpGrp → (NrmSGrp‘𝐺) ≈ 2o)
Theorem	trivnsimpgd 20074	Trivial groups are not simple. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    ⇒   ⊢ (𝜑 → ¬ 𝐺 ∈ SimpGrp)
Theorem	simpgntrivd 20075	Simple groups are nontrivial. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → ¬ 𝐵 = { 0 })
Theorem	simpgnideld 20076*	A simple group contains a nonidentity element. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ¬ 𝑥 = 0 )
Theorem	simpgnsgd 20077	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 20078	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 20079*	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 20080	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 20081	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 20082*	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 20083	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 20084*	Lemma for ablsimpgfind 20087. 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 20085*	Lemma for ablsimpgfind 20087. 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 20086*	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 20087	An abelian simple group is finite. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → 𝐵 ∈ Fin)
Theorem	fincygsubgd 20088*	The subgroup referenced in fincygsubgodd 20089 is a subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐻 = (𝑛 ∈ ℤ ↦ (𝑛 · (𝐶 · 𝐴)))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    ⇒   ⊢ (𝜑 → ran 𝐻 ∈ (SubGrp‘𝐺))
Theorem	fincygsubgodd 20089*	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 20090*	A finite cyclic group has subgroups of every possible order. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CycGrp)    &   ⊢ (𝜑 → 𝐶 ∥ (♯‘𝐵))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (SubGrp‘𝐺)(♯‘𝑥) = 𝐶)
Theorem	prmgrpsimpgd 20091	A group of prime order is simple. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → (♯‘𝐵) ∈ ℙ)    ⇒   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)
Theorem	ablsimpgprmd 20092	An abelian simple group has prime order. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → (♯‘𝐵) ∈ ℙ)
Theorem	ablsimpgd 20093	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 20094	Extend class notation with the class of all right ordered monoids.
class oMnd
Syntax	cogrp 20095	Extend class notation with the class of all right ordered groups.
class oGrp
Definition	df-omnd 20096*	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 20097	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 20098*	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 20099	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 20100	A left-ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018.)
⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp)