Definition df-gsumfi 14128

Description: Define the finite group sum (iterated sum) over an unordered finite set.

Given 𝐺 Σ_g 𝐹 where 𝐹:𝐴⟶(Base‘𝐺), the set of indices is 𝐴 and the values are given by 𝐹 at each index. For this notation, 𝐴 is a finite set and 𝐺 is a commutative monoid, and the sum adds up these elements in some order (the sum does not depend on the order).

For a sum indexed by consecutive integers (and thus defining an order for the sum), see df-gzsum 13590. (Contributed by Jim Kingdon, 23-Mar-2026.)

Assertion

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

Distinct variable group:   𝑤,𝑓,𝑥,𝑔

Detailed syntax breakdown of Definition df-gsumfi

Step	Hyp	Ref	Expression
1		cgsu 14127	. 2 class Σg
2		vw	. . 3 setvar 𝑤
3		vf	. . 3 setvar 𝑓
4		ccmn 14064	. . 3 class CMnd
5		cvv 2821	. . 3 class V
6	3	cv 1401	. . . . . . 7 class 𝑓
7	6	cdm 4769	. . . . . 6 class dom 𝑓
8		cfn 7012	. . . . . 6 class Fin
9	7, 8	wcel 2209	. . . . 5 wff dom 𝑓 ∈ Fin
10		c1 8170	. . . . . . . . 9 class 1
11		chash 11192	. . . . . . . . . 10 class ♯
12	7, 11	cfv 5372	. . . . . . . . 9 class (♯‘dom 𝑓)
13		cfz 10390	. . . . . . . . 9 class ...
14	10, 12, 13	co 6075	. . . . . . . 8 class (1...(♯‘dom 𝑓))
15		vg	. . . . . . . . 9 setvar 𝑔
16	15	cv 1401	. . . . . . . 8 class 𝑔
17	14, 7, 16	wf1o 5371	. . . . . . 7 wff 𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓
18		vx	. . . . . . . . 9 setvar 𝑥
19	18	cv 1401	. . . . . . . 8 class 𝑥
20	2	cv 1401	. . . . . . . . 9 class 𝑤
21	6, 16	ccom 4773	. . . . . . . . 9 class (𝑓 ∘ 𝑔)
22		cgzsu 13588	. . . . . . . . 9 class Σgz
23	20, 21, 22	co 6075	. . . . . . . 8 class (𝑤 Σgz (𝑓 ∘ 𝑔))
24	19, 23	wceq 1402	. . . . . . 7 wff 𝑥 = (𝑤 Σgz (𝑓 ∘ 𝑔))
25	17, 24	wa 104	. . . . . 6 wff (𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σgz (𝑓 ∘ 𝑔)))
26	25, 15	wex 1545	. . . . 5 wff ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σgz (𝑓 ∘ 𝑔)))
27	9, 26	wa 104	. . . 4 wff (dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σgz (𝑓 ∘ 𝑔))))
28	27, 18	cio 5330	. . 3 class (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σgz (𝑓 ∘ 𝑔)))))
29	2, 3, 4, 5, 28	cmpo 6077	. 2 class (𝑤 ∈ CMnd, 𝑓 ∈ V ↦ (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σgz (𝑓 ∘ 𝑔))))))
30	1, 29	wceq 1402	1 wff Σg = (𝑤 ∈ CMnd, 𝑓 ∈ V ↦ (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σgz (𝑓 ∘ 𝑔))))))

This definition is referenced by:  gsumvalfi  14129