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
Theorem	lsmsubg2 19901	The sum of two subgroups is a subgroup. (Contributed by NM, 4-Feb-2014.) (Proof shortened by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊕ 𝑈) ∈ (SubGrp‘𝐺))
Theorem	lsm4 19902	Commutative/associative law for subgroup sum. (Contributed by NM, 26-Sep-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ (𝑄 ∈ (SubGrp‘𝐺) ∧ 𝑅 ∈ (SubGrp‘𝐺)) ∧ (𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺))) → ((𝑄 ⊕ 𝑅) ⊕ (𝑇 ⊕ 𝑈)) = ((𝑄 ⊕ 𝑇) ⊕ (𝑅 ⊕ 𝑈)))
Theorem	prdscmnd 19903	The product of a family of commutative monoids is commutative. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶CMnd)    ⇒   ⊢ (𝜑 → 𝑌 ∈ CMnd)
Theorem	prdsabld 19904	The product of a family of Abelian groups is an Abelian group. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Abel)    ⇒   ⊢ (𝜑 → 𝑌 ∈ Abel)
Theorem	pwscmn 19905	The structure power on a commutative monoid is commutative. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ CMnd ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ CMnd)
Theorem	pwsabl 19906	The structure power on an Abelian group is Abelian. (Contributed by Mario Carneiro, 21-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ Abel ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Abel)
Theorem	qusabl 19907	If 𝑌 is a subgroup of the abelian group 𝐺, then 𝐻 = 𝐺 / 𝑌 is an abelian group. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆))    ⇒   ⊢ ((𝐺 ∈ Abel ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Abel)
Theorem	abl1 19908	The (smallest) structure representing a trivial abelian group. (Contributed by AV, 28-Apr-2019.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩}    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Abel)
Theorem	abln0 19909	Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019.)
⊢ Abel ≠ ∅
Theorem	cnaddablx 19910	The complex numbers are an Abelian group under addition. This version of cnaddabl 19911 shows the explicit structure "scaffold" we chose for the definition for Abelian groups. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use cnaddabl 19911 instead. (New usage is discouraged.) (Contributed by NM, 18-Oct-2012.)
⊢ 𝐺 = {⟨1, ℂ⟩, ⟨2, + ⟩}    ⇒   ⊢ 𝐺 ∈ Abel
Theorem	cnaddabl 19911	The complex numbers are an Abelian group under addition. This version of cnaddablx 19910 hides the explicit structure indices i.e. is "scaffold-independent". Note that the proof also does not reference explicit structure indices. The actual structure is dependent on how Base and +g is defined. This theorem should not be referenced in any proof. For the group/ring properties of the complex numbers, see cnring 21426. (Contributed by NM, 20-Oct-2012.) (New usage is discouraged.)
⊢ 𝐺 = {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩}    ⇒   ⊢ 𝐺 ∈ Abel
Theorem	cnaddid 19912	The group identity element of complex number addition is zero. See also cnfld0 21428. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 26-Aug-2021.) (New usage is discouraged.)
⊢ 𝐺 = {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩}    ⇒   ⊢ (0g‘𝐺) = 0
Theorem	cnaddinv 19913	Value of the group inverse of complex number addition. See also cnfldneg 21431. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 26-Aug-2021.) (New usage is discouraged.)
⊢ 𝐺 = {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩}    ⇒   ⊢ (𝐴 ∈ ℂ → ((invg‘𝐺)‘𝐴) = -𝐴)
Theorem	zaddablx 19914	The integers are an Abelian group under addition. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. Use zsubrg 21461 instead. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.)
⊢ 𝐺 = {⟨1, ℤ⟩, ⟨2, + ⟩}    ⇒   ⊢ 𝐺 ∈ Abel
Theorem	frgpnabllem1 19915*	Lemma for frgpnabl 19917. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 25-Apr-2024.)
⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑈 = (varFGrp‘𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ ∈ (𝐷 ∩ ((𝑈‘𝐴) + (𝑈‘𝐵))))
Theorem	frgpnabllem2 19916*	Lemma for frgpnabl 19917. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 25-Apr-2024.)
⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑈 = (varFGrp‘𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐼)    &   ⊢ (𝜑 → ((𝑈‘𝐴) + (𝑈‘𝐵)) = ((𝑈‘𝐵) + (𝑈‘𝐴)))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	frgpnabl 19917	The free group on two or more generators is not abelian. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐺 = (freeGrp‘𝐼)    ⇒   ⊢ (1o ≺ 𝐼 → ¬ 𝐺 ∈ Abel)
Theorem	imasabl 19918*	The image structure of an abelian group is an abelian group (imasgrp 19096 analog). (Contributed by AV, 22-Feb-2025.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))    &   ⊢ (𝜑 → 𝑅 ∈ Abel)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝜑 → (𝑈 ∈ Abel ∧ (𝐹‘ 0 ) = (0g‘𝑈)))
10.2.14.2  Cyclic groups
Syntax	ccyg 19919	Cyclic group.
class CycGrp
Definition	df-cyg 19920*	Define a cyclic group, which is a group with an element 𝑥, called the generator of the group, such that all elements in the group are multiples of 𝑥. A generator is usually not unique. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ CycGrp = {𝑔 ∈ Grp ∣ ∃𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥)) = (Base‘𝑔)}
Theorem	iscyg 19921*	Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝐺 ∈ CycGrp ↔ (𝐺 ∈ Grp ∧ ∃𝑥 ∈ 𝐵 ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵))
Theorem	iscyggen 19922*	The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵}    ⇒   ⊢ (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) = 𝐵))
Theorem	iscyggen2 19923*	The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵}    ⇒   ⊢ (𝐺 ∈ Grp → (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑋))))
Theorem	iscyg2 19924*	A cyclic group is a group which contains a generator. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵}    ⇒   ⊢ (𝐺 ∈ CycGrp ↔ (𝐺 ∈ Grp ∧ 𝐸 ≠ ∅))
Theorem	cyggeninv 19925*	The inverse of a cyclic generator is a generator. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵}    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) → (𝑁‘𝑋) ∈ 𝐸)
Theorem	cyggenod 19926*	An element is the generator of a finite group iff the order of the generator equals the order of the group. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵}    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) → (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ (𝑂‘𝑋) = (♯‘𝐵))))
Theorem	cyggenod2 19927*	In an infinite cyclic group, the generator must have infinite order, but this property no longer characterizes the generators. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵}    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) → (𝑂‘𝑋) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))
Theorem	iscyg3 19928*	Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝐺 ∈ CycGrp ↔ (𝐺 ∈ Grp ∧ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑥)))
Theorem	iscygd 19929*	Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑋))    ⇒   ⊢ (𝜑 → 𝐺 ∈ CycGrp)
Theorem	iscygodd 19930	Show that a group with an element the same order as the group is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑂‘𝑋) = (♯‘𝐵))    ⇒   ⊢ (𝜑 → 𝐺 ∈ CycGrp)
Theorem	cycsubmcmn 19931*	The set of nonnegative integer powers of an element 𝐴 of a monoid forms a commutative monoid. (Contributed by AV, 20-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ ℕ0 ↦ (𝑥 · 𝐴))    &   ⊢ 𝐶 = ran 𝐹    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → (𝐺 ↾s 𝐶) ∈ CMnd)
Theorem	cyggrp 19932	A cyclic group is a group. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Grp)
Theorem	cygabl 19933	A cyclic group is abelian. (Contributed by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 20-Jan-2024.)
⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Abel)
Theorem	cygctb 19934	A cyclic group is countable. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ CycGrp → 𝐵 ≼ ω)
Theorem	0cyg 19935	The trivial group is cyclic. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1o) → 𝐺 ∈ CycGrp)
Theorem	prmcyg 19936	A group with prime order is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ ℙ) → 𝐺 ∈ CycGrp)
Theorem	lt6abl 19937	A group with fewer than 6 elements is abelian. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐺 ∈ Abel)
Theorem	ghmcyg 19938	The image of a cyclic group under a surjective group homomorphism is cyclic. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐶 = (Base‘𝐻)    ⇒   ⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝐹:𝐵–onto→𝐶) → (𝐺 ∈ CycGrp → 𝐻 ∈ CycGrp))
Theorem	cyggex2 19939	The exponent of a cyclic group is 0 if the group is infinite, otherwise it equals the order of the group. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    ⇒   ⊢ (𝐺 ∈ CycGrp → 𝐸 = if(𝐵 ∈ Fin, (♯‘𝐵), 0))
Theorem	cyggex 19940	The exponent of a finite cyclic group is the order of the group. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ CycGrp ∧ 𝐵 ∈ Fin) → 𝐸 = (♯‘𝐵))
Theorem	cyggexb 19941	A finite abelian group is cyclic iff the exponent equals the order of the group. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ 𝐵 ∈ Fin) → (𝐺 ∈ CycGrp ↔ 𝐸 = (♯‘𝐵)))
Theorem	giccyg 19942	Cyclicity is a group property, i.e. it is preserved under isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ (𝐺 ≃𝑔 𝐻 → (𝐺 ∈ CycGrp → 𝐻 ∈ CycGrp))
Theorem	cycsubgcyg 19943*	The cyclic subgroup generated by 𝐴 is a cyclic group. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝑆 = ran (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐺 ↾s 𝑆) ∈ CycGrp)
Theorem	cycsubgcyg2 19944	The cyclic subgroup generated by 𝐴 is a cyclic group. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵) → (𝐺 ↾s (𝐾‘{𝐴})) ∈ CycGrp)
10.2.14.3  Group sum operation
Theorem	gsumval3a 19945*	Value of the group sum operation over an index set with finite support. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by AV, 29-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ (𝜑 → 𝑊 ∈ Fin)    &   ⊢ (𝜑 → 𝑊 ≠ ∅)    &   ⊢ 𝑊 = (𝐹 supp 0 )    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ran ...)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))
Theorem	gsumval3eu 19946*	The group sum as defined in gsumval3a 19945 is uniquely defined. (Contributed by Mario Carneiro, 8-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ (𝜑 → 𝑊 ∈ Fin)    &   ⊢ (𝜑 → 𝑊 ≠ ∅)    &   ⊢ (𝜑 → 𝑊 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ∃!𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))
Theorem	gsumval3lem1 19947*	Lemma 1 for gsumval3 19949. (Contributed by AV, 31-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴)    &   ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻)    &   ⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 )    ⇒   ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))
Theorem	gsumval3lem2 19948*	Lemma 2 for gsumval3 19949. (Contributed by AV, 31-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴)    &   ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻)    &   ⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 )    ⇒   ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)))
Theorem	gsumval3 19949	Value of the group sum operation over an arbitrary finite set. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 31-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴)    &   ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻)    &   ⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))
Theorem	gsumcllem 19950*	Lemma for gsumcl 19957 and related theorems. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 31-May-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊)    ⇒   ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑘 ∈ 𝐴 ↦ 𝑍))
Theorem	gsumzres 19951	Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 31-May-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝑊)) = (𝐺 Σg 𝐹))
Theorem	gsumzcl2 19952	Closure of a finite group sum. This theorem has a weaker hypothesis than gsumzcl 19953, because it is not required that 𝐹 is a function (actually, the hypothesis always holds for any proper class 𝐹). (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 1-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ (𝜑 → (𝐹 supp 0 ) ∈ Fin)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵)
Theorem	gsumzcl 19953	Closure of a finite group sum. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 1-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵)
Theorem	gsumzf1o 19954	Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 2-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ (𝜑 → 𝐻:𝐶–1-1-onto→𝐴)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻)))
Theorem	gsumres 19955	Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝑊)) = (𝐺 Σg 𝐹))
Theorem	gsumcl2 19956	Closure of a finite group sum. This theorem has a weaker hypothesis than gsumcl 19957, because it is not required that 𝐹 is a function (actually, the hypothesis always holds for any proper class 𝐹). (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 supp 0 ) ∈ Fin)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵)
Theorem	gsumcl 19957	Closure of a finite group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵)
Theorem	gsumf1o 19958	Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ (𝜑 → 𝐻:𝐶–1-1-onto→𝐴)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻)))
Theorem	gsumreidx 19959	Re-index a finite group sum using a bijection. Corresponds to the first equation in [Lang] p. 5 with 𝑀 = 1. (Contributed by AV, 26-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    &   ⊢ (𝜑 → 𝐻:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻)))
Theorem	gsumzsubmcl 19960	Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝑆)
Theorem	gsumsubmcl 19961	Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝑆)
Theorem	gsumsubgcl 19962	Closure of a group sum in a subgroup. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 3-Jun-2019.)
⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝑆)
Theorem	gsumzaddlem 19963*	The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ (𝜑 → 𝐻 finSupp 0 )    &   ⊢ 𝑊 = ((𝐹 ∪ 𝐻) supp 0 )    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻))    &   ⊢ (𝜑 → ran (𝐹 ∘f + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘f + 𝐻)))    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
Theorem	gsumzadd 19964	The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ (𝜑 → 𝐻 finSupp 0 )    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   ⊢ (𝜑 → 𝑆 ⊆ (𝑍‘𝑆))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐻:𝐴⟶𝑆)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
Theorem	gsumadd 19965	The sum of two group sums. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ (𝜑 → 𝐻 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
Theorem	gsummptfsadd 19966*	The sum of two group sums expressed as mappings. (Contributed by AV, 4-Apr-2019.) (Revised by AV, 9-Jul-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶))    &   ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐴 ↦ 𝐷))    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ (𝜑 → 𝐻 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ (𝐶 + 𝐷))) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
Theorem	gsummptfidmadd 19967*	The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ 𝐷)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ (𝐶 + 𝐷))) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
Theorem	gsummptfidmadd2 19968*	The sum of two group sums expressed as mappings with finite domain, using a function operation. (Contributed by AV, 23-Jul-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ 𝐷)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
Theorem	gsumzsplit 19969	Split a group sum into two parts. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷))    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹 ↾ 𝐶)) + (𝐺 Σg (𝐹 ↾ 𝐷))))
Theorem	gsumsplit 19970	Split a group sum into two parts. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 5-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷))    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹 ↾ 𝐶)) + (𝐺 Σg (𝐹 ↾ 𝐷))))
Theorem	gsumsplit2 19971*	Split a group sum into two parts. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 5-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 )    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷))    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)) + (𝐺 Σg (𝑘 ∈ 𝐷 ↦ 𝑋))))
Theorem	gsummptfidmsplit 19972*	Split a group sum expressed as mapping with a finite domain into two parts. (Contributed by AV, 23-Jul-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷))    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑌)) = ((𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑌)) + (𝐺 Σg (𝑘 ∈ 𝐷 ↦ 𝑌))))
Theorem	gsummptfidmsplitres 19973*	Split a group sum expressed as mapping with a finite domain into two parts using restrictions. (Contributed by AV, 23-Jul-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷))    &   ⊢ 𝐹 = (𝑘 ∈ 𝐴 ↦ 𝑌)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹 ↾ 𝐶)) + (𝐺 Σg (𝐹 ↾ 𝐷))))
Theorem	gsummptfzsplit 19974*	Split a group sum expressed as mapping with a finite set of sequential integers as domain into two parts, extracting a singleton from the right. (Contributed by AV, 25-Oct-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ 𝑌)) = ((𝐺 Σg (𝑘 ∈ (0...𝑁) ↦ 𝑌)) + (𝐺 Σg (𝑘 ∈ {(𝑁 + 1)} ↦ 𝑌))))
Theorem	gsummptfzsplitl 19975*	Split a group sum expressed as mapping with a finite set of sequential integers as domain into two parts, , extracting a singleton from the left. (Contributed by AV, 7-Nov-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (0...𝑁) ↦ 𝑌)) = ((𝐺 Σg (𝑘 ∈ (1...𝑁) ↦ 𝑌)) + (𝐺 Σg (𝑘 ∈ {0} ↦ 𝑌))))
Theorem	gsumconst 19976*	Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((♯‘𝐴) · 𝑋))
Theorem	gsumconstf 19977*	Sum of a constant series. (Contributed by Thierry Arnoux, 5-Jul-2017.)
⊢ Ⅎ𝑘𝑋    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((♯‘𝐴) · 𝑋))
Theorem	gsummptshft 19978*	Index shift of a finite group sum over a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ 𝐵)    &   ⊢ (𝑗 = (𝑘 − 𝐾) → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ (𝑀...𝑁) ↦ 𝐴)) = (𝐺 Σg (𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ 𝐶)))
Theorem	gsumzmhm 19979	Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 6-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐻 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐺 MndHom 𝐻))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐻 Σg (𝐾 ∘ 𝐹)) = (𝐾‘(𝐺 Σg 𝐹)))
Theorem	gsummhm 19980	Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 6-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐻 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐺 MndHom 𝐻))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐻 Σg (𝐾 ∘ 𝐹)) = (𝐾‘(𝐺 Σg 𝐹)))
Theorem	gsummhm2 19981*	Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015.) (Revised by AV, 6-Jun-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐻 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ (𝐺 MndHom 𝐻))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 )    &   ⊢ (𝑥 = 𝑋 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) → 𝐶 = 𝐸)    ⇒   ⊢ (𝜑 → (𝐻 Σg (𝑘 ∈ 𝐴 ↦ 𝐷)) = 𝐸)
Theorem	gsummptmhm 19982*	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 19983*	Lemma for gsummulg 19984 and gsummulgz 19985. (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 19984*	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 19985*	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 19986	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 19987	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 19988	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 19989*	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 19990	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 19991*	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 19992*	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 19993*	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 19994*	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 19995*	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 19996*	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 19997*	Group sum of a pair. (Contributed by AV, 6-Dec-2018.) (Proof shortened by AV, 28-Jul-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐶)    &   ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐷)    ⇒   ⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → (𝐺 Σg (𝑘 ∈ {𝑀, 𝑁} ↦ 𝐴)) = (𝐶 + 𝐷))
Theorem	gsumzunsnd 19998*	Append an element to a finite group sum, more general version of gsumunsnd 20000. (Contributed by AV, 7-Oct-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝐹 = (𝑘 ∈ (𝐴 ∪ {𝑀}) ↦ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑀 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) + 𝑌))
Theorem	gsumunsnfd 19999*	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 20000*	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 (𝑘 ∈ 𝐴 ↦ 𝑋)) + 𝑌))