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	|- 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 16628	. 2 class gfsumgf
2		vw	. . 3 setvar w
3		vf	. . 3 setvar f
4		ccmn 13864	. . 3 class CMnd
5		cvv 2800	. . 3 class _V
6	3	cv 1394	. . . . . . 7 class f
7	6	cdm 4723	. . . . . 6 class dom f
8		cfn 6904	. . . . . 6 class Fin
9	7, 8	wcel 2200	. . . . 5 wff dom f e. Fin
10		c1 8026	. . . . . . . . 9 class 1
11		chash 11030	. . . . . . . . . 10 class ♯
12	7, 11	cfv 5324	. . . . . . . . 9 class (♯ ` dom f )
13		cfz 10236	. . . . . . . . 9 class ...
14	10, 12, 13	co 6013	. . . . . . . 8 class ( 1 ... (♯ ` dom f ) )
15		vg	. . . . . . . . 9 setvar g
16	15	cv 1394	. . . . . . . 8 class g
17	14, 7, 16	wf1o 5323	. . . . . . 7 wff g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f
18		vx	. . . . . . . . 9 setvar x
19	18	cv 1394	. . . . . . . 8 class x
20	2	cv 1394	. . . . . . . . 9 class w
21	6, 16	ccom 4727	. . . . . . . . 9 class ( f o. g )
22		cgsu 13333	. . . . . . . . 9 class gsumg
23	20, 21, 22	co 6013	. . . . . . . 8 class ( w gsumg ( f o. g ) )
24	19, 23	wceq 1395	. . . . . . 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 1538	. . . . 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 5282	. . 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 6015	. 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 1395	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  16630