Metamath Proof Explorer

Definition df-bj-finsum

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)

Ref Expression
Assertion 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 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfinsum 
 |-  FinSum
1 vx 
 |-  x
2 vy 
 |-  y
3 vz 
 |-  z
4 2 cv 
 |-  y
5 ccmn 
 |-  CMnd
6 4 5 wcel 
 |-  y e. CMnd
7 vt 
 |-  t
8 cfn 
 |-  Fin
9 3 cv 
 |-  z
10 7 cv 
 |-  t
11 cbs 
 |-  Base
12 4 11 cfv 
 |-  ( Base ` y )
13 10 12 9 wf 
 |-  z : t --> ( Base ` y )
14 13 7 8 wrex 
 |-  E. t e. Fin z : t --> ( Base ` y )
15 6 14 wa 
 |-  ( y e. CMnd /\ E. t e. Fin z : t --> ( Base ` y ) )
16 15 2 3 copab 
 |-  { <. y , z >. | ( y e. CMnd /\ E. t e. Fin z : t --> ( Base ` y ) ) }
17 vs 
 |-  s
18 vm 
 |-  m
19 cn0 
 |-  NN0
20 vf 
 |-  f
21 20 cv 
 |-  f
22 c1 
 |-  1
23 cfz 
 |-  ...
24 18 cv 
 |-  m
25 22 24 23 co 
 |-  ( 1 ... m )
26 c2nd 
 |-  2nd
27 1 cv 
 |-  x
28 27 26 cfv 
 |-  ( 2nd ` x )
29 28 cdm 
 |-  dom ( 2nd ` x )
30 25 29 21 wf1o 
 |-  f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x )
31 17 cv 
 |-  s
32 cplusg 
 |-  +g
33 c1st 
 |-  1st
34 27 33 cfv 
 |-  ( 1st ` x )
35 34 32 cfv 
 |-  ( +g ` ( 1st ` x ) )
36 vn 
 |-  n
37 cn 
 |-  NN
38 36 cv 
 |-  n
39 38 21 cfv 
 |-  ( f ` n )
40 39 28 cfv 
 |-  ( ( 2nd ` x ) ` ( f ` n ) )
41 36 37 40 cmpt 
 |-  ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) )
42 35 41 22 cseq 
 |-  seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) )
43 24 42 cfv 
 |-  ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m )
44 31 43 wceq 
 |-  s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m )
45 30 44 wa 
 |-  ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) )
46 45 20 wex 
 |-  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 46 18 19 wrex 
 |-  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 ) )
48 47 17 cio 
 |-  ( 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 ) ) )
49 1 16 48 cmpt 
 |-  ( 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 ) ) ) )
50 0 49 wceq 
 |-  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 ) ) ) )