Definition df-gsumfi 14128

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

Given G gsum_g F where F : A --> ( Base ` G ), the set of indices is A and the values are given by F at each index. For this notation, A is a finite set and G 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	|- gsumg = ( w e. CMnd , f e. _V |-> ( iota x ( dom f e. Fin /\ E. g ( g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f /\ x = ( w gzsumgz ( f o. g ) ) ) ) ) )

Distinct variable group:   w, f, x, g

Detailed syntax breakdown of Definition df-gsumfi

Step	Hyp	Ref	Expression
1		cgsu 14127	. 2 class gsumg
2		vw	. . 3 setvar w
3		vf	. . 3 setvar f
4		ccmn 14064	. . 3 class CMnd
5		cvv 2821	. . 3 class _V
6	3	cv 1401	. . . . . . 7 class f
7	6	cdm 4769	. . . . . 6 class dom f
8		cfn 7012	. . . . . 6 class Fin
9	7, 8	wcel 2209	. . . . 5 wff dom f e. Fin
10		c1 8170	. . . . . . . . 9 class 1
11		chash 11192	. . . . . . . . . 10 class ♯
12	7, 11	cfv 5372	. . . . . . . . 9 class (♯ ` dom f )
13		cfz 10390	. . . . . . . . 9 class ...
14	10, 12, 13	co 6075	. . . . . . . 8 class ( 1 ... (♯ ` dom f ) )
15		vg	. . . . . . . . 9 setvar g
16	15	cv 1401	. . . . . . . 8 class g
17	14, 7, 16	wf1o 5371	. . . . . . 7 wff g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f
18		vx	. . . . . . . . 9 setvar x
19	18	cv 1401	. . . . . . . 8 class x
20	2	cv 1401	. . . . . . . . 9 class w
21	6, 16	ccom 4773	. . . . . . . . 9 class ( f o. g )
22		cgzsu 13588	. . . . . . . . 9 class gzsumgz
23	20, 21, 22	co 6075	. . . . . . . 8 class ( w gzsumgz ( f o. g ) )
24	19, 23	wceq 1402	. . . . . . 7 wff x = ( w gzsumgz ( f o. g ) )
25	17, 24	wa 104	. . . . . 6 wff ( g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f /\ x = ( w gzsumgz ( f o. g ) ) )
26	25, 15	wex 1545	. . . . 5 wff E. g ( g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f /\ x = ( w gzsumgz ( f o. g ) ) )
27	9, 26	wa 104	. . . 4 wff ( dom f e. Fin /\ E. g ( g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f /\ x = ( w gzsumgz ( f o. g ) ) ) )
28	27, 18	cio 5330	. . 3 class ( iota x ( dom f e. Fin /\ E. g ( g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f /\ x = ( w gzsumgz ( f o. g ) ) ) ) )
29	2, 3, 4, 5, 28	cmpo 6077	. 2 class ( w e. CMnd , f e. _V |-> ( iota x ( dom f e. Fin /\ E. g ( g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f /\ x = ( w gzsumgz ( f o. g ) ) ) ) ) )
30	1, 29	wceq 1402	1 wff gsumg = ( w e. CMnd , f e. _V |-> ( iota x ( dom f e. Fin /\ E. g ( g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f /\ x = ( w gzsumgz ( f o. g ) ) ) ) ) )

This definition is referenced by:  gsumvalfi  14129