Metamath Proof Explorer


Definition df-gsum

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

Detailed syntax breakdown

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