Definition df-bj-finsum 37349

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 37348	. 2 class FinSum
2		vx	. . 3 setvar 𝑥
3		vy	. . . . . . 7 setvar 𝑦
4	3	cv 1540	. . . . . 6 class 𝑦
5		ccmn 19694	. . . . . 6 class CMnd
6	4, 5	wcel 2113	. . . . 5 wff 𝑦 ∈ CMnd
7		vt	. . . . . . . 8 setvar 𝑡
8	7	cv 1540	. . . . . . 7 class 𝑡
9		cbs 17122	. . . . . . . 8 class Base
10	4, 9	cfv 6486	. . . . . . 7 class (Base‘𝑦)
11		vz	. . . . . . . 8 setvar 𝑧
12	11	cv 1540	. . . . . . 7 class 𝑧
13	8, 10, 12	wf 6482	. . . . . 6 wff 𝑧:𝑡⟶(Base‘𝑦)
14		cfn 8875	. . . . . 6 class Fin
15	13, 7, 14	wrex 3057	. . . . 5 wff ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦)
16	6, 15	wa 395	. . . 4 wff (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))
17	16, 3, 11	copab 5155	. . 3 class {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))}
18		c1 11014	. . . . . . . . 9 class 1
19		vm	. . . . . . . . . 10 setvar 𝑚
20	19	cv 1540	. . . . . . . . 9 class 𝑚
21		cfz 13409	. . . . . . . . 9 class ...
22	18, 20, 21	co 7352	. . . . . . . 8 class (1...𝑚)
23	2	cv 1540	. . . . . . . . . 10 class 𝑥
24		c2nd 7926	. . . . . . . . . 10 class 2nd
25	23, 24	cfv 6486	. . . . . . . . 9 class (2nd ‘𝑥)
26	25	cdm 5619	. . . . . . . 8 class dom (2nd ‘𝑥)
27		vf	. . . . . . . . 9 setvar 𝑓
28	27	cv 1540	. . . . . . . 8 class 𝑓
29	22, 26, 28	wf1o 6485	. . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥)
30		vs	. . . . . . . . 9 setvar 𝑠
31	30	cv 1540	. . . . . . . 8 class 𝑠
32		c1st 7925	. . . . . . . . . . . 12 class 1st
33	23, 32	cfv 6486	. . . . . . . . . . 11 class (1st ‘𝑥)
34		cplusg 17163	. . . . . . . . . . 11 class +g
35	33, 34	cfv 6486	. . . . . . . . . 10 class (+g‘(1st ‘𝑥))
36		vn	. . . . . . . . . . 11 setvar 𝑛
37		cn 12132	. . . . . . . . . . 11 class ℕ
38	36	cv 1540	. . . . . . . . . . . . 13 class 𝑛
39	38, 28	cfv 6486	. . . . . . . . . . . 12 class (𝑓‘𝑛)
40	39, 25	cfv 6486	. . . . . . . . . . 11 class ((2nd ‘𝑥)‘(𝑓‘𝑛))
41	36, 37, 40	cmpt 5174	. . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛)))
42	35, 41, 18	cseq 13910	. . . . . . . . 9 class seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))
43	20, 42	cfv 6486	. . . . . . . 8 class (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚)
44	31, 43	wceq 1541	. . . . . . 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 1780	. . . . 5 wff ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))
47		cn0 12388	. . . . 5 class ℕ0
48	46, 19, 47	wrex 3057	. . . 4 wff ∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))
49	48, 30	cio 6440	. . 3 class (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚)))
50	2, 17, 49	cmpt 5174	. 2 class (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))))
51	1, 50	wceq 1541	1 wff FinSum = (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))))

This definition is referenced by:  bj-finsumval0  37350