Definition df-bj-finsum 37533

Description: Finite summation in commutative monoids. This finite summation function can be extended to pairs ⟨𝑦, 𝑧⟩ where 𝑦 is a left-unital magma and 𝑧 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 = (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))))

Distinct variable group:   𝑥,𝑦,𝑧,𝑡,𝑠,𝑓,𝑚,𝑛

Detailed syntax breakdown of Definition df-bj-finsum

Step	Hyp	Ref	Expression
1		cfinsum 37532	. 2 class FinSum
2		vx	. . 3 setvar 𝑥
3		vy	. . . . . . 7 setvar 𝑦
4	3	cv 1541	. . . . . 6 class 𝑦
5		ccmn 19721	. . . . . 6 class CMnd
6	4, 5	wcel 2114	. . . . 5 wff 𝑦 ∈ CMnd
7		vt	. . . . . . . 8 setvar 𝑡
8	7	cv 1541	. . . . . . 7 class 𝑡
9		cbs 17148	. . . . . . . 8 class Base
10	4, 9	cfv 6500	. . . . . . 7 class (Base‘𝑦)
11		vz	. . . . . . . 8 setvar 𝑧
12	11	cv 1541	. . . . . . 7 class 𝑧
13	8, 10, 12	wf 6496	. . . . . 6 wff 𝑧:𝑡⟶(Base‘𝑦)
14		cfn 8895	. . . . . 6 class Fin
15	13, 7, 14	wrex 3062	. . . . 5 wff ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦)
16	6, 15	wa 395	. . . 4 wff (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))
17	16, 3, 11	copab 5162	. . 3 class {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))}
18		c1 11039	. . . . . . . . 9 class 1
19		vm	. . . . . . . . . 10 setvar 𝑚
20	19	cv 1541	. . . . . . . . 9 class 𝑚
21		cfz 13435	. . . . . . . . 9 class ...
22	18, 20, 21	co 7368	. . . . . . . 8 class (1...𝑚)
23	2	cv 1541	. . . . . . . . . 10 class 𝑥
24		c2nd 7942	. . . . . . . . . 10 class 2nd
25	23, 24	cfv 6500	. . . . . . . . 9 class (2nd ‘𝑥)
26	25	cdm 5632	. . . . . . . 8 class dom (2nd ‘𝑥)
27		vf	. . . . . . . . 9 setvar 𝑓
28	27	cv 1541	. . . . . . . 8 class 𝑓
29	22, 26, 28	wf1o 6499	. . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥)
30		vs	. . . . . . . . 9 setvar 𝑠
31	30	cv 1541	. . . . . . . 8 class 𝑠
32		c1st 7941	. . . . . . . . . . . 12 class 1st
33	23, 32	cfv 6500	. . . . . . . . . . 11 class (1st ‘𝑥)
34		cplusg 17189	. . . . . . . . . . 11 class +g
35	33, 34	cfv 6500	. . . . . . . . . 10 class (+g‘(1st ‘𝑥))
36		vn	. . . . . . . . . . 11 setvar 𝑛
37		cn 12157	. . . . . . . . . . 11 class ℕ
38	36	cv 1541	. . . . . . . . . . . . 13 class 𝑛
39	38, 28	cfv 6500	. . . . . . . . . . . 12 class (𝑓‘𝑛)
40	39, 25	cfv 6500	. . . . . . . . . . 11 class ((2nd ‘𝑥)‘(𝑓‘𝑛))
41	36, 37, 40	cmpt 5181	. . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛)))
42	35, 41, 18	cseq 13936	. . . . . . . . 9 class seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))
43	20, 42	cfv 6500	. . . . . . . 8 class (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚)
44	31, 43	wceq 1542	. . . . . . 7 wff 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚)
45	29, 44	wa 395	. . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))
46	45, 27	wex 1781	. . . . 5 wff ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))
47		cn0 12413	. . . . 5 class ℕ0
48	46, 19, 47	wrex 3062	. . . 4 wff ∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))
49	48, 30	cio 6454	. . 3 class (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚)))
50	2, 17, 49	cmpt 5181	. 2 class (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))))
51	1, 50	wceq 1542	1 wff FinSum = (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))))

This definition is referenced by:  bj-finsumval0  37534