Theorem gsumf1o

Description: Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016) (Revised by AV, 3-Jun-2019)

	Ref	Expression
Hypotheses	gsumcl.b	$$⊢B={\mathrm{Base}}_G$$
	gsumcl.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumcl.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsumcl.a	$$⊢\phi \to A\in V$$
	gsumcl.f	$$⊢\phi \to F:A⟶B$$
	gsumcl.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
	gsumf1o.h	$$⊢\phi \to H:C\underset{1-1\; onto}{⟶}A$$
Assertion	gsumf1o	$$⊢\phi \to {\sum }_{G}F={\sum }_G\left(F\circ H\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsumcl.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumcl.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsumcl.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsumcl.a	$$⊢\phi \to A\in V$$
5		gsumcl.f	$$⊢\phi \to F:A⟶B$$
6		gsumcl.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
7		gsumf1o.h	$$⊢\phi \to H:C\underset{1-1\; onto}{⟶}A$$
8		eqid	$$⊢\mathrm{Cntz}\left(G\right)=\mathrm{Cntz}\left(G\right)$$
9		cmnmnd	$$⊢G\in \mathrm{CMnd}\to G\in \mathrm{Mnd}$$
10	3 9	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
11	1 8 3 5	cntzcmnf	$$⊢\phi \to \mathrm{ran}F\subseteq \mathrm{Cntz}\left(G\right)\left(\mathrm{ran}F\right)$$
12	1 2 8 10 4 5 11 6 7	gsumzf1o	$$⊢\phi \to {\sum }_{G}F={\sum }_G\left(F\circ H\right)$$