Definition df-bj-finsum 37227

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 37226	. 2 class FinSum
2		vx	. . 3 setvar 𝑥
3		vy	. . . . . . 7 setvar 𝑦
4	3	cv 1534	. . . . . 6 class 𝑦
5		ccmn 19799	. . . . . 6 class CMnd
6	4, 5	wcel 2104	. . . . 5 wff 𝑦 ∈ CMnd
7		vt	. . . . . . . 8 setvar 𝑡
8	7	cv 1534	. . . . . . 7 class 𝑡
9		cbs 17235	. . . . . . . 8 class Base
10	4, 9	cfv 6559	. . . . . . 7 class (Base‘𝑦)
11		vz	. . . . . . . 8 setvar 𝑧
12	11	cv 1534	. . . . . . 7 class 𝑧
13	8, 10, 12	wf 6555	. . . . . 6 wff 𝑧:𝑡⟶(Base‘𝑦)
14		cfn 8979	. . . . . 6 class Fin
15	13, 7, 14	wrex 3066	. . . . 5 wff ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦)
16	6, 15	wa 395	. . . 4 wff (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))
17	16, 3, 11	copab 5212	. . 3 class {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))}
18		c1 11148	. . . . . . . . 9 class 1
19		vm	. . . . . . . . . 10 setvar 𝑚
20	19	cv 1534	. . . . . . . . 9 class 𝑚
21		cfz 13538	. . . . . . . . 9 class ...
22	18, 20, 21	co 7426	. . . . . . . 8 class (1...𝑚)
23	2	cv 1534	. . . . . . . . . 10 class 𝑥
24		c2nd 8007	. . . . . . . . . 10 class 2nd
25	23, 24	cfv 6559	. . . . . . . . 9 class (2nd ‘𝑥)
26	25	cdm 5684	. . . . . . . 8 class dom (2nd ‘𝑥)
27		vf	. . . . . . . . 9 setvar 𝑓
28	27	cv 1534	. . . . . . . 8 class 𝑓
29	22, 26, 28	wf1o 6558	. . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥)
30		vs	. . . . . . . . 9 setvar 𝑠
31	30	cv 1534	. . . . . . . 8 class 𝑠
32		c1st 8006	. . . . . . . . . . . 12 class 1st
33	23, 32	cfv 6559	. . . . . . . . . . 11 class (1st ‘𝑥)
34		cplusg 17288	. . . . . . . . . . 11 class +g
35	33, 34	cfv 6559	. . . . . . . . . 10 class (+g‘(1st ‘𝑥))
36		vn	. . . . . . . . . . 11 setvar 𝑛
37		cn 12258	. . . . . . . . . . 11 class ℕ
38	36	cv 1534	. . . . . . . . . . . . 13 class 𝑛
39	38, 28	cfv 6559	. . . . . . . . . . . 12 class (𝑓‘𝑛)
40	39, 25	cfv 6559	. . . . . . . . . . 11 class ((2nd ‘𝑥)‘(𝑓‘𝑛))
41	36, 37, 40	cmpt 5233	. . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛)))
42	35, 41, 18	cseq 14029	. . . . . . . . 9 class seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))
43	20, 42	cfv 6559	. . . . . . . 8 class (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚)
44	31, 43	wceq 1535	. . . . . . 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 1774	. . . . 5 wff ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))
47		cn0 12518	. . . . 5 class ℕ0
48	46, 19, 47	wrex 3066	. . . 4 wff ∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))
49	48, 30	cio 6509	. . 3 class (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚)))
50	2, 17, 49	cmpt 5233	. 2 class (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))))
51	1, 50	wceq 1535	1 wff FinSum = (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))))

This definition is referenced by:  bj-finsumval0  37228