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 ‘ 𝐺 )
	gsumsubgcl.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	gsumsubgcl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsumsubgcl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
	gsumsubgcl.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
	gsumsubgcl.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion	gsumsubgcl	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		gsumsubgcl.z	⊢ 0 = ( 0g ‘ 𝐺 )
2		gsumsubgcl.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
3		gsumsubgcl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		gsumsubgcl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
5		gsumsubgcl.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
6		gsumsubgcl.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
7		ablcmn	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ CMnd )
8	2 7	syl	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
9		subgsubm	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
10	4 9	syl	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
11	1 8 3 10 5 6	gsumsubmcl	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝑆 )