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={\mathrm{Base}}_G$$
	gsummptcl.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsummptcl.n	$$⊢\phi \to N\in \mathrm{Fin}$$
	gsummptcl.e	$$⊢\phi \to \forall i\in NX\in B$$
	gsummptfif1o.f	$$⊢F=\left(i\in N⟼X\right)$$
	gsummptfif1o.h	$$⊢\phi \to H:C\underset{1-1\; onto}{⟶}N$$
Assertion	gsummptfif1o	$$⊢\phi \to {\sum }_{G}F={\sum }_G\left(F\circ H\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsummptcl.b	$$⊢B={\mathrm{Base}}_G$$
2		gsummptcl.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
3		gsummptcl.n	$$⊢\phi \to N\in \mathrm{Fin}$$
4		gsummptcl.e	$$⊢\phi \to \forall i\in NX\in B$$
5		gsummptfif1o.f	$$⊢F=\left(i\in N⟼X\right)$$
6		gsummptfif1o.h	$$⊢\phi \to H:C\underset{1-1\; onto}{⟶}N$$
7		eqid	$$⊢0_G=0_G$$
8	5	fmpt	$$⊢\forall i\in NX\in B\leftrightarrow F:N⟶B$$
9	4 8	sylib	$$⊢\phi \to F:N⟶B$$
10		fvexd	$$⊢\phi \to 0_G\in \mathrm{V}$$
11	9 3 10	fdmfifsupp	$$⊢\phi \to {finSupp}_{0_G}\left(F\right)$$
12	1 7 2 3 9 11 6	gsumf1o	$$⊢\phi \to {\sum }_{G}F={\sum }_G\left(F\circ H\right)$$