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	gsummptmhm 20001*	Apply a group homomorphism to a group sum expressed with a mapping. (Contributed by Thierry Arnoux, 7-Sep-2018.) (Revised by AV, 8-Sep-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐻 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐺 MndHom 𝐻))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐻 Σg (𝑥 ∈ 𝐴 ↦ (𝐾‘𝐶))) = (𝐾‘(𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝐶))))
Theorem	gsummulglem 20002*	Lemma for gsummulg 20003 and gsummulgz 20004. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 6-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 )    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → (𝐺 ∈ Abel ∨ 𝑁 ∈ ℕ0))    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ (𝑁 · 𝑋))) = (𝑁 · (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋))))
Theorem	gsummulg 20003*	Nonnegative multiple of a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 6-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 )    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ (𝑁 · 𝑋))) = (𝑁 · (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋))))
Theorem	gsummulgz 20004*	Integer multiple of a group sum. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 6-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 )    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ (𝑁 · 𝑋))) = (𝑁 · (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋))))
Theorem	gsumzoppg 20005	The opposite of a group sum is the same as the original. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 6-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝑂 = (oppg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑂 Σg 𝐹) = (𝐺 Σg 𝐹))
Theorem	gsumzinv 20006	Inverse of a group sum. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 6-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐼 ∘ 𝐹)) = (𝐼‘(𝐺 Σg 𝐹)))
Theorem	gsuminv 20007	Inverse of a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 4-May-2015.) (Revised by AV, 6-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐼 ∘ 𝐹)) = (𝐼‘(𝐺 Σg 𝐹)))
Theorem	gsummptfidminv 20008*	Inverse of a group sum expressed as mapping with a finite domain. (Contributed by AV, 23-Jul-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐼 ∘ 𝐹)) = (𝐼‘(𝐺 Σg 𝐹)))
Theorem	gsumsub 20009	The difference of two group sums. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 6-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ (𝜑 → 𝐻 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐹 ∘f − 𝐻)) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻)))
Theorem	gsummptfssub 20010*	The difference of two group sums expressed as mappings. (Contributed by AV, 7-Nov-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶))    &   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐴 ↦ 𝐷))    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ (𝜑 → 𝐻 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐷))) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻)))
Theorem	gsummptfidmsub 20011*	The difference of two group sums expressed as mappings with finite domain. (Contributed by AV, 7-Nov-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ 𝐷)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐷))) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻)))
Theorem	gsumsnfd 20012*	Group sum of a singleton, deduction form, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, 28-Mar-2018.) (Revised by AV, 11-Dec-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝐴 = 𝐶)    &   ⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐶    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ {𝑀} ↦ 𝐴)) = 𝐶)
Theorem	gsumsnd 20013*	Group sum of a singleton, deduction form. (Contributed by Thierry Arnoux, 30-Jan-2017.) (Proof shortened by AV, 11-Dec-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ {𝑀} ↦ 𝐴)) = 𝐶)
Theorem	gsumsnf 20014*	Group sum of a singleton, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, 28-Mar-2018.) (Proof shortened by AV, 11-Dec-2019.)
⊢ Ⅎ𝑘𝐶    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐶)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ {𝑀} ↦ 𝐴)) = 𝐶)
Theorem	gsumsn 20015*	Group sum of a singleton. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Proof shortened by AV, 11-Dec-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐶)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ {𝑀} ↦ 𝐴)) = 𝐶)
Theorem	gsumpr 20016*	Group sum of a pair. (Contributed by AV, 6-Dec-2018.) (Proof shortened by AV, 28-Jul-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐶)    &   ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐷)    ⇒   ⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → (𝐺 Σg (𝑘 ∈ {𝑀, 𝑁} ↦ 𝐴)) = (𝐶 + 𝐷))
Theorem	gsumzunsnd 20017*	Append an element to a finite group sum, more general version of gsumunsnd 20019. (Contributed by AV, 7-Oct-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝐹 = (𝑘 ∈ (𝐴 ∪ {𝑀}) ↦ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑀 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) + 𝑌))
Theorem	gsumunsnfd 20018*	Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 11-Dec-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑀 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌)    &   ⊢ Ⅎ𝑘𝑌    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 ∪ {𝑀}) ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) + 𝑌))
Theorem	gsumunsnd 20019*	Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 2-Jan-2019.) (Proof shortened by AV, 11-Dec-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑀 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 ∪ {𝑀}) ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) + 𝑌))
Theorem	gsumunsnf 20020*	Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, 28-Mar-2018.) (Proof shortened by AV, 11-Dec-2019.)
⊢ Ⅎ𝑘𝑌    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑀 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝑘 = 𝑀 → 𝑋 = 𝑌)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 ∪ {𝑀}) ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) + 𝑌))
Theorem	gsumunsn 20021*	Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014.) (Proof shortened by AV, 8-Mar-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑀 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝑘 = 𝑀 → 𝑋 = 𝑌)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 ∪ {𝑀}) ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) + 𝑌))
Theorem	gsumdifsnd 20022*	Extract a summand from a finitely supported group sum. (Contributed by AV, 21-Apr-2019.) (Revised by AV, 28-Jul-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp (0g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ (𝐴 ∖ {𝑀}) ↦ 𝑋)) + 𝑌))
Theorem	gsumpt 20023	Sum of a family that is nonzero at at most one point. (Contributed by Stefan O'Rear, 7-Feb-2015.) (Revised by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 6-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ {𝑋})    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐹‘𝑋))
Theorem	gsummptf1o 20024*	Re-index a finite group sum using a bijection. (Contributed by Thierry Arnoux, 29-Mar-2018.)
⊢ Ⅎ𝑥𝐻    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝑥 = 𝐸 → 𝐶 = 𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐹)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐸 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 ∈ 𝐷 𝑥 = 𝐸)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝐺 Σg (𝑦 ∈ 𝐷 ↦ 𝐻)))
Theorem	gsummptun 20025*	Group sum of a disjoint union, whereas sums are expressed as mappings. (Contributed by Thierry Arnoux, 28-Mar-2018.) (Proof shortened by AV, 11-Dec-2019.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ CMnd)    &   ⊢ (𝜑 → (𝐴 ∪ 𝐶) ∈ Fin)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ 𝐶)) → 𝐷 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ (𝐴 ∪ 𝐶) ↦ 𝐷)) = ((𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐷)) + (𝑊 Σg (𝑥 ∈ 𝐶 ↦ 𝐷))))
Theorem	gsummpt1n0 20026*	If only one summand in a finite group sum is not zero, the whole sum equals this summand. More general version of gsummptif1n0 20027. (Contributed by AV, 11-Oct-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ 𝐹 = (𝑛 ∈ 𝐼 ↦ if(𝑛 = 𝑋, 𝐴, 0 ))    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝐼 𝐴 ∈ (Base‘𝐺))    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = ⦋𝑋 / 𝑛⦌𝐴)
Theorem	gsummptif1n0 20027*	If only one summand in a finite group sum is not zero, the whole sum equals this summand. (Contributed by AV, 17-Feb-2019.) (Proof shortened by AV, 11-Oct-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ 𝐹 = (𝑛 ∈ 𝐼 ↦ if(𝑛 = 𝑋, 𝐴, 0 ))    &   ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐺))    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = 𝐴)
Theorem	gsummptcl 20028*	Closure of a finite group sum over a finite set as map. (Contributed by AV, 29-Dec-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ 𝑁 ↦ 𝑋)) ∈ 𝐵)
Theorem	gsummptfif1o 20029*	Re-index a finite group sum as map, using a bijection. (Contributed by by AV, 23-Jul-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑖 ∈ 𝑁 ↦ 𝑋)    &   ⊢ (𝜑 → 𝐻:𝐶–1-1-onto→𝑁)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻)))
Theorem	gsummptfzcl 20030*	Closure of a finite group sum over a finite set of sequential integers as map. (Contributed by AV, 14-Dec-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝐼 = (𝑀...𝑁))    &   ⊢ (𝜑 → ∀𝑖 ∈ 𝐼 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ 𝐼 ↦ 𝑋)) ∈ 𝐵)
Theorem	gsum2dlem1 20031*	Lemma 1 for gsum2d 20033. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → Rel 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → dom 𝐴 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
Theorem	gsum2dlem2 20032*	Lemma for gsum2d 20033. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → Rel 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → dom 𝐴 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
Theorem	gsum2d 20033*	Write a sum over a two-dimensional region as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → Rel 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → dom 𝐴 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
Theorem	gsum2d2lem 20034*	Lemma for gsum2d2 20035: show the function is finitely supported. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 9-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 )    ⇒   ⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 )
Theorem	gsum2d2 20035*	Write a group sum over a two-dimensional region as a double sum. Note that 𝐶(𝑗) is a function of 𝑗. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)))))
Theorem	gsumcom2 20036*	Two-dimensional commutation of a group sum. Note that while 𝐴 and 𝐷 are constants w.r.t. 𝑗, 𝑘, 𝐶(𝑗) and 𝐸(𝑘) are not. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 )    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ↔ (𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸)))    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ 𝑋)))
Theorem	gsumxp 20037*	Write a group sum over a cartesian product as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 9-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))))
Theorem	gsumcom 20038*	Commute the arguments of a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg (𝑘 ∈ 𝐶, 𝑗 ∈ 𝐴 ↦ 𝑋)))
Theorem	gsumcom3 20039*	A commutative law for finitely supported iterated sums. (Contributed by Stefan O'Rear, 2-Nov-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)))) = (𝐺 Σg (𝑘 ∈ 𝐶 ↦ (𝐺 Σg (𝑗 ∈ 𝐴 ↦ 𝑋)))))
Theorem	gsumcom3fi 20040*	A commutative law for finite iterated sums. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ Fin)    &   ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)))) = (𝐺 Σg (𝑘 ∈ 𝐶 ↦ (𝐺 Σg (𝑗 ∈ 𝐴 ↦ 𝑋)))))
Theorem	gsumxp2 20041*	Write a group sum over a cartesian product as a double sum in two ways. This corresponds to the first equation in [Lang] p. 6. (Contributed by AV, 27-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐶 ↦ (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))))
Theorem	prdsgsum 20042*	Finite commutative sums in a product structure are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by Mario Carneiro, 3-Jul-2015.) (Revised by AV, 9-Jun-2019.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CMnd)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))))
Theorem	pwsgsum 20043*	Finite commutative sums in a power structure are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by Mario Carneiro, 3-Jul-2015.) (Revised by AV, 9-Jun-2019.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CMnd)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))))
10.2.14.4  Group sums over (ranges of) integers
Theorem	fsfnn0gsumfsffz 20044*	Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m ℕ0))    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ 𝐻 = (𝐹 ↾ (0...𝑆))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ ℕ0 (𝑆 < 𝑥 → (𝐹‘𝑥) = 0 ) → (𝐺 Σg 𝐹) = (𝐺 Σg 𝐻)))
Theorem	nn0gsumfz 20045*	Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m ℕ0))    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ ℕ0 ∃𝑓 ∈ (𝐵 ↑m (0...𝑠))(𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓)))
Theorem	nn0gsumfz0 20046*	Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m ℕ0))    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ ℕ0 ∃𝑓 ∈ (𝐵 ↑m (0...𝑠))(𝐺 Σg 𝐹) = (𝐺 Σg 𝑓))
Theorem	gsummptnn0fz 20047*	A final group sum over a function over the nonnegative integers (given as mapping) is equal to a final group sum over a finite interval of nonnegative integers. (Contributed by AV, 10-Oct-2019.) (Revised by AV, 3-Jul-2022.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝑆 < 𝑘 → 𝐶 = 0 ))    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ ℕ0 ↦ 𝐶)) = (𝐺 Σg (𝑘 ∈ (0...𝑆) ↦ 𝐶)))
Theorem	gsummptnn0fzfv 20048*	A final group sum over a function over the nonnegative integers (given as mapping to its function values) is equal to a final group sum over a finite interval of nonnegative integers. (Contributed by AV, 10-Oct-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m ℕ0))    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ0 (𝑆 < 𝑥 → (𝐹‘𝑥) = 0 ))    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ ℕ0 ↦ (𝐹‘𝑘))) = (𝐺 Σg (𝑘 ∈ (0...𝑆) ↦ (𝐹‘𝑘))))
Theorem	telgsumfzslem 20049*	Lemma for telgsumfzs 20050 (induction step). (Contributed by AV, 23-Nov-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝑦 ∈ (ℤ≥‘𝑀) ∧ (𝜑 ∧ ∀𝑘 ∈ (𝑀...((𝑦 + 1) + 1))𝐶 ∈ 𝐵)) → ((𝐺 Σg (𝑖 ∈ (𝑀...𝑦) ↦ (⦋𝑖 / 𝑘⦌𝐶 − ⦋(𝑖 + 1) / 𝑘⦌𝐶))) = (⦋𝑀 / 𝑘⦌𝐶 − ⦋(𝑦 + 1) / 𝑘⦌𝐶) → (𝐺 Σg (𝑖 ∈ (𝑀...(𝑦 + 1)) ↦ (⦋𝑖 / 𝑘⦌𝐶 − ⦋(𝑖 + 1) / 𝑘⦌𝐶))) = (⦋𝑀 / 𝑘⦌𝐶 − ⦋((𝑦 + 1) + 1) / 𝑘⦌𝐶)))
Theorem	telgsumfzs 20050*	Telescoping group sum ranging over a finite set of sequential integers, using explicit substitution. (Contributed by AV, 23-Nov-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...(𝑁 + 1))𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ (𝑀...𝑁) ↦ (⦋𝑖 / 𝑘⦌𝐶 − ⦋(𝑖 + 1) / 𝑘⦌𝐶))) = (⦋𝑀 / 𝑘⦌𝐶 − ⦋(𝑁 + 1) / 𝑘⦌𝐶))
Theorem	telgsumfz 20051*	Telescoping group sum ranging over a finite set of sequential integers, using implicit substitution, analogous to telfsum 15846. (Contributed by AV, 23-Nov-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...(𝑁 + 1))𝐴 ∈ 𝐵)    &   ⊢ (𝑘 = 𝑖 → 𝐴 = 𝐿)    &   ⊢ (𝑘 = (𝑖 + 1) → 𝐴 = 𝐶)    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷)    &   ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐸)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ (𝑀...𝑁) ↦ (𝐿 − 𝐶))) = (𝐷 − 𝐸))
Theorem	telgsumfz0s 20052*	Telescoping finite group sum ranging over nonnegative integers, using explicit substitution. (Contributed by AV, 24-Oct-2019.) (Proof shortened by AV, 25-Nov-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0...(𝑆 + 1))𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ (0...𝑆) ↦ (⦋𝑖 / 𝑘⦌𝐶 − ⦋(𝑖 + 1) / 𝑘⦌𝐶))) = (⦋0 / 𝑘⦌𝐶 − ⦋(𝑆 + 1) / 𝑘⦌𝐶))
Theorem	telgsumfz0 20053*	Telescoping finite group sum ranging over nonnegative integers, using implicit substitution, analogous to telfsum 15846. (Contributed by AV, 23-Nov-2019.)
⊢ 𝐾 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0...(𝑆 + 1))𝐴 ∈ 𝐾)    &   ⊢ (𝑘 = 𝑖 → 𝐴 = 𝐵)    &   ⊢ (𝑘 = (𝑖 + 1) → 𝐴 = 𝐶)    &   ⊢ (𝑘 = 0 → 𝐴 = 𝐷)    &   ⊢ (𝑘 = (𝑆 + 1) → 𝐴 = 𝐸)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ (0...𝑆) ↦ (𝐵 − 𝐶))) = (𝐷 − 𝐸))
Theorem	telgsums 20054*	Telescoping finitely supported group sum ranging over nonnegative integers, using explicit substitution. (Contributed by AV, 24-Oct-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝑆 < 𝑘 → 𝐶 = 0 ))    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ ℕ0 ↦ (⦋𝑖 / 𝑘⦌𝐶 − ⦋(𝑖 + 1) / 𝑘⦌𝐶))) = ⦋0 / 𝑘⦌𝐶)
Theorem	telgsum 20055*	Telescoping finitely supported group sum ranging over nonnegative integers, using implicit substitution. (Contributed by AV, 31-Dec-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝑆 < 𝑘 → 𝐴 = 0 ))    &   ⊢ (𝑘 = 𝑖 → 𝐴 = 𝐶)    &   ⊢ (𝑘 = (𝑖 + 1) → 𝐴 = 𝐷)    &   ⊢ (𝑘 = 0 → 𝐴 = 𝐸)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ ℕ0 ↦ (𝐶 − 𝐷))) = 𝐸)
10.2.14.5  Internal direct products
Syntax	cdprd 20056	Internal direct product of a family of subgroups.
class DProd
Syntax	cdpj 20057	Projection operator for a direct product.
class dProj
Definition	df-dprd 20058*	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 20059*	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 20060	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 20061*	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 20062*	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 20063	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 20064	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 20065	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 20066*	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 20067*	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 20068	Reverse closure for the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp)
Theorem	dprdf 20069	The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝐺dom DProd 𝑆 → 𝑆:dom 𝑆⟶(SubGrp‘𝐺))
Theorem	dprdf2 20070	The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    ⇒   ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺))
Theorem	dprdcntz 20071	The function 𝑆 is a family having pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))
Theorem	dprddisj 20072	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 20073*	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 20074*	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 20075*	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 20076*	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 20077*	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 20078*	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 20079	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 20080*	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 20081*	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 20082*	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 20083*	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 20084*	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 20085*	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 20086*	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 20087	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 20088	Each factor is a subset of the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝐺 DProd 𝑆))
Theorem	dprdlub 20089*	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 20090	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 20091	Restriction of a direct product (dropping factors). (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐴) ∧ (𝐺 DProd (𝑆 ↾ 𝐴)) ⊆ (𝐺 DProd 𝑆)))
Theorem	dprdss 20092*	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 20093*	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 20094	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 20095	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 20096	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 20097	A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubGrp‘𝐺) → (𝐻dom DProd 𝑆 ↔ (𝐺dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴)))
Theorem	subgdprd 20098	A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 𝐴)    ⇒   ⊢ (𝜑 → (𝐻 DProd 𝑆) = (𝐺 DProd 𝑆))
Theorem	dprdsn 20099	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 20100*	Lemma for dmdprdsplit 20110. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }    &   ⊢ (𝜑 → 𝐺dom DProd 𝑆)    &   ⊢ (𝜑 → dom 𝑆 = 𝐼)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    &   ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ (𝐺 DProd (𝑆 ↾ 𝐴)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐼 ∖ 𝐴)) → (𝐹‘𝑋) = 0 )