Definition df-bj-finsum

Description: Finite summation in commutative monoids. This finite summation function can be extended to pairs <. y , z >. where y is a left-unital magma and z 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)

	Ref	Expression
Assertion	df-bj-finsum	⊢ FinSum = ( 𝑥 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝑦 ) ) } ↦ ( ℩ 𝑠 ∃ 𝑚 ∈ ℕ0 ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +g ‘ ( 1st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfinsum	⊢ FinSum
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3		vz	⊢ 𝑧
4	2	cv	⊢ 𝑦
5		ccmn	⊢ CMnd
6	4 5	wcel	⊢ 𝑦 ∈ CMnd
7		vt	⊢ 𝑡
8		cfn	⊢ Fin
9	3	cv	⊢ 𝑧
10	7	cv	⊢ 𝑡
11		cbs	⊢ Base
12	4 11	cfv	⊢ ( Base ‘ 𝑦 )
13	10 12 9	wf	⊢ 𝑧 : 𝑡 ⟶ ( Base ‘ 𝑦 )
14	13 7 8	wrex	⊢ ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝑦 )
15	6 14	wa	⊢ ( 𝑦 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝑦 ) )
16	15 2 3	copab	⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝑦 ) ) }
17		vs	⊢ 𝑠
18		vm	⊢ 𝑚
19		cn0	⊢ ℕ0
20		vf	⊢ 𝑓
21	20	cv	⊢ 𝑓
22		c1	⊢ 1
23		cfz	⊢ ...
24	18	cv	⊢ 𝑚
25	22 24 23	co	⊢ ( 1 ... 𝑚 )
26		c2nd	⊢ 2nd
27	1	cv	⊢ 𝑥
28	27 26	cfv	⊢ ( 2nd ‘ 𝑥 )
29	28	cdm	⊢ dom ( 2nd ‘ 𝑥 )
30	25 29 21	wf1o	⊢ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2nd ‘ 𝑥 )
31	17	cv	⊢ 𝑠
32		cplusg	⊢ +g
33		c1st	⊢ 1st
34	27 33	cfv	⊢ ( 1st ‘ 𝑥 )
35	34 32	cfv	⊢ ( +g ‘ ( 1st ‘ 𝑥 ) )
36		vn	⊢ 𝑛
37		cn	⊢ ℕ
38	36	cv	⊢ 𝑛
39	38 21	cfv	⊢ ( 𝑓 ‘ 𝑛 )
40	39 28	cfv	⊢ ( ( 2nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) )
41	36 37 40	cmpt	⊢ ( 𝑛 ∈ ℕ ↦ ( ( 2nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
42	35 41 22	cseq	⊢ seq 1 ( ( +g ‘ ( 1st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
43	24 42	cfv	⊢ ( seq 1 ( ( +g ‘ ( 1st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 )
44	31 43	wceq	⊢ 𝑠 = ( seq 1 ( ( +g ‘ ( 1st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 )
45	30 44	wa	⊢ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +g ‘ ( 1st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) )
46	45 20	wex	⊢ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +g ‘ ( 1st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) )
47	46 18 19	wrex	⊢ ∃ 𝑚 ∈ ℕ0 ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +g ‘ ( 1st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) )
48	47 17	cio	⊢ ( ℩ 𝑠 ∃ 𝑚 ∈ ℕ0 ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +g ‘ ( 1st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) )
49	1 16 48	cmpt	⊢ ( 𝑥 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝑦 ) ) } ↦ ( ℩ 𝑠 ∃ 𝑚 ∈ ℕ0 ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +g ‘ ( 1st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) ) )
50	0 49	wceq	⊢ FinSum = ( 𝑥 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝑦 ) ) } ↦ ( ℩ 𝑠 ∃ 𝑚 ∈ ℕ0 ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +g ‘ ( 1st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) ) )