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 ∈ y z | y ∈ CMnd ∧ ∃ t ∈ Fin z : t ⟶ Base y ⟼ ι s | ∃ m ∈ ℕ 0 ∃ f f : 1 … m ⟶ 1-1 onto dom ⁡ 2 nd ⁡ x ∧ s = seq 1 + 1 st ⁡ x n ∈ ℕ ⟼ 2 nd ⁡ x ⁡ f ⁡ n ⁡ m

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfinsum class FinSum
1 vx setvar x
2 vy setvar y
3 vz setvar z
4 2 cv setvar y
5 ccmn class CMnd
6 4 5 wcel wff y ∈ CMnd
7 vt setvar t
8 cfn class Fin
9 3 cv setvar z
10 7 cv setvar t
11 cbs class Base
12 4 11 cfv class Base y
13 10 12 9 wf wff z : t ⟶ Base y
14 13 7 8 wrex wff ∃ t ∈ Fin z : t ⟶ Base y
15 6 14 wa wff y ∈ CMnd ∧ ∃ t ∈ Fin z : t ⟶ Base y
16 15 2 3 copab class y z | y ∈ CMnd ∧ ∃ t ∈ Fin z : t ⟶ Base y
17 vs setvar s
18 vm setvar m
19 cn0 class ℕ 0
20 vf setvar f
21 20 cv setvar f
22 c1 class 1
23 cfz class …
24 18 cv setvar m
25 22 24 23 co class 1 … m
26 c2nd class 2 nd
27 1 cv setvar x
28 27 26 cfv class 2 nd ⁡ x
29 28 cdm class dom ⁡ 2 nd ⁡ x
30 25 29 21 wf1o wff f : 1 … m ⟶ 1-1 onto dom ⁡ 2 nd ⁡ x
31 17 cv setvar s
32 cplusg class + 𝑔
33 c1st class 1 st
34 27 33 cfv class 1 st ⁡ x
35 34 32 cfv class + 1 st ⁡ x
36 vn setvar n
37 cn class ℕ
38 36 cv setvar n
39 38 21 cfv class f ⁡ n
40 39 28 cfv class 2 nd ⁡ x ⁡ f ⁡ n
41 36 37 40 cmpt class n ∈ ℕ ⟼ 2 nd ⁡ x ⁡ f ⁡ n
42 35 41 22 cseq class seq 1 + 1 st ⁡ x n ∈ ℕ ⟼ 2 nd ⁡ x ⁡ f ⁡ n
43 24 42 cfv class seq 1 + 1 st ⁡ x n ∈ ℕ ⟼ 2 nd ⁡ x ⁡ f ⁡ n ⁡ m
44 31 43 wceq wff s = seq 1 + 1 st ⁡ x n ∈ ℕ ⟼ 2 nd ⁡ x ⁡ f ⁡ n ⁡ m
45 30 44 wa wff f : 1 … m ⟶ 1-1 onto dom ⁡ 2 nd ⁡ x ∧ s = seq 1 + 1 st ⁡ x n ∈ ℕ ⟼ 2 nd ⁡ x ⁡ f ⁡ n ⁡ m
46 45 20 wex wff ∃ f f : 1 … m ⟶ 1-1 onto dom ⁡ 2 nd ⁡ x ∧ s = seq 1 + 1 st ⁡ x n ∈ ℕ ⟼ 2 nd ⁡ x ⁡ f ⁡ n ⁡ m
47 46 18 19 wrex wff ∃ m ∈ ℕ 0 ∃ f f : 1 … m ⟶ 1-1 onto dom ⁡ 2 nd ⁡ x ∧ s = seq 1 + 1 st ⁡ x n ∈ ℕ ⟼ 2 nd ⁡ x ⁡ f ⁡ n ⁡ m
48 47 17 cio class ι s | ∃ m ∈ ℕ 0 ∃ f f : 1 … m ⟶ 1-1 onto dom ⁡ 2 nd ⁡ x ∧ s = seq 1 + 1 st ⁡ x n ∈ ℕ ⟼ 2 nd ⁡ x ⁡ f ⁡ n ⁡ m
49 1 16 48 cmpt class x ∈ y z | y ∈ CMnd ∧ ∃ t ∈ Fin z : t ⟶ Base y ⟼ ι s | ∃ m ∈ ℕ 0 ∃ f f : 1 … m ⟶ 1-1 onto dom ⁡ 2 nd ⁡ x ∧ s = seq 1 + 1 st ⁡ x n ∈ ℕ ⟼ 2 nd ⁡ x ⁡ f ⁡ n ⁡ m
50 0 49 wceq wff FinSum = x ∈ y z | y ∈ CMnd ∧ ∃ t ∈ Fin z : t ⟶ Base y ⟼ ι s | ∃ m ∈ ℕ 0 ∃ f f : 1 … m ⟶ 1-1 onto dom ⁡ 2 nd ⁡ x ∧ s = seq 1 + 1 st ⁡ x n ∈ ℕ ⟼ 2 nd ⁡ x ⁡ f ⁡ n ⁡ m