Theorem gsumsubmcl

Description: Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015) (Revised by Mario Carneiro, 24-Apr-2016) (Revised by AV, 3-Jun-2019)

	Ref	Expression
Hypotheses	gsumsubmcl.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsumsubmcl.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsumsubmcl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsumsubmcl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
	gsumsubmcl.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
	gsumsubmcl.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion	gsumsubmcl	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		gsumsubmcl.z	⊢ 0 = ( 0g ‘ 𝐺 )
2		gsumsubmcl.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
3		gsumsubmcl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		gsumsubmcl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
5		gsumsubmcl.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
6		gsumsubmcl.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
7		eqid	⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
8		cmnmnd	⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
9	2 8	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
10		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
11	10	submss	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
12	4 11	syl	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
13	5 12	fssd	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( Base ‘ 𝐺 ) )
14	10 7 2 13	cntzcmnf	⊢ ( 𝜑 → ran 𝐹 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐹 ) )
15	1 7 9 3 4 5 14 6	gsumzsubmcl	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝑆 )