Theorem gsummptfif1o

Description: Re-index a finite group sum as map, using a bijection. (Contributed by by AV, 23-Jul-2019)

	Ref	Expression
Hypotheses	gsummptcl.b	|- B = ( Base ` G )
	gsummptcl.g	|- ( ph -> G e. CMnd )
	gsummptcl.n	|- ( ph -> N e. Fin )
	gsummptcl.e	|- ( ph -> A. i e. N X e. B )
	gsummptfif1o.f	|- F = ( i e. N |-> X )
	gsummptfif1o.h	|- ( ph -> H : C -1-1-onto-> N )
Assertion	gsummptfif1o	|- ( ph -> ( G gsum F ) = ( G gsum ( F o. H ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptcl.b	|- B = ( Base ` G )
2		gsummptcl.g	|- ( ph -> G e. CMnd )
3		gsummptcl.n	|- ( ph -> N e. Fin )
4		gsummptcl.e	|- ( ph -> A. i e. N X e. B )
5		gsummptfif1o.f	|- F = ( i e. N |-> X )
6		gsummptfif1o.h	|- ( ph -> H : C -1-1-onto-> N )
7		eqid	|- ( 0g ` G ) = ( 0g ` G )
8	5	fmpt	|- ( A. i e. N X e. B <-> F : N --> B )
9	4 8	sylib	|- ( ph -> F : N --> B )
10		fvexd	|- ( ph -> ( 0g ` G ) e. _V )
11	9 3 10	fdmfifsupp	|- ( ph -> F finSupp ( 0g ` G ) )
12	1 7 2 3 9 11 6	gsumf1o	|- ( ph -> ( G gsum F ) = ( G gsum ( F o. H ) ) )