Definition df-gfsum 16629

Description: Define the finite group sum (iterated sum) over an unordered finite set. As currently defined, df-igsum 13335 is indexed by consecutive integers, but in the case of a commutative monoid, the order of the sum doesn't matter and we can define a sum indexed by any finite set without needing to specify an order. (Contributed by Jim Kingdon, 23-Mar-2026.)

Assertion

Ref	Expression
df-gfsum	⊢ Σgf = (𝑤 ∈ CMnd, 𝑓 ∈ V ↦ (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔))))))

Distinct variable group:   𝑤,𝑓,𝑥,𝑔

Detailed syntax breakdown of Definition df-gfsum

Step	Hyp	Ref	Expression
1		cgfsu 16628	. 2 class Σgf
2		vw	. . 3 setvar 𝑤
3		vf	. . 3 setvar 𝑓
4		ccmn 13864	. . 3 class CMnd
5		cvv 2800	. . 3 class V
6	3	cv 1394	. . . . . . 7 class 𝑓
7	6	cdm 4723	. . . . . 6 class dom 𝑓
8		cfn 6904	. . . . . 6 class Fin
9	7, 8	wcel 2200	. . . . 5 wff dom 𝑓 ∈ Fin
10		c1 8026	. . . . . . . . 9 class 1
11		chash 11030	. . . . . . . . . 10 class ♯
12	7, 11	cfv 5324	. . . . . . . . 9 class (♯‘dom 𝑓)
13		cfz 10236	. . . . . . . . 9 class ...
14	10, 12, 13	co 6013	. . . . . . . 8 class (1...(♯‘dom 𝑓))
15		vg	. . . . . . . . 9 setvar 𝑔
16	15	cv 1394	. . . . . . . 8 class 𝑔
17	14, 7, 16	wf1o 5323	. . . . . . 7 wff 𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓
18		vx	. . . . . . . . 9 setvar 𝑥
19	18	cv 1394	. . . . . . . 8 class 𝑥
20	2	cv 1394	. . . . . . . . 9 class 𝑤
21	6, 16	ccom 4727	. . . . . . . . 9 class (𝑓 ∘ 𝑔)
22		cgsu 13333	. . . . . . . . 9 class Σg
23	20, 21, 22	co 6013	. . . . . . . 8 class (𝑤 Σg (𝑓 ∘ 𝑔))
24	19, 23	wceq 1395	. . . . . . 7 wff 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔))
25	17, 24	wa 104	. . . . . 6 wff (𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔)))
26	25, 15	wex 1538	. . . . 5 wff ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔)))
27	9, 26	wa 104	. . . 4 wff (dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔))))
28	27, 18	cio 5282	. . 3 class (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔)))))
29	2, 3, 4, 5, 28	cmpo 6015	. 2 class (𝑤 ∈ CMnd, 𝑓 ∈ V ↦ (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔))))))
30	1, 29	wceq 1395	1 wff Σgf = (𝑤 ∈ CMnd, 𝑓 ∈ V ↦ (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔))))))

This definition is referenced by:  gfsumval  16630