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 ) ) ) ) ) ) ) |