Definition df-bj-finsum 37272

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 37271	. 2 class FinSum
2		vx	. . 3 setvar 𝑥
3		vy	. . . . . . 7 setvar 𝑦
4	3	cv 1539	. . . . . 6 class 𝑦
5		ccmn 19710	. . . . . 6 class CMnd
6	4, 5	wcel 2109	. . . . 5 wff 𝑦 ∈ CMnd
7		vt	. . . . . . . 8 setvar 𝑡
8	7	cv 1539	. . . . . . 7 class 𝑡
9		cbs 17179	. . . . . . . 8 class Base
10	4, 9	cfv 6511	. . . . . . 7 class (Base‘𝑦)
11		vz	. . . . . . . 8 setvar 𝑧
12	11	cv 1539	. . . . . . 7 class 𝑧
13	8, 10, 12	wf 6507	. . . . . 6 wff 𝑧:𝑡⟶(Base‘𝑦)
14		cfn 8918	. . . . . 6 class Fin
15	13, 7, 14	wrex 3053	. . . . 5 wff ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦)
16	6, 15	wa 395	. . . 4 wff (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))
17	16, 3, 11	copab 5169	. . 3 class {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))}
18		c1 11069	. . . . . . . . 9 class 1
19		vm	. . . . . . . . . 10 setvar 𝑚
20	19	cv 1539	. . . . . . . . 9 class 𝑚
21		cfz 13468	. . . . . . . . 9 class ...
22	18, 20, 21	co 7387	. . . . . . . 8 class (1...𝑚)
23	2	cv 1539	. . . . . . . . . 10 class 𝑥
24		c2nd 7967	. . . . . . . . . 10 class 2nd
25	23, 24	cfv 6511	. . . . . . . . 9 class (2nd ‘𝑥)
26	25	cdm 5638	. . . . . . . 8 class dom (2nd ‘𝑥)
27		vf	. . . . . . . . 9 setvar 𝑓
28	27	cv 1539	. . . . . . . 8 class 𝑓
29	22, 26, 28	wf1o 6510	. . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥)
30		vs	. . . . . . . . 9 setvar 𝑠
31	30	cv 1539	. . . . . . . 8 class 𝑠
32		c1st 7966	. . . . . . . . . . . 12 class 1st
33	23, 32	cfv 6511	. . . . . . . . . . 11 class (1st ‘𝑥)
34		cplusg 17220	. . . . . . . . . . 11 class +g
35	33, 34	cfv 6511	. . . . . . . . . 10 class (+g‘(1st ‘𝑥))
36		vn	. . . . . . . . . . 11 setvar 𝑛
37		cn 12186	. . . . . . . . . . 11 class ℕ
38	36	cv 1539	. . . . . . . . . . . . 13 class 𝑛
39	38, 28	cfv 6511	. . . . . . . . . . . 12 class (𝑓‘𝑛)
40	39, 25	cfv 6511	. . . . . . . . . . 11 class ((2nd ‘𝑥)‘(𝑓‘𝑛))
41	36, 37, 40	cmpt 5188	. . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛)))
42	35, 41, 18	cseq 13966	. . . . . . . . 9 class seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))
43	20, 42	cfv 6511	. . . . . . . 8 class (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚)
44	31, 43	wceq 1540	. . . . . . 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 1779	. . . . 5 wff ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))
47		cn0 12442	. . . . 5 class ℕ0
48	46, 19, 47	wrex 3053	. . . 4 wff ∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))
49	48, 30	cio 6462	. . 3 class (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚)))
50	2, 17, 49	cmpt 5188	. 2 class (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))))
51	1, 50	wceq 1540	1 wff FinSum = (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))))

This definition is referenced by:  bj-finsumval0  37273