ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-gsum Unicode version

Definition df-gsum 12382
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 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.

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  gsumg cannot handle this case. (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 12380 . 2  class  gsumg
2 vw . . 3  setvar  w
3 vf . . 3  setvar  f
4 cvv 2712 . . 3  class  _V
5 vo . . . 4  setvar  o
6 vx . . . . . . . . . 10  setvar  x
76cv 1334 . . . . . . . . 9  class  x
8 vy . . . . . . . . . 10  setvar  y
98cv 1334 . . . . . . . . 9  class  y
102cv 1334 . . . . . . . . . 10  class  w
11 cplusg 12263 . . . . . . . . . 10  class  +g
1210, 11cfv 5170 . . . . . . . . 9  class  ( +g  `  w )
137, 9, 12co 5824 . . . . . . . 8  class  ( x ( +g  `  w
) y )
1413, 9wceq 1335 . . . . . . 7  wff  ( x ( +g  `  w
) y )  =  y
159, 7, 12co 5824 . . . . . . . 8  class  ( y ( +g  `  w
) x )
1615, 9wceq 1335 . . . . . . 7  wff  ( y ( +g  `  w
) x )  =  y
1714, 16wa 103 . . . . . 6  wff  ( ( x ( +g  `  w
) y )  =  y  /\  ( y ( +g  `  w
) x )  =  y )
18 cbs 12201 . . . . . . 7  class  Base
1910, 18cfv 5170 . . . . . 6  class  ( Base `  w )
2017, 8, 19wral 2435 . . . . 5  wff  A. y  e.  ( Base `  w
) ( ( x ( +g  `  w
) y )  =  y  /\  ( y ( +g  `  w
) x )  =  y )
2120, 6, 19crab 2439 . . . 4  class  { x  e.  ( Base `  w
)  |  A. y  e.  ( Base `  w
) ( ( x ( +g  `  w
) y )  =  y  /\  ( y ( +g  `  w
) x )  =  y ) }
223cv 1334 . . . . . . 7  class  f
2322crn 4587 . . . . . 6  class  ran  f
245cv 1334 . . . . . 6  class  o
2523, 24wss 3102 . . . . 5  wff  ran  f  C_  o
26 c0g 12379 . . . . . 6  class  0g
2710, 26cfv 5170 . . . . 5  class  ( 0g
`  w )
2822cdm 4586 . . . . . . 7  class  dom  f
29 cfz 9912 . . . . . . . 8  class  ...
3029crn 4587 . . . . . . 7  class  ran  ...
3128, 30wcel 2128 . . . . . 6  wff  dom  f  e.  ran  ...
32 vm . . . . . . . . . . . . 13  setvar  m
3332cv 1334 . . . . . . . . . . . 12  class  m
34 vn . . . . . . . . . . . . 13  setvar  n
3534cv 1334 . . . . . . . . . . . 12  class  n
3633, 35, 29co 5824 . . . . . . . . . . 11  class  ( m ... n )
3728, 36wceq 1335 . . . . . . . . . 10  wff  dom  f  =  ( m ... n )
3812, 22, 33cseq 10344 . . . . . . . . . . . 12  class  seq m
( ( +g  `  w
) ,  f )
3935, 38cfv 5170 . . . . . . . . . . 11  class  (  seq m ( ( +g  `  w ) ,  f ) `  n )
407, 39wceq 1335 . . . . . . . . . 10  wff  x  =  (  seq m ( ( +g  `  w
) ,  f ) `
 n )
4137, 40wa 103 . . . . . . . . 9  wff  ( dom  f  =  ( m ... n )  /\  x  =  (  seq m ( ( +g  `  w ) ,  f ) `  n ) )
42 cuz 9439 . . . . . . . . . 10  class  ZZ>=
4333, 42cfv 5170 . . . . . . . . 9  class  ( ZZ>= `  m )
4441, 34, 43wrex 2436 . . . . . . . 8  wff  E. n  e.  ( ZZ>= `  m )
( dom  f  =  ( m ... n
)  /\  x  =  (  seq m ( ( +g  `  w ) ,  f ) `  n ) )
4544, 32wex 1472 . . . . . . 7  wff  E. m E. n  e.  ( ZZ>=
`  m ) ( dom  f  =  ( m ... n )  /\  x  =  (  seq m ( ( +g  `  w ) ,  f ) `  n ) )
4645, 6cio 5133 . . . . . 6  class  ( iota
x E. m E. n  e.  ( ZZ>= `  m ) ( dom  f  =  ( m ... n )  /\  x  =  (  seq m ( ( +g  `  w ) ,  f ) `  n ) ) )
47 c1 7733 . . . . . . . . . . . 12  class  1
48 chash 10649 . . . . . . . . . . . . 13  class
499, 48cfv 5170 . . . . . . . . . . . 12  class  ( `  y
)
5047, 49, 29co 5824 . . . . . . . . . . 11  class  ( 1 ... ( `  y
) )
51 vg . . . . . . . . . . . 12  setvar  g
5251cv 1334 . . . . . . . . . . 11  class  g
5350, 9, 52wf1o 5169 . . . . . . . . . 10  wff  g : ( 1 ... ( `  y ) ) -1-1-onto-> y
5422, 52ccom 4590 . . . . . . . . . . . . 13  class  ( f  o.  g )
5512, 54, 47cseq 10344 . . . . . . . . . . . 12  class  seq 1
( ( +g  `  w
) ,  ( f  o.  g ) )
5649, 55cfv 5170 . . . . . . . . . . 11  class  (  seq 1 ( ( +g  `  w ) ,  ( f  o.  g ) ) `  ( `  y
) )
577, 56wceq 1335 . . . . . . . . . 10  wff  x  =  (  seq 1 ( ( +g  `  w
) ,  ( f  o.  g ) ) `
 ( `  y
) )
5853, 57wa 103 . . . . . . . . 9  wff  ( g : ( 1 ... ( `  y )
)
-1-1-onto-> y  /\  x  =  (  seq 1 ( ( +g  `  w ) ,  ( f  o.  g ) ) `  ( `  y ) ) )
5922ccnv 4585 . . . . . . . . . 10  class  `' f
604, 24cdif 3099 . . . . . . . . . 10  class  ( _V 
\  o )
6159, 60cima 4589 . . . . . . . . 9  class  ( `' f " ( _V 
\  o ) )
6258, 8, 61wsbc 2937 . . . . . . . 8  wff  [. ( `' f " ( _V  \  o ) )  /  y ]. (
g : ( 1 ... ( `  y
) ) -1-1-onto-> y  /\  x  =  (  seq 1
( ( +g  `  w
) ,  ( f  o.  g ) ) `
 ( `  y
) ) )
6362, 51wex 1472 . . . . . . 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 5133 . . . . . 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 3505 . . . . 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 3505 . . . 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 3031 . . 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, 67cmpo 5826 . 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 1335 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: (None)
  Copyright terms: Public domain W3C validator