Theorem gsumres

Description: Extend a finite group sum by padding outside with zeroes. (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$$
	gsumres.s	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq W$$
	gsumres.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	gsumres	$$⊢\phi \to {\sum }_G\left({F\upharpoonright }_W\right)={\sum }_{G}F$$

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		gsumres.s	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq W$$
7		gsumres.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
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	gsumzres	$$⊢\phi \to {\sum }_G\left({F\upharpoonright }_W\right)={\sum }_{G}F$$