Definition df-gfsum 16700

Description: Define the finite group sum (iterated sum) over an unordered finite set. As currently defined, df-igsum 13344 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 16699	. 2 class Σgf
2		vw	. . 3 setvar 𝑤
3		vf	. . 3 setvar 𝑓
4		ccmn 13873	. . 3 class CMnd
5		cvv 2802	. . 3 class V
6	3	cv 1396	. . . . . . 7 class 𝑓
7	6	cdm 4725	. . . . . 6 class dom 𝑓
8		cfn 6909	. . . . . 6 class Fin
9	7, 8	wcel 2202	. . . . 5 wff dom 𝑓 ∈ Fin
10		c1 8033	. . . . . . . . 9 class 1
11		chash 11038	. . . . . . . . . 10 class ♯
12	7, 11	cfv 5326	. . . . . . . . 9 class (♯‘dom 𝑓)
13		cfz 10243	. . . . . . . . 9 class ...
14	10, 12, 13	co 6018	. . . . . . . 8 class (1...(♯‘dom 𝑓))
15		vg	. . . . . . . . 9 setvar 𝑔
16	15	cv 1396	. . . . . . . 8 class 𝑔
17	14, 7, 16	wf1o 5325	. . . . . . 7 wff 𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓
18		vx	. . . . . . . . 9 setvar 𝑥
19	18	cv 1396	. . . . . . . 8 class 𝑥
20	2	cv 1396	. . . . . . . . 9 class 𝑤
21	6, 16	ccom 4729	. . . . . . . . 9 class (𝑓 ∘ 𝑔)
22		cgsu 13342	. . . . . . . . 9 class Σg
23	20, 21, 22	co 6018	. . . . . . . 8 class (𝑤 Σg (𝑓 ∘ 𝑔))
24	19, 23	wceq 1397	. . . . . . 7 wff 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔))
25	17, 24	wa 104	. . . . . 6 wff (𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔)))
26	25, 15	wex 1540	. . . . 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 5284	. . 3 class (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔)))))
29	2, 3, 4, 5, 28	cmpo 6020	. 2 class (𝑤 ∈ CMnd, 𝑓 ∈ V ↦ (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔))))))
30	1, 29	wceq 1397	1 wff Σgf = (𝑤 ∈ CMnd, 𝑓 ∈ V ↦ (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔))))))

This definition is referenced by:  gfsumval  16701