Description: Define the group sum (also called "iterated 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 any other operation. 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. See gsum0 .
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. See gsumval2 and gsumnunsn .
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. See gsumval3 .
4. If A is an infinite set and G is a Hausdorff topological group, then there is a meaningful sum, but gsum cannot handle this case. See df-tsms .
Remark: this definition is required here because the symbol gsum is already used in df-prds and df-imas . The related theorems are provided later, see gsumvalx . (Contributed by FL, 5-Sep-2010) (Revised by FL, 17-Oct-2011) (Revised by Mario Carneiro, 7-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | df-gsum | |- gsum = ( 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 ) ) ) ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cgsu | |- gsum |
|
1 | vw | |- w |
|
2 | cvv | |- _V |
|
3 | vf | |- f |
|
4 | vx | |- x |
|
5 | cbs | |- Base |
|
6 | 1 | cv | |- w |
7 | 6 5 | cfv | |- ( Base ` w ) |
8 | vy | |- y |
|
9 | 4 | cv | |- x |
10 | cplusg | |- +g |
|
11 | 6 10 | cfv | |- ( +g ` w ) |
12 | 8 | cv | |- y |
13 | 9 12 11 | co | |- ( x ( +g ` w ) y ) |
14 | 13 12 | wceq | |- ( x ( +g ` w ) y ) = y |
15 | 12 9 11 | co | |- ( y ( +g ` w ) x ) |
16 | 15 12 | wceq | |- ( y ( +g ` w ) x ) = y |
17 | 14 16 | wa | |- ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) |
18 | 17 8 7 | wral | |- A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) |
19 | 18 4 7 | crab | |- { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } |
20 | vo | |- o |
|
21 | 3 | cv | |- f |
22 | 21 | crn | |- ran f |
23 | 20 | cv | |- o |
24 | 22 23 | wss | |- ran f C_ o |
25 | c0g | |- 0g |
|
26 | 6 25 | cfv | |- ( 0g ` w ) |
27 | 21 | cdm | |- dom f |
28 | cfz | |- ... |
|
29 | 28 | crn | |- ran ... |
30 | 27 29 | wcel | |- dom f e. ran ... |
31 | vm | |- m |
|
32 | vn | |- n |
|
33 | cuz | |- ZZ>= |
|
34 | 31 | cv | |- m |
35 | 34 33 | cfv | |- ( ZZ>= ` m ) |
36 | 32 | cv | |- n |
37 | 34 36 28 | co | |- ( m ... n ) |
38 | 27 37 | wceq | |- dom f = ( m ... n ) |
39 | 11 21 34 | cseq | |- seq m ( ( +g ` w ) , f ) |
40 | 36 39 | cfv | |- ( seq m ( ( +g ` w ) , f ) ` n ) |
41 | 9 40 | wceq | |- x = ( seq m ( ( +g ` w ) , f ) ` n ) |
42 | 38 41 | wa | |- ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) |
43 | 42 32 35 | wrex | |- E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) |
44 | 43 31 | wex | |- E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) |
45 | 44 4 | cio | |- ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) |
46 | vg | |- g |
|
47 | 21 | ccnv | |- `' f |
48 | 2 23 | cdif | |- ( _V \ o ) |
49 | 47 48 | cima | |- ( `' f " ( _V \ o ) ) |
50 | 46 | cv | |- g |
51 | c1 | |- 1 |
|
52 | chash | |- # |
|
53 | 12 52 | cfv | |- ( # ` y ) |
54 | 51 53 28 | co | |- ( 1 ... ( # ` y ) ) |
55 | 54 12 50 | wf1o | |- g : ( 1 ... ( # ` y ) ) -1-1-onto-> y |
56 | 21 50 | ccom | |- ( f o. g ) |
57 | 11 56 51 | cseq | |- seq 1 ( ( +g ` w ) , ( f o. g ) ) |
58 | 53 57 | cfv | |- ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) |
59 | 9 58 | wceq | |- x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) |
60 | 55 59 | wa | |- ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) ) |
61 | 60 8 49 | wsbc | |- [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) ) |
62 | 61 46 | wex | |- E. g [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) ) |
63 | 62 4 | cio | |- ( iota x E. g [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) ) ) |
64 | 30 45 63 | cif | |- 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 ) ) ) ) ) |
65 | 24 26 64 | cif | |- 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 ) ) ) ) ) ) |
66 | 20 19 65 | csb | |- [_ { 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 ) ) ) ) ) ) |
67 | 1 3 2 2 66 | cmpo | |- ( 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 ) ) ) ) ) ) ) |
68 | 0 67 | wceq | |- gsum = ( 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 ) ) ) ) ) ) ) |