Theorem gsumcl

Description: Closure of a finite group sum. (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)$$
Assertion	gsumcl	$$⊢\phi \to {\sum }_{G}F\in B$$

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	6	fsuppimpd	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
8	1 2 3 4 5 7	gsumcl2	$$⊢\phi \to {\sum }_{G}F\in B$$