Definition df-gsum 16103

Description: Define the group sum for the structure G of a finite sequence of elements whose values are defined by the expression B and whose set of indices is A. It may be viewed as a product (if G is a multiplication), a sum (if G is an addition) or whatever. The variable k is normally a free variable in B ( i.e. B can be thought of as B ( k )). 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. ( B ( 1 ) + B ( 2 ) ) + B ( 3 ) etc.

3. If A is a finite set (or is nonzero for finitely many indices) and G is a commutative monoid, then the sum adds up these elements in some order, which is then uniquely defined.

4. If A is an infinite set and G is a Hausdorff topological group, then there is a meaningful sum, but gsum_g cannot handle this case. See df-tsms 21930. Remark: this definition is required here because the symbol gsum_g is already used in df-prds 16108 and df-imas 16168. The related theorems are provided later, see gsumvalx 17270. (Contributed by FL, 5-Sep-2010.) (Revised by FL, 17-Oct-2011.) (Revised by Mario Carneiro, 7-Dec-2014.)

Assertion

Ref

Expression

df-gsum

|- gsumg = ( w e. _V , f e. _V |-> [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran f C_ o , ( 0g ` w ) , if ( dom f e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) , ( iota x E. g [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) ) ) ) ) )

Distinct variable group:   f, g, m, n, o, w, x, y

Detailed syntax breakdown of Definition df-gsum

Step	Hyp	Ref	Expression
1		cgsu 16101	. 2 class gsumg
2		vw	. . 3 setvar w
3		vf	. . 3 setvar f
4		cvv 3200	. . 3 class _V
5		vo	. . . 4 setvar o
6		vx	. . . . . . . . . 10 setvar x
7	6	cv 1482	. . . . . . . . 9 class x
8		vy	. . . . . . . . . 10 setvar y
9	8	cv 1482	. . . . . . . . 9 class y
10	2	cv 1482	. . . . . . . . . 10 class w
11		cplusg 15941	. . . . . . . . . 10 class +g
12	10, 11	cfv 5888	. . . . . . . . 9 class ( +g ` w )
13	7, 9, 12	co 6650	. . . . . . . 8 class ( x ( +g ` w ) y )
14	13, 9	wceq 1483	. . . . . . 7 wff ( x ( +g ` w ) y ) = y
15	9, 7, 12	co 6650	. . . . . . . 8 class ( y ( +g ` w ) x )
16	15, 9	wceq 1483	. . . . . . 7 wff ( y ( +g ` w ) x ) = y
17	14, 16	wa 384	. . . . . 6 wff ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y )
18		cbs 15857	. . . . . . 7 class Base
19	10, 18	cfv 5888	. . . . . 6 class ( Base ` w )
20	17, 8, 19	wral 2912	. . . . 5 wff A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y )
21	20, 6, 19	crab 2916	. . . 4 class { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) }
22	3	cv 1482	. . . . . . 7 class f
23	22	crn 5115	. . . . . 6 class ran f
24	5	cv 1482	. . . . . 6 class o
25	23, 24	wss 3574	. . . . 5 wff ran f C_ o
26		c0g 16100	. . . . . 6 class 0g
27	10, 26	cfv 5888	. . . . 5 class ( 0g ` w )
28	22	cdm 5114	. . . . . . 7 class dom f
29		cfz 12326	. . . . . . . 8 class ...
30	29	crn 5115	. . . . . . 7 class ran ...
31	28, 30	wcel 1990	. . . . . 6 wff dom f e. ran ...
32		vm	. . . . . . . . . . . . 13 setvar m
33	32	cv 1482	. . . . . . . . . . . 12 class m
34		vn	. . . . . . . . . . . . 13 setvar n
35	34	cv 1482	. . . . . . . . . . . 12 class n
36	33, 35, 29	co 6650	. . . . . . . . . . 11 class ( m ... n )
37	28, 36	wceq 1483	. . . . . . . . . 10 wff dom f = ( m ... n )
38	12, 22, 33	cseq 12801	. . . . . . . . . . . 12 class seq m ( ( +g ` w ) , f )
39	35, 38	cfv 5888	. . . . . . . . . . 11 class ( seq m ( ( +g ` w ) , f ) ` n )
40	7, 39	wceq 1483	. . . . . . . . . 10 wff x = ( seq m ( ( +g ` w ) , f ) ` n )
41	37, 40	wa 384	. . . . . . . . 9 wff ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) )
42		cuz 11687	. . . . . . . . . 10 class ZZ>=
43	33, 42	cfv 5888	. . . . . . . . 9 class ( ZZ>= ` m )
44	41, 34, 43	wrex 2913	. . . . . . . 8 wff E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) )
45	44, 32	wex 1704	. . . . . . 7 wff E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) )
46	45, 6	cio 5849	. . . . . 6 class ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) )
47		c1 9937	. . . . . . . . . . . 12 class 1
48		chash 13117	. . . . . . . . . . . . 13 class #
49	9, 48	cfv 5888	. . . . . . . . . . . 12 class ( # ` y )
50	47, 49, 29	co 6650	. . . . . . . . . . 11 class ( 1 ... ( # ` y ) )
51		vg	. . . . . . . . . . . 12 setvar g
52	51	cv 1482	. . . . . . . . . . 11 class g
53	50, 9, 52	wf1o 5887	. . . . . . . . . 10 wff g : ( 1 ... ( # ` y ) ) -1-1-onto-> y
54	22, 52	ccom 5118	. . . . . . . . . . . . 13 class ( f o. g )
55	12, 54, 47	cseq 12801	. . . . . . . . . . . 12 class seq 1 ( ( +g ` w ) , ( f o. g ) )
56	49, 55	cfv 5888	. . . . . . . . . . 11 class ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) )
57	7, 56	wceq 1483	. . . . . . . . . 10 wff x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) )
58	53, 57	wa 384	. . . . . . . . 9 wff ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) )
59	22	ccnv 5113	. . . . . . . . . 10 class `' f
60	4, 24	cdif 3571	. . . . . . . . . 10 class ( _V \ o )
61	59, 60	cima 5117	. . . . . . . . 9 class ( `' f " ( _V \ o ) )
62	58, 8, 61	wsbc 3435	. . . . . . . 8 wff [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) )
63	62, 51	wex 1704	. . . . . . 7 wff E. g [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) )
64	63, 6	cio 5849	. . . . . 6 class ( iota x E. g [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) ) )
65	31, 46, 64	cif 4086	. . . . 5 class if ( dom f e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) , ( iota x E. g [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) ) ) )
66	25, 27, 65	cif 4086	. . . 4 class if ( ran f C_ o , ( 0g ` w ) , if ( dom f e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) , ( iota x E. g [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) ) ) ) )
67	5, 21, 66	csb 3533	. . 3 class [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran f C_ o , ( 0g ` w ) , if ( dom f e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) , ( iota x E. g [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) ) ) ) )
68	2, 3, 4, 4, 67	cmpt2 6652	. 2 class ( w e. _V , f e. _V |-> [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran f C_ o , ( 0g ` w ) , if ( dom f e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) , ( iota x E. g [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) ) ) ) ) )
69	1, 68	wceq 1483	1 wff gsumg = ( w e. _V , f e. _V |-> [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran f C_ o , ( 0g ` w ) , if ( dom f e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) , ( iota x E. g [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) ) ) ) ) )

This definition is referenced by:  gsumvalx  17270  gsum0  17278