Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-finsum Structured version   Unicode version

Definition df-bj-finsum 32921
Description: Finite summation in commutative monoids. This finite summation function can be extended to pairs 
<. y ,  z >. where  y is a left-unital magma and  z is defined on a totally ordered set (choosing left-associative composition), or dropping unitality and requiring nonempty families, or on any monoids for families of permutable elements, etc. We use the term "summation", even though the definition stands for any unital, commutative and associative composition law. (Contributed by BJ, 9-Jun-2019.)
Assertion
Ref Expression
df-bj-finsum  |- FinSum  =  ( x  e.  { <. y ,  z >.  |  ( y  e. CMnd  /\  E. t  e.  Fin  z : t --> ( Base `  y
) ) }  |->  ( iota s E. m  e.  NN0  E. f ( f : ( 1 ... m ) -1-1-onto-> dom  ( 2nd `  x )  /\  s  =  (  seq 1 ( ( +g  `  ( 1st `  x
) ) ,  ( n  e.  NN  |->  ( ( 2nd `  x
) `  ( f `  n ) ) ) ) `  m ) ) ) )
Distinct variable group:    x, y, z, t, s, f, m, n

Detailed syntax breakdown of Definition df-bj-finsum
StepHypRef Expression
1 cfinsum 32920 . 2  class FinSum
2 vx . . 3  setvar  x
3 vy . . . . . . 7  setvar  y
43cv 1369 . . . . . 6  class  y
5 ccmn 16399 . . . . . 6  class CMnd
64, 5wcel 1758 . . . . 5  wff  y  e. CMnd
7 vt . . . . . . . 8  setvar  t
87cv 1369 . . . . . . 7  class  t
9 cbs 14293 . . . . . . . 8  class  Base
104, 9cfv 5527 . . . . . . 7  class  ( Base `  y )
11 vz . . . . . . . 8  setvar  z
1211cv 1369 . . . . . . 7  class  z
138, 10, 12wf 5523 . . . . . 6  wff  z : t --> ( Base `  y
)
14 cfn 7421 . . . . . 6  class  Fin
1513, 7, 14wrex 2800 . . . . 5  wff  E. t  e.  Fin  z : t --> ( Base `  y
)
166, 15wa 369 . . . 4  wff  ( y  e. CMnd  /\  E. t  e.  Fin  z : t --> ( Base `  y
) )
1716, 3, 11copab 4458 . . 3  class  { <. y ,  z >.  |  ( y  e. CMnd  /\  E. t  e.  Fin  z : t --> ( Base `  y
) ) }
18 c1 9395 . . . . . . . . 9  class  1
19 vm . . . . . . . . . 10  setvar  m
2019cv 1369 . . . . . . . . 9  class  m
21 cfz 11555 . . . . . . . . 9  class  ...
2218, 20, 21co 6201 . . . . . . . 8  class  ( 1 ... m )
232cv 1369 . . . . . . . . . 10  class  x
24 c2nd 6687 . . . . . . . . . 10  class  2nd
2523, 24cfv 5527 . . . . . . . . 9  class  ( 2nd `  x )
2625cdm 4949 . . . . . . . 8  class  dom  ( 2nd `  x )
27 vf . . . . . . . . 9  setvar  f
2827cv 1369 . . . . . . . 8  class  f
2922, 26, 28wf1o 5526 . . . . . . 7  wff  f : ( 1 ... m
)
-1-1-onto-> dom  ( 2nd `  x
)
30 vs . . . . . . . . 9  setvar  s
3130cv 1369 . . . . . . . 8  class  s
32 c1st 6686 . . . . . . . . . . . 12  class  1st
3323, 32cfv 5527 . . . . . . . . . . 11  class  ( 1st `  x )
34 cplusg 14358 . . . . . . . . . . 11  class  +g
3533, 34cfv 5527 . . . . . . . . . 10  class  ( +g  `  ( 1st `  x
) )
36 vn . . . . . . . . . . 11  setvar  n
37 cn 10434 . . . . . . . . . . 11  class  NN
3836cv 1369 . . . . . . . . . . . . 13  class  n
3938, 28cfv 5527 . . . . . . . . . . . 12  class  ( f `
 n )
4039, 25cfv 5527 . . . . . . . . . . 11  class  ( ( 2nd `  x ) `
 ( f `  n ) )
4136, 37, 40cmpt 4459 . . . . . . . . . 10  class  ( n  e.  NN  |->  ( ( 2nd `  x ) `
 ( f `  n ) ) )
4235, 41, 18cseq 11924 . . . . . . . . 9  class  seq 1
( ( +g  `  ( 1st `  x ) ) ,  ( n  e.  NN  |->  ( ( 2nd `  x ) `  (
f `  n )
) ) )
4320, 42cfv 5527 . . . . . . . 8  class  (  seq 1 ( ( +g  `  ( 1st `  x
) ) ,  ( n  e.  NN  |->  ( ( 2nd `  x
) `  ( f `  n ) ) ) ) `  m )
4431, 43wceq 1370 . . . . . . 7  wff  s  =  (  seq 1 ( ( +g  `  ( 1st `  x ) ) ,  ( n  e.  NN  |->  ( ( 2nd `  x ) `  (
f `  n )
) ) ) `  m )
4529, 44wa 369 . . . . . 6  wff  ( f : ( 1 ... m ) -1-1-onto-> dom  ( 2nd `  x
)  /\  s  =  (  seq 1 ( ( +g  `  ( 1st `  x ) ) ,  ( n  e.  NN  |->  ( ( 2nd `  x
) `  ( f `  n ) ) ) ) `  m ) )
4645, 27wex 1587 . . . . 5  wff  E. f
( f : ( 1 ... m ) -1-1-onto-> dom  ( 2nd `  x
)  /\  s  =  (  seq 1 ( ( +g  `  ( 1st `  x ) ) ,  ( n  e.  NN  |->  ( ( 2nd `  x
) `  ( f `  n ) ) ) ) `  m ) )
47 cn0 10691 . . . . 5  class  NN0
4846, 19, 47wrex 2800 . . . 4  wff  E. m  e.  NN0  E. f ( f : ( 1 ... m ) -1-1-onto-> dom  ( 2nd `  x )  /\  s  =  (  seq 1 ( ( +g  `  ( 1st `  x
) ) ,  ( n  e.  NN  |->  ( ( 2nd `  x
) `  ( f `  n ) ) ) ) `  m ) )
4948, 30cio 5488 . . 3  class  ( iota s E. m  e. 
NN0  E. f ( f : ( 1 ... m ) -1-1-onto-> dom  ( 2nd `  x
)  /\  s  =  (  seq 1 ( ( +g  `  ( 1st `  x ) ) ,  ( n  e.  NN  |->  ( ( 2nd `  x
) `  ( f `  n ) ) ) ) `  m ) ) )
502, 17, 49cmpt 4459 . 2  class  ( x  e.  { <. y ,  z >.  |  ( y  e. CMnd  /\  E. t  e.  Fin  z : t --> ( Base `  y
) ) }  |->  ( iota s E. m  e.  NN0  E. f ( f : ( 1 ... m ) -1-1-onto-> dom  ( 2nd `  x )  /\  s  =  (  seq 1 ( ( +g  `  ( 1st `  x
) ) ,  ( n  e.  NN  |->  ( ( 2nd `  x
) `  ( f `  n ) ) ) ) `  m ) ) ) )
511, 50wceq 1370 1  wff FinSum  =  ( x  e.  { <. y ,  z >.  |  ( y  e. CMnd  /\  E. t  e.  Fin  z : t --> ( Base `  y
) ) }  |->  ( iota s E. m  e.  NN0  E. f ( f : ( 1 ... m ) -1-1-onto-> dom  ( 2nd `  x )  /\  s  =  (  seq 1 ( ( +g  `  ( 1st `  x
) ) ,  ( n  e.  NN  |->  ( ( 2nd `  x
) `  ( f `  n ) ) ) ) `  m ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  bj-finsumval0  32922
  Copyright terms: Public domain W3C validator