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 35062
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 35061 . 2  class FinSum
2 vx . . 3  setvar  x
3 vy . . . . . . 7  setvar  y
43cv 1397 . . . . . 6  class  y
5 ccmn 16997 . . . . . 6  class CMnd
64, 5wcel 1823 . . . . 5  wff  y  e. CMnd
7 vt . . . . . . . 8  setvar  t
87cv 1397 . . . . . . 7  class  t
9 cbs 14716 . . . . . . . 8  class  Base
104, 9cfv 5570 . . . . . . 7  class  ( Base `  y )
11 vz . . . . . . . 8  setvar  z
1211cv 1397 . . . . . . 7  class  z
138, 10, 12wf 5566 . . . . . 6  wff  z : t --> ( Base `  y
)
14 cfn 7509 . . . . . 6  class  Fin
1513, 7, 14wrex 2805 . . . . 5  wff  E. t  e.  Fin  z : t --> ( Base `  y
)
166, 15wa 367 . . . 4  wff  ( y  e. CMnd  /\  E. t  e.  Fin  z : t --> ( Base `  y
) )
1716, 3, 11copab 4496 . . 3  class  { <. y ,  z >.  |  ( y  e. CMnd  /\  E. t  e.  Fin  z : t --> ( Base `  y
) ) }
18 c1 9482 . . . . . . . . 9  class  1
19 vm . . . . . . . . . 10  setvar  m
2019cv 1397 . . . . . . . . 9  class  m
21 cfz 11675 . . . . . . . . 9  class  ...
2218, 20, 21co 6270 . . . . . . . 8  class  ( 1 ... m )
232cv 1397 . . . . . . . . . 10  class  x
24 c2nd 6772 . . . . . . . . . 10  class  2nd
2523, 24cfv 5570 . . . . . . . . 9  class  ( 2nd `  x )
2625cdm 4988 . . . . . . . 8  class  dom  ( 2nd `  x )
27 vf . . . . . . . . 9  setvar  f
2827cv 1397 . . . . . . . 8  class  f
2922, 26, 28wf1o 5569 . . . . . . 7  wff  f : ( 1 ... m
)
-1-1-onto-> dom  ( 2nd `  x
)
30 vs . . . . . . . . 9  setvar  s
3130cv 1397 . . . . . . . 8  class  s
32 c1st 6771 . . . . . . . . . . . 12  class  1st
3323, 32cfv 5570 . . . . . . . . . . 11  class  ( 1st `  x )
34 cplusg 14784 . . . . . . . . . . 11  class  +g
3533, 34cfv 5570 . . . . . . . . . 10  class  ( +g  `  ( 1st `  x
) )
36 vn . . . . . . . . . . 11  setvar  n
37 cn 10531 . . . . . . . . . . 11  class  NN
3836cv 1397 . . . . . . . . . . . . 13  class  n
3938, 28cfv 5570 . . . . . . . . . . . 12  class  ( f `
 n )
4039, 25cfv 5570 . . . . . . . . . . 11  class  ( ( 2nd `  x ) `
 ( f `  n ) )
4136, 37, 40cmpt 4497 . . . . . . . . . 10  class  ( n  e.  NN  |->  ( ( 2nd `  x ) `
 ( f `  n ) ) )
4235, 41, 18cseq 12089 . . . . . . . . 9  class  seq 1
( ( +g  `  ( 1st `  x ) ) ,  ( n  e.  NN  |->  ( ( 2nd `  x ) `  (
f `  n )
) ) )
4320, 42cfv 5570 . . . . . . . 8  class  (  seq 1 ( ( +g  `  ( 1st `  x
) ) ,  ( n  e.  NN  |->  ( ( 2nd `  x
) `  ( f `  n ) ) ) ) `  m )
4431, 43wceq 1398 . . . . . . 7  wff  s  =  (  seq 1 ( ( +g  `  ( 1st `  x ) ) ,  ( n  e.  NN  |->  ( ( 2nd `  x ) `  (
f `  n )
) ) ) `  m )
4529, 44wa 367 . . . . . 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 1617 . . . . 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 10791 . . . . 5  class  NN0
4846, 19, 47wrex 2805 . . . 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 5532 . . 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 4497 . 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 1398 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  35063
  Copyright terms: Public domain W3C validator