MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-gsum Unicode version

Definition df-gsum 13400
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 three 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 non-zero 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  gsumg cannot handle this case. See df-tsms 17804. (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
StepHypRef Expression
1 cgsu 13396 . 2  class  gsumg
2 vw . . 3  set  w
3 vf . . 3  set  f
4 cvv 2790 . . 3  class  _V
5 vo . . . 4  set  o
6 vx . . . . . . . . . 10  set  x
76cv 1623 . . . . . . . . 9  class  x
8 vy . . . . . . . . . 10  set  y
98cv 1623 . . . . . . . . 9  class  y
102cv 1623 . . . . . . . . . 10  class  w
11 cplusg 13203 . . . . . . . . . 10  class  +g
1210, 11cfv 5222 . . . . . . . . 9  class  ( +g  `  w )
137, 9, 12co 5820 . . . . . . . 8  class  ( x ( +g  `  w
) y )
1413, 9wceq 1624 . . . . . . 7  wff  ( x ( +g  `  w
) y )  =  y
159, 7, 12co 5820 . . . . . . . 8  class  ( y ( +g  `  w
) x )
1615, 9wceq 1624 . . . . . . 7  wff  ( y ( +g  `  w
) x )  =  y
1714, 16wa 360 . . . . . 6  wff  ( ( x ( +g  `  w
) y )  =  y  /\  ( y ( +g  `  w
) x )  =  y )
18 cbs 13143 . . . . . . 7  class  Base
1910, 18cfv 5222 . . . . . 6  class  ( Base `  w )
2017, 8, 19wral 2545 . . . . 5  wff  A. y  e.  ( Base `  w
) ( ( x ( +g  `  w
) y )  =  y  /\  ( y ( +g  `  w
) x )  =  y )
2120, 6, 19crab 2549 . . . 4  class  { x  e.  ( Base `  w
)  |  A. y  e.  ( Base `  w
) ( ( x ( +g  `  w
) y )  =  y  /\  ( y ( +g  `  w
) x )  =  y ) }
223cv 1623 . . . . . . 7  class  f
2322crn 4690 . . . . . 6  class  ran  f
245cv 1623 . . . . . 6  class  o
2523, 24wss 3154 . . . . 5  wff  ran  f  C_  o
26 c0g 13395 . . . . . 6  class  0g
2710, 26cfv 5222 . . . . 5  class  ( 0g
`  w )
2822cdm 4689 . . . . . . 7  class  dom  f
29 cfz 10777 . . . . . . . 8  class  ...
3029crn 4690 . . . . . . 7  class  ran  ...
3128, 30wcel 1685 . . . . . 6  wff  dom  f  e.  ran  ...
32 vm . . . . . . . . . . . . 13  set  m
3332cv 1623 . . . . . . . . . . . 12  class  m
34 vn . . . . . . . . . . . . 13  set  n
3534cv 1623 . . . . . . . . . . . 12  class  n
3633, 35, 29co 5820 . . . . . . . . . . 11  class  ( m ... n )
3728, 36wceq 1624 . . . . . . . . . 10  wff  dom  f  =  ( m ... n )
3812, 22, 33cseq 11041 . . . . . . . . . . . 12  class  seq  m
( ( +g  `  w
) ,  f )
3935, 38cfv 5222 . . . . . . . . . . 11  class  (  seq  m ( ( +g  `  w ) ,  f ) `  n )
407, 39wceq 1624 . . . . . . . . . 10  wff  x  =  (  seq  m ( ( +g  `  w
) ,  f ) `
 n )
4137, 40wa 360 . . . . . . . . 9  wff  ( dom  f  =  ( m ... n )  /\  x  =  (  seq  m ( ( +g  `  w ) ,  f ) `  n ) )
42 cuz 10226 . . . . . . . . . 10  class  ZZ>=
4333, 42cfv 5222 . . . . . . . . 9  class  ( ZZ>= `  m )
4441, 34, 43wrex 2546 . . . . . . . 8  wff  E. n  e.  ( ZZ>= `  m )
( dom  f  =  ( m ... n
)  /\  x  =  (  seq  m ( ( +g  `  w ) ,  f ) `  n ) )
4544, 32wex 1529 . . . . . . 7  wff  E. m E. n  e.  ( ZZ>=
`  m ) ( dom  f  =  ( m ... n )  /\  x  =  (  seq  m ( ( +g  `  w ) ,  f ) `  n ) )
4645, 6cio 6251 . . . . . 6  class  ( iota
x E. m E. n  e.  ( ZZ>= `  m ) ( dom  f  =  ( m ... n )  /\  x  =  (  seq  m ( ( +g  `  w ) ,  f ) `  n ) ) )
47 c1 8734 . . . . . . . . . . . 12  class  1
48 chash 11332 . . . . . . . . . . . . 13  class  #
499, 48cfv 5222 . . . . . . . . . . . 12  class  ( # `  y )
5047, 49, 29co 5820 . . . . . . . . . . 11  class  ( 1 ... ( # `  y
) )
51 vg . . . . . . . . . . . 12  set  g
5251cv 1623 . . . . . . . . . . 11  class  g
5350, 9, 52wf1o 5221 . . . . . . . . . 10  wff  g : ( 1 ... ( # `
 y ) ) -1-1-onto-> y
5422, 52ccom 4693 . . . . . . . . . . . . 13  class  ( f  o.  g )
5512, 54, 47cseq 11041 . . . . . . . . . . . 12  class  seq  1
( ( +g  `  w
) ,  ( f  o.  g ) )
5649, 55cfv 5222 . . . . . . . . . . 11  class  (  seq  1 ( ( +g  `  w ) ,  ( f  o.  g ) ) `  ( # `  y ) )
577, 56wceq 1624 . . . . . . . . . 10  wff  x  =  (  seq  1 ( ( +g  `  w
) ,  ( f  o.  g ) ) `
 ( # `  y
) )
5853, 57wa 360 . . . . . . . . 9  wff  ( g : ( 1 ... ( # `  y
) ) -1-1-onto-> y  /\  x  =  (  seq  1
( ( +g  `  w
) ,  ( f  o.  g ) ) `
 ( # `  y
) ) )
5922ccnv 4688 . . . . . . . . . 10  class  `' f
604, 24cdif 3151 . . . . . . . . . 10  class  ( _V 
\  o )
6159, 60cima 4692 . . . . . . . . 9  class  ( `' f " ( _V 
\  o ) )
6258, 8, 61wsbc 2993 . . . . . . . 8  wff  [. ( `' f " ( _V  \  o ) )  /  y ]. (
g : ( 1 ... ( # `  y
) ) -1-1-onto-> y  /\  x  =  (  seq  1
( ( +g  `  w
) ,  ( f  o.  g ) ) `
 ( # `  y
) ) )
6362, 51wex 1529 . . . . . . 7  wff  E. g [. ( `' f "
( _V  \  o
) )  /  y ]. ( g : ( 1 ... ( # `  y ) ) -1-1-onto-> y  /\  x  =  (  seq  1 ( ( +g  `  w ) ,  ( f  o.  g ) ) `  ( # `  y ) ) )
6463, 6cio 6251 . . . . . 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
) ) ) )
6531, 46, 64cif 3567 . . . . 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
) ) ) ) )
6625, 27, 65cif 3567 . . . 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
) ) ) ) ) )
675, 21, 66csb 3083 . . 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
) ) ) ) ) )
682, 3, 4, 4, 67cmpt2 5822 . 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
) ) ) ) ) ) )
691, 68wceq 1624 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
) ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  gsumvalx  14446  gsum0  14452
  Copyright terms: Public domain W3C validator