P. 200 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19901-20000   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cdpj 19901	Projection operator for a direct product.
class dProj
Definition	df-dprd 19902*	Define the internal direct product of a family of subgroups. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 11-Jul-2019.)
⊢ DProd = (𝑔 ∈ Grp, 𝑠 ∈ {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ “ (dom ℎ ∖ {𝑥})))) = {(0g‘𝑔)}))} ↦ ran (𝑓 ∈ {ℎ ∈ X𝑥 ∈ dom 𝑠(𝑠‘𝑥) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓)))
Definition	df-dpj 19903*	Define the projection operator for a direct product. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ dProj = (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠‘𝑖)(proj1‘𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))))
Theorem	reldmdprd 19904	The domain of the internal direct product operation is a relation. (Contributed by Mario Carneiro, 25-Apr-2016.) (Proof shortened by AV, 11-Jul-2019.)
⊢ Rel dom DProd
Theorem	dmdprd 19905*	The domain of definition of the internal direct product, which states that 𝑆 is a family of subgroups that mutually commute and have trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016.) (Proof shortened by AV, 11-Jul-2019.)
⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼) → (𝐺dom DProd 𝑆 ↔ (𝐺 ∈ Grp ∧ 𝑆:𝐼⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 }))))
Theorem	dmdprdd 19906*	Show that a given family is a direct product decomposition. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) ⊆ { 0 })    ⇒   ⊢ (𝜑 → 𝐺dom DProd 𝑆)
Theorem	dprddomprc 19907	A family of subgroups indexed by a proper class cannot be a family of subgroups for an internal direct product. (Contributed by AV, 13-Jul-2019.)
⊢ (dom 𝑆 ∉ V → ¬ 𝐺dom DProd 𝑆)
Theorem	dprddomcld 19908	If a family of subgroups is a family of subgroups for an internal direct product, then it is indexed by a set. (Contributed by AV, 13-Jul-2019.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    ⇒   ⊢ (𝜑 → 𝐼 ∈ V)
Theorem	dprdval0prc 19909	The internal direct product of a family of subgroups indexed by a proper class is empty. (Contributed by AV, 13-Jul-2019.)
⊢ (dom 𝑆 ∉ V → (𝐺 DProd 𝑆) = ∅)
Theorem	dprdval 19910*	The value of the internal direct product operation, which is a function mapping the (infinite, but finitely supported) cartesian product of subgroups (which mutually commute and have trivial intersections) to its (group) sum . (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    ⇒   ⊢ ((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) → (𝐺 DProd 𝑆) = ran (𝑓 ∈ 𝑊 ↦ (𝐺 Σg 𝑓)))
Theorem	eldprd 19911*	A class 𝐴 is an internal direct product iff it is the (group) sum of an infinite, but finitely supported cartesian product of subgroups (which mutually commute and have trivial intersections). (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    ⇒   ⊢ (dom 𝑆 = 𝐼 → (𝐴 ∈ (𝐺 DProd 𝑆) ↔ (𝐺dom DProd 𝑆 ∧ ∃𝑓 ∈ 𝑊 𝐴 = (𝐺 Σg 𝑓))))
Theorem	dprdgrp 19912	Reverse closure for the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp)
Theorem	dprdf 19913	The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝐺dom DProd 𝑆 → 𝑆:dom 𝑆⟶(SubGrp‘𝐺))
Theorem	dprdf2 19914	The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    ⇒   ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺))
Theorem	dprdcntz 19915	The function 𝑆 is a family having pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))
Theorem	dprddisj 19916	The function 𝑆 is a family having trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ (𝜑 → ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) = { 0 })
Theorem	dprdw 19917*	The property of being a finitely supported function in the family 𝑆. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝑊 ↔ (𝐹 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥) ∈ (𝑆‘𝑥) ∧ 𝐹 finSupp 0 )))
Theorem	dprdwd 19918*	A mapping being a finitely supported function in the family 𝑆. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) (Proof shortened by OpenAI, 30-Mar-2020.)
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐴 ∈ (𝑆‘𝑥))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐴) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐴) ∈ 𝑊)
Theorem	dprdff 19919*	A finitely supported function in 𝑆 is a function into the base. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)
Theorem	dprdfcl 19920*	A finitely supported function in 𝑆 has its 𝑋-th element in 𝑆(𝑋). (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐼) → (𝐹‘𝑋) ∈ (𝑆‘𝑋))
Theorem	dprdffsupp 19921*	A finitely supported function in 𝑆 is a finitely supported function. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 0 )
Theorem	dprdfcntz 19922*	A function on the elements of an internal direct product has pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
Theorem	dprdssv 19923	The internal direct product of a family of subgroups is a subset of the base. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 DProd 𝑆) ⊆ 𝐵
Theorem	dprdfid 19924*	A function mapping all but one arguments to zero sums to the value of this argument in a direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑆‘𝑋))    &   ⊢ 𝐹 = (𝑛 ∈ 𝐼 ↦ if(𝑛 = 𝑋, 𝐴, 0 ))    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝑊 ∧ (𝐺 Σg 𝐹) = 𝐴))
Theorem	eldprdi 19925*	The domain of definition of the internal direct product, which states that 𝑆 is a family of subgroups that mutually commute and have trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ (𝐺 DProd 𝑆))
Theorem	dprdfinv 19926*	Take the inverse of a group sum over a family of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝜑 → ((𝑁 ∘ 𝐹) ∈ 𝑊 ∧ (𝐺 Σg (𝑁 ∘ 𝐹)) = (𝑁‘(𝐺 Σg 𝐹))))
Theorem	dprdfadd 19927*	Take the sum of group sums over two families of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝜑 → ((𝐹 ∘f + 𝐻) ∈ 𝑊 ∧ (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
Theorem	dprdfsub 19928*	Take the difference of group sums over two families of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝜑 → ((𝐹 ∘f − 𝐻) ∈ 𝑊 ∧ (𝐺 Σg (𝐹 ∘f − 𝐻)) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻))))
Theorem	dprdfeq0 19929*	The zero function is the only function that sums to zero in a direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝐺 Σg 𝐹) = 0 ↔ 𝐹 = (𝑥 ∈ 𝐼 ↦ 0 )))
Theorem	dprdf11 19930*	Two group sums over a direct product that give the same value are equal as functions. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝐺 Σg 𝐹) = (𝐺 Σg 𝐻) ↔ 𝐹 = 𝐻))
Theorem	dprdsubg 19931	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 19932	Each factor is a subset of the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝐺 DProd 𝑆))
Theorem	dprdlub 19933*	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 19934	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 19935	Restriction of a direct product (dropping factors). (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐴) ∧ (𝐺 DProd (𝑆 ↾ 𝐴)) ⊆ (𝐺 DProd 𝑆)))
Theorem	dprdss 19936*	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 19937*	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 19938	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 19939	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 19940	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 19941	A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubGrp‘𝐺) → (𝐻dom DProd 𝑆 ↔ (𝐺dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴)))
Theorem	subgdprd 19942	A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 𝐴)    ⇒   ⊢ (𝜑 → (𝐻 DProd 𝑆) = (𝐺 DProd 𝑆))
Theorem	dprdsn 19943	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 19944*	Lemma for dmdprdsplit 19954. (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 19945	The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐼)    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))))
Theorem	dprddisj2 19946	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 19947*	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 19948*	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 19949*	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 19950*	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 19951*	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 19952	Lemma for dmdprdsplit 19954. (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 19953	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 19954	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 19955	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 19956	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 19957	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 19958	Lemma for theorems about direct product projection. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ {𝑋})) = (𝑆‘𝑋))
Theorem	dpjcntz 19959	The two subgroups that appear in dpjval 19963 commute. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))))
Theorem	dpjdisj 19960	The two subgroups that appear in dpjval 19963 are disjoint. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝜑 → ((𝑆‘𝑋) ∩ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))) = { 0 })
Theorem	dpjlsm 19961	The two subgroups that appear in dpjval 19963 add to the full direct product. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (𝜑 → (𝐺 DProd 𝑆) = ((𝑆‘𝑋) ⊕ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))))
Theorem	dpjfval 19962*	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 19963	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 19964	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 19965*	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 19966*	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 19967*	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 19968	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 19969	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 19970	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 19971	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 19972*	Lemma for ablfacrp2 19974. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀}    &   ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    &   ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁))    ⇒   ⊢ (𝜑 → ((♯‘𝐾) gcd 𝑁) = 1)
Theorem	ablfacrp 19973*	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 19974*	The factors 𝐾, 𝐿 of ablfacrp 19973 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 19975*	Lemma for ablfac1b 19977. Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    &   ⊢ 𝑀 = (𝑃↑(𝑃 pCnt (♯‘𝐵)))    &   ⊢ 𝑁 = ((♯‘𝐵) / 𝑀)    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑀 gcd 𝑁) = 1 ∧ (♯‘𝐵) = (𝑀 · 𝑁)))
Theorem	ablfac1a 19976*	The factors of ablfac1b 19977 are of prime power order. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → (♯‘(𝑆‘𝑃)) = (𝑃↑(𝑃 pCnt (♯‘𝐵))))
Theorem	ablfac1b 19977*	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 19978*	The factors of ablfac1b 19977 cover the entire group. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    &   ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝐵)
Theorem	ablfac1eulem 19979*	Lemma for ablfac1eu 19980. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℙ)    &   ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    &   ⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵))    &   ⊢ (𝜑 → dom 𝑇 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → ¬ 𝑃 ∥ (♯‘(𝐺 DProd (𝑇 ↾ (𝐴 ∖ {𝑃})))))
Theorem	ablfac1eu 19980*	The factorization of ablfac1b 19977 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 19981*	Lemma for pgpfac1 19987. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    &   ⊢ 𝑆 = (𝐾‘{𝐴})    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸)    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 })    &   ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈)    &   ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤))    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) = 𝑈)
Theorem	pgpfac1lem2 19982*	Lemma for pgpfac1 19987. (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 19983*	Lemma for pgpfac1 19987. (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 19984*	Lemma for pgpfac1 19987. (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 19985*	Lemma for pgpfac1 19987. (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 19986*	Lemma for pgpfac1 19987. (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 19987*	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 19988*	Lemma for pgpfac 19991. (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 19989*	Lemma for pgpfac 19991. (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 19990*	Lemma for pgpfac 19991. (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 19991*	Full factorization of a finite abelian p-group, by iterating pgpfac1 19987. 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 19992*	Lemma for ablfac 19995. (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 19993*	Lemma for ablfac 19995. (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 19994*	Lemma for ablfac 19995. (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 19995*	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 19996*	Choose generators for each cyclic group in ablfac 19995. (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 19997	Extend class notation with the class of simple groups.
class SimpGrp
Definition	df-simpg 19998	Define class of all simple groups. A simple group is a group (df-grp 18841) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity (simpgnsgbid 20010). (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o}
Theorem	issimpg 19999	The predicate "is a simple group". (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝐺 ∈ SimpGrp ↔ (𝐺 ∈ Grp ∧ (NrmSGrp‘𝐺) ≈ 2o))
Theorem	issimpgd 20000	Deduce a simple group from its properties. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 2o)    ⇒   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)