Definition df-igsum 12870

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

Given G gsum_g F where F : A --> ( Base ` G ), the set of indices is A and the values are given by F 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 A and each demanding different properties of G.

1. If A = (/) and G has an identity element, then the sum equals this identity.

2. If A = ( M ... N ) and G is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e., ( ( F ` 1 ) + ( F ` 2 ) ) + ( F ` 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	|- gsumg = ( w e. _V , f e. _V |-> ( iota x ( ( dom f = (/) /\ x = ( 0g ` w ) ) \/ E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) ) )

Distinct variable group:   f, m, n, w, x

Detailed syntax breakdown of Definition df-igsum

Step	Hyp	Ref	Expression
1		cgsu 12868	. 2 class gsumg
2		vw	. . 3 setvar w
3		vf	. . 3 setvar f
4		cvv 2760	. . 3 class _V
5	3	cv 1363	. . . . . . . 8 class f
6	5	cdm 4659	. . . . . . 7 class dom f
7		c0 3446	. . . . . . 7 class (/)
8	6, 7	wceq 1364	. . . . . 6 wff dom f = (/)
9		vx	. . . . . . . 8 setvar x
10	9	cv 1363	. . . . . . 7 class x
11	2	cv 1363	. . . . . . . 8 class w
12		c0g 12867	. . . . . . . 8 class 0g
13	11, 12	cfv 5254	. . . . . . 7 class ( 0g ` w )
14	10, 13	wceq 1364	. . . . . 6 wff x = ( 0g ` w )
15	8, 14	wa 104	. . . . 5 wff ( dom f = (/) /\ x = ( 0g ` w ) )
16		vm	. . . . . . . . . . 11 setvar m
17	16	cv 1363	. . . . . . . . . 10 class m
18		vn	. . . . . . . . . . 11 setvar n
19	18	cv 1363	. . . . . . . . . 10 class n
20		cfz 10074	. . . . . . . . . 10 class ...
21	17, 19, 20	co 5918	. . . . . . . . 9 class ( m ... n )
22	6, 21	wceq 1364	. . . . . . . 8 wff dom f = ( m ... n )
23		cplusg 12695	. . . . . . . . . . . 12 class +g
24	11, 23	cfv 5254	. . . . . . . . . . 11 class ( +g ` w )
25	24, 5, 17	cseq 10518	. . . . . . . . . 10 class seq m ( ( +g ` w ) , f )
26	19, 25	cfv 5254	. . . . . . . . 9 class ( seq m ( ( +g ` w ) , f ) ` n )
27	10, 26	wceq 1364	. . . . . . . 8 wff x = ( seq m ( ( +g ` w ) , f ) ` n )
28	22, 27	wa 104	. . . . . . 7 wff ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) )
29		cuz 9592	. . . . . . . 8 class ZZ>=
30	17, 29	cfv 5254	. . . . . . 7 class ( ZZ>= ` m )
31	28, 18, 30	wrex 2473	. . . . . 6 wff E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) )
32	31, 16	wex 1503	. . . . 5 wff E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) )
33	15, 32	wo 709	. . . 4 wff ( ( dom f = (/) /\ x = ( 0g ` w ) ) \/ E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) )
34	33, 9	cio 5213	. . 3 class ( iota x ( ( dom f = (/) /\ x = ( 0g ` w ) ) \/ E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) )
35	2, 3, 4, 4, 34	cmpo 5920	. 2 class ( w e. _V , f e. _V |-> ( iota x ( ( dom f = (/) /\ x = ( 0g ` w ) ) \/ E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) ) )
36	1, 35	wceq 1364	1 wff gsumg = ( w e. _V , f e. _V |-> ( iota x ( ( dom f = (/) /\ x = ( 0g ` w ) ) \/ E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) ) )

This definition is referenced by:  fngsum  12971  igsumvalx  12972