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	subgdprd 20001	A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 𝐴)    ⇒   ⊢ (𝜑 → (𝐻 DProd 𝑆) = (𝐺 DProd 𝑆))
Theorem	dprdsn 20002	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 20003*	Lemma for dmdprdsplit 20013. (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 20004	The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐼)    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))))
Theorem	dprddisj2 20005	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 20006*	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 20007*	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 20008*	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 20009*	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 20010*	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 20011	Lemma for dmdprdsplit 20013. (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 20012	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 20013	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 20014	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 20015	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 20016	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 20017	Lemma for theorems about direct product projection. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ {𝑋})) = (𝑆‘𝑋))
Theorem	dpjcntz 20018	The two subgroups that appear in dpjval 20022 commute. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))))
Theorem	dpjdisj 20019	The two subgroups that appear in dpjval 20022 are disjoint. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑋) ∩ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))) = { 0 })
Theorem	dpjlsm 20020	The two subgroups that appear in dpjval 20022 add to the full direct product. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (𝜑 → (𝐺 DProd 𝑆) = ((𝑆‘𝑋) ⊕ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))))
Theorem	dpjfval 20021*	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 20022	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 20023	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 20024*	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 20025*	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 20026*	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 20027	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 20028	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 20029	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 20030	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 20031*	Lemma for ablfacrp2 20033. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀}    &   ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    &   ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁))    ⇒   ⊢ (𝜑 → ((♯‘𝐾) gcd 𝑁) = 1)
Theorem	ablfacrp 20032*	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 20033*	The factors 𝐾, 𝐿 of ablfacrp 20032 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 20034*	Lemma for ablfac1b 20036. Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    &   ⊢ 𝑀 = (𝑃↑(𝑃 pCnt (♯‘𝐵)))    &   ⊢ 𝑁 = ((♯‘𝐵) / 𝑀)    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑀 gcd 𝑁) = 1 ∧ (♯‘𝐵) = (𝑀 · 𝑁)))
Theorem	ablfac1a 20035*	The factors of ablfac1b 20036 are of prime power order. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → (♯‘(𝑆‘𝑃)) = (𝑃↑(𝑃 pCnt (♯‘𝐵))))
Theorem	ablfac1b 20036*	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 20037*	The factors of ablfac1b 20036 cover the entire group. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    &   ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝐵)
Theorem	ablfac1eulem 20038*	Lemma for ablfac1eu 20039. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    &   ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    &   ⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵))    &   ⊢ (𝜑 → dom 𝑇 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → ¬ 𝑃 ∥ (♯‘(𝐺 DProd (𝑇 ↾ (𝐴 ∖ {𝑃})))))
Theorem	ablfac1eu 20039*	The factorization of ablfac1b 20036 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 20040*	Lemma for pgpfac1 20046. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    &   ⊢ 𝑆 = (𝐾‘{𝐴})    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸)    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 })    &   ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈)    &   ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤))    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) = 𝑈)
Theorem	pgpfac1lem2 20041*	Lemma for pgpfac1 20046. (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 20042*	Lemma for pgpfac1 20046. (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 20043*	Lemma for pgpfac1 20046. (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 20044*	Lemma for pgpfac1 20046. (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 20045*	Lemma for pgpfac1 20046. (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 20046*	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 20047*	Lemma for pgpfac 20050. (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 20048*	Lemma for pgpfac 20050. (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 20049*	Lemma for pgpfac 20050. (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 20050*	Full factorization of a finite abelian p-group, by iterating pgpfac1 20046. 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 20051*	Lemma for ablfac 20054. (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 20052*	Lemma for ablfac 20054. (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 20053*	Lemma for ablfac 20054. (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 20054*	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 20055*	Choose generators for each cyclic group in ablfac 20054. (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 20056	Extend class notation with the class of simple groups.
class SimpGrp
Definition	df-simpg 20057	Define class of all simple groups. A simple group is a group (df-grp 18901) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity (simpgnsgbid 20069). (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o}
Theorem	issimpg 20058	The predicate "is a simple group". (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝐺 ∈ SimpGrp ↔ (𝐺 ∈ Grp ∧ (NrmSGrp‘𝐺) ≈ 2o))
Theorem	issimpgd 20059	Deduce a simple group from its properties. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 2o)    ⇒   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)
Theorem	simpggrp 20060	A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝐺 ∈ SimpGrp → 𝐺 ∈ Grp)
Theorem	simpggrpd 20061	A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	simpg2nsg 20062	A simple group has two normal subgroups. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝐺 ∈ SimpGrp → (NrmSGrp‘𝐺) ≈ 2o)
Theorem	trivnsimpgd 20063	Trivial groups are not simple. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    ⇒   ⊢ (𝜑 → ¬ 𝐺 ∈ SimpGrp)
Theorem	simpgntrivd 20064	Simple groups are nontrivial. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → ¬ 𝐵 = { 0 })
Theorem	simpgnideld 20065*	A simple group contains a nonidentity element. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ¬ 𝑥 = 0 )
Theorem	simpgnsgd 20066	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 20067	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 20068*	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 20069	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 20070	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 20071*	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 20072	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 20073*	Lemma for ablsimpgfind 20076. 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 20074*	Lemma for ablsimpgfind 20076. 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 20075*	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 20076	An abelian simple group is finite. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → 𝐵 ∈ Fin)
Theorem	fincygsubgd 20077*	The subgroup referenced in fincygsubgodd 20078 is a subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐻 = (𝑛 ∈ ℤ ↦ (𝑛 · (𝐶 · 𝐴)))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    ⇒   ⊢ (𝜑 → ran 𝐻 ∈ (SubGrp‘𝐺))
Theorem	fincygsubgodd 20078*	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 20079*	A finite cyclic group has subgroups of every possible order. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CycGrp)    &   ⊢ (𝜑 → 𝐶 ∥ (♯‘𝐵))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (SubGrp‘𝐺)(♯‘𝑥) = 𝐶)
Theorem	prmgrpsimpgd 20080	A group of prime order is simple. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → (♯‘𝐵) ∈ ℙ)    ⇒   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)
Theorem	ablsimpgprmd 20081	An abelian simple group has prime order. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → (♯‘𝐵) ∈ ℙ)
Theorem	ablsimpgd 20082	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 20083	Extend class notation with the class of all right ordered monoids.
class oMnd
Syntax	cogrp 20084	Extend class notation with the class of all right ordered groups.
class oGrp
Definition	df-omnd 20085*	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 20086	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 20087*	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 20088	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 20089	A left-ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018.)
⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp)
Theorem	omndmnd 20090	A left-ordered monoid is a monoid. (Contributed by Thierry Arnoux, 13-Mar-2018.)
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Mnd)
Theorem	omndtos 20091	A left-ordered monoid is a totally ordered set. (Contributed by Thierry Arnoux, 13-Mar-2018.)
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset)
Theorem	omndadd 20092	In an ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ≤ = (le‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 + 𝑍) ≤ (𝑌 + 𝑍))
Theorem	omndaddr 20093	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 20094	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 20095	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 20096	A submonoid of an ordered monoid is also ordered. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ oMnd)
Theorem	omndmul2 20097	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 20098	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 20099	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 20100	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 ))