Definition df-gfsum 14106

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

Given G gfsum_gf 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-igsum 13561. (Contributed by Jim Kingdon, 23-Mar-2026.)

Assertion

Ref	Expression
df-gfsum	|- gfsumgf = ( 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 gsumg ( f o. g ) ) ) ) ) )

Distinct variable group:   w, f, x, g

Detailed syntax breakdown of Definition df-gfsum

Step	Hyp	Ref	Expression
1		cgfsu 14105	. 2 class gfsumgf
2		vw	. . 3 setvar w
3		vf	. . 3 setvar f
4		ccmn 14042	. . 3 class CMnd
5		cvv 2815	. . 3 class _V
6	3	cv 1397	. . . . . . 7 class f
7	6	cdm 4755	. . . . . 6 class dom f
8		cfn 6989	. . . . . 6 class Fin
9	7, 8	wcel 2205	. . . . 5 wff dom f e. Fin
10		c1 8145	. . . . . . . . 9 class 1
11		chash 11167	. . . . . . . . . 10 class ♯
12	7, 11	cfv 5358	. . . . . . . . 9 class (♯ ` dom f )
13		cfz 10365	. . . . . . . . 9 class ...
14	10, 12, 13	co 6059	. . . . . . . 8 class ( 1 ... (♯ ` dom f ) )
15		vg	. . . . . . . . 9 setvar g
16	15	cv 1397	. . . . . . . 8 class g
17	14, 7, 16	wf1o 5357	. . . . . . 7 wff g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f
18		vx	. . . . . . . . 9 setvar x
19	18	cv 1397	. . . . . . . 8 class x
20	2	cv 1397	. . . . . . . . 9 class w
21	6, 16	ccom 4759	. . . . . . . . 9 class ( f o. g )
22		cgsu 13559	. . . . . . . . 9 class gsumg
23	20, 21, 22	co 6059	. . . . . . . 8 class ( w gsumg ( f o. g ) )
24	19, 23	wceq 1398	. . . . . . 7 wff x = ( w gsumg ( f o. g ) )
25	17, 24	wa 104	. . . . . 6 wff ( g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f /\ x = ( w gsumg ( f o. g ) ) )
26	25, 15	wex 1541	. . . . 5 wff E. g ( g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f /\ x = ( w gsumg ( 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 gsumg ( f o. g ) ) ) )
28	27, 18	cio 5316	. . 3 class ( iota x ( dom f e. Fin /\ E. g ( g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f /\ x = ( w gsumg ( f o. g ) ) ) ) )
29	2, 3, 4, 5, 28	cmpo 6061	. 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 gsumg ( f o. g ) ) ) ) ) )
30	1, 29	wceq 1398	1 wff gfsumgf = ( 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 gsumg ( f o. g ) ) ) ) ) )

This definition is referenced by:  gfsumval  14107