Definition df-igsum 12930

Description: Define a finite group sum (also called "iterated sum") of a structure.

Given 𝐺 Σ_g 𝐹 where 𝐹:𝐴⟶(Base‘𝐺), the set of indices is 𝐴 and the values are given by 𝐹 at each index. A group sum over a multiplicative group may be viewed as a product. The definition is meaningful in different contexts, depending on the size of the index set 𝐴 and each demanding different properties of 𝐺.

1. If 𝐴 = ∅ and 𝐺 has an identity element, then the sum equals this identity.

2. If 𝐴 = (𝑀...𝑁) and 𝐺 is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e., ((𝐹‘1) + (𝐹‘2)) + (𝐹‘3), etc.

3. This definition does not handle other cases.

(Contributed by FL, 5-Sep-2010.) (Revised by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 27-Jun-2025.)

Assertion

Ref	Expression
df-igsum	⊢ Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ (℩𝑥((dom 𝑓 = ∅ ∧ 𝑥 = (0g‘𝑤)) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)))))

Distinct variable group:   𝑓,𝑚,𝑛,𝑤,𝑥

Detailed syntax breakdown of Definition df-igsum

Step	Hyp	Ref	Expression
1		cgsu 12928	. 2 class Σg
2		vw	. . 3 setvar 𝑤
3		vf	. . 3 setvar 𝑓
4		cvv 2763	. . 3 class V
5	3	cv 1363	. . . . . . . 8 class 𝑓
6	5	cdm 4663	. . . . . . 7 class dom 𝑓
7		c0 3450	. . . . . . 7 class ∅
8	6, 7	wceq 1364	. . . . . 6 wff dom 𝑓 = ∅
9		vx	. . . . . . . 8 setvar 𝑥
10	9	cv 1363	. . . . . . 7 class 𝑥
11	2	cv 1363	. . . . . . . 8 class 𝑤
12		c0g 12927	. . . . . . . 8 class 0g
13	11, 12	cfv 5258	. . . . . . 7 class (0g‘𝑤)
14	10, 13	wceq 1364	. . . . . 6 wff 𝑥 = (0g‘𝑤)
15	8, 14	wa 104	. . . . 5 wff (dom 𝑓 = ∅ ∧ 𝑥 = (0g‘𝑤))
16		vm	. . . . . . . . . . 11 setvar 𝑚
17	16	cv 1363	. . . . . . . . . 10 class 𝑚
18		vn	. . . . . . . . . . 11 setvar 𝑛
19	18	cv 1363	. . . . . . . . . 10 class 𝑛
20		cfz 10083	. . . . . . . . . 10 class ...
21	17, 19, 20	co 5922	. . . . . . . . 9 class (𝑚...𝑛)
22	6, 21	wceq 1364	. . . . . . . 8 wff dom 𝑓 = (𝑚...𝑛)
23		cplusg 12755	. . . . . . . . . . . 12 class +g
24	11, 23	cfv 5258	. . . . . . . . . . 11 class (+g‘𝑤)
25	24, 5, 17	cseq 10539	. . . . . . . . . 10 class seq𝑚((+g‘𝑤), 𝑓)
26	19, 25	cfv 5258	. . . . . . . . 9 class (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)
27	10, 26	wceq 1364	. . . . . . . 8 wff 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)
28	22, 27	wa 104	. . . . . . 7 wff (dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))
29		cuz 9601	. . . . . . . 8 class ℤ≥
30	17, 29	cfv 5258	. . . . . . 7 class (ℤ≥‘𝑚)
31	28, 18, 30	wrex 2476	. . . . . 6 wff ∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))
32	31, 16	wex 1506	. . . . 5 wff ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))
33	15, 32	wo 709	. . . 4 wff ((dom 𝑓 = ∅ ∧ 𝑥 = (0g‘𝑤)) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)))
34	33, 9	cio 5217	. . 3 class (℩𝑥((dom 𝑓 = ∅ ∧ 𝑥 = (0g‘𝑤)) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))))
35	2, 3, 4, 4, 34	cmpo 5924	. 2 class (𝑤 ∈ V, 𝑓 ∈ V ↦ (℩𝑥((dom 𝑓 = ∅ ∧ 𝑥 = (0g‘𝑤)) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)))))
36	1, 35	wceq 1364	1 wff Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ (℩𝑥((dom 𝑓 = ∅ ∧ 𝑥 = (0g‘𝑤)) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)))))

This definition is referenced by:  fngsum  13031  igsumvalx  13032