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	|- .0. = ( 0g ` G )
	gsumsubgcl.g	|- ( ph -> G e. Abel )
	gsumsubgcl.a	|- ( ph -> A e. V )
	gsumsubgcl.s	|- ( ph -> S e. ( SubGrp ` G ) )
	gsumsubgcl.f	|- ( ph -> F : A --> S )
	gsumsubgcl.w	|- ( ph -> F finSupp .0. )
Assertion	gsumsubgcl	|- ( ph -> ( G gsum F ) e. S )

Proof

Step	Hyp	Ref	Expression
1		gsumsubgcl.z	|- .0. = ( 0g ` G )
2		gsumsubgcl.g	|- ( ph -> G e. Abel )
3		gsumsubgcl.a	|- ( ph -> A e. V )
4		gsumsubgcl.s	|- ( ph -> S e. ( SubGrp ` G ) )
5		gsumsubgcl.f	|- ( ph -> F : A --> S )
6		gsumsubgcl.w	|- ( ph -> F finSupp .0. )
7		ablcmn	|- ( G e. Abel -> G e. CMnd )
8	2 7	syl	|- ( ph -> G e. CMnd )
9		subgsubm	|- ( S e. ( SubGrp ` G ) -> S e. ( SubMnd ` G ) )
10	4 9	syl	|- ( ph -> S e. ( SubMnd ` G ) )
11	1 8 3 10 5 6	gsumsubmcl	|- ( ph -> ( G gsum F ) e. S )