Definition df-bj-finsum 37317

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 37316	. 2 class FinSum
2		vx	. . 3 setvar 𝑥
3		vy	. . . . . . 7 setvar 𝑦
4	3	cv 1540	. . . . . 6 class 𝑦
5		ccmn 19690	. . . . . 6 class CMnd
6	4, 5	wcel 2111	. . . . 5 wff 𝑦 ∈ CMnd
7		vt	. . . . . . . 8 setvar 𝑡
8	7	cv 1540	. . . . . . 7 class 𝑡
9		cbs 17117	. . . . . . . 8 class Base
10	4, 9	cfv 6481	. . . . . . 7 class (Base‘𝑦)
11		vz	. . . . . . . 8 setvar 𝑧
12	11	cv 1540	. . . . . . 7 class 𝑧
13	8, 10, 12	wf 6477	. . . . . 6 wff 𝑧:𝑡⟶(Base‘𝑦)
14		cfn 8869	. . . . . 6 class Fin
15	13, 7, 14	wrex 3056	. . . . 5 wff ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦)
16	6, 15	wa 395	. . . 4 wff (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))
17	16, 3, 11	copab 5153	. . 3 class {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))}
18		c1 11004	. . . . . . . . 9 class 1
19		vm	. . . . . . . . . 10 setvar 𝑚
20	19	cv 1540	. . . . . . . . 9 class 𝑚
21		cfz 13404	. . . . . . . . 9 class ...
22	18, 20, 21	co 7346	. . . . . . . 8 class (1...𝑚)
23	2	cv 1540	. . . . . . . . . 10 class 𝑥
24		c2nd 7920	. . . . . . . . . 10 class 2nd
25	23, 24	cfv 6481	. . . . . . . . 9 class (2nd ‘𝑥)
26	25	cdm 5616	. . . . . . . 8 class dom (2nd ‘𝑥)
27		vf	. . . . . . . . 9 setvar 𝑓
28	27	cv 1540	. . . . . . . 8 class 𝑓
29	22, 26, 28	wf1o 6480	. . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥)
30		vs	. . . . . . . . 9 setvar 𝑠
31	30	cv 1540	. . . . . . . 8 class 𝑠
32		c1st 7919	. . . . . . . . . . . 12 class 1st
33	23, 32	cfv 6481	. . . . . . . . . . 11 class (1st ‘𝑥)
34		cplusg 17158	. . . . . . . . . . 11 class +g
35	33, 34	cfv 6481	. . . . . . . . . 10 class (+g‘(1st ‘𝑥))
36		vn	. . . . . . . . . . 11 setvar 𝑛
37		cn 12122	. . . . . . . . . . 11 class ℕ
38	36	cv 1540	. . . . . . . . . . . . 13 class 𝑛
39	38, 28	cfv 6481	. . . . . . . . . . . 12 class (𝑓‘𝑛)
40	39, 25	cfv 6481	. . . . . . . . . . 11 class ((2nd ‘𝑥)‘(𝑓‘𝑛))
41	36, 37, 40	cmpt 5172	. . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛)))
42	35, 41, 18	cseq 13905	. . . . . . . . 9 class seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))
43	20, 42	cfv 6481	. . . . . . . 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 12378	. . . . 5 class ℕ0
48	46, 19, 47	wrex 3056	. . . 4 wff ∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))
49	48, 30	cio 6435	. . 3 class (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚)))
50	2, 17, 49	cmpt 5172	. 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  37318