Theorem gsumsubgcl

Description: Closure of a group sum in a subgroup. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by AV, 3-Jun-2019)

	Ref	Expression
Hypotheses	gsumsubgcl.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumsubgcl.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	gsumsubgcl.a	$$⊢\phi \to A\in V$$
	gsumsubgcl.s	$$⊢\phi \to S\in \mathrm{SubGrp}\left(G\right)$$
	gsumsubgcl.f	$$⊢\phi \to F:A⟶S$$
	gsumsubgcl.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	gsumsubgcl	$$⊢\phi \to {\sum }_{G}F\in S$$

Proof

Step	Hyp	Ref	Expression
1		gsumsubgcl.z	$$⊢\underset{\dot{}}{0}=0_G$$
2		gsumsubgcl.g	$$⊢\phi \to G\in \mathrm{Abel}$$
3		gsumsubgcl.a	$$⊢\phi \to A\in V$$
4		gsumsubgcl.s	$$⊢\phi \to S\in \mathrm{SubGrp}\left(G\right)$$
5		gsumsubgcl.f	$$⊢\phi \to F:A⟶S$$
6		gsumsubgcl.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
7		ablcmn	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{CMnd}$$
8	2 7	syl	$$⊢\phi \to G\in \mathrm{CMnd}$$
9		subgsubm	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to S\in \mathrm{SubMnd}\left(G\right)$$
10	4 9	syl	$$⊢\phi \to S\in \mathrm{SubMnd}\left(G\right)$$
11	1 8 3 10 5 6	gsumsubmcl	$$⊢\phi \to {\sum }_{G}F\in S$$