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

Proof

Step	Hyp	Ref	Expression
1		gsumsubmcl.z	|- .0. = ( 0g ` G )
2		gsumsubmcl.g	|- ( ph -> G e. CMnd )
3		gsumsubmcl.a	|- ( ph -> A e. V )
4		gsumsubmcl.s	|- ( ph -> S e. ( SubMnd ` G ) )
5		gsumsubmcl.f	|- ( ph -> F : A --> S )
6		gsumsubmcl.w	|- ( ph -> F finSupp .0. )
7		eqid	|- ( Cntz ` G ) = ( Cntz ` G )
8		cmnmnd	|- ( G e. CMnd -> G e. Mnd )
9	2 8	syl	|- ( ph -> G e. Mnd )
10		eqid	|- ( Base ` G ) = ( Base ` G )
11	10	submss	|- ( S e. ( SubMnd ` G ) -> S C_ ( Base ` G ) )
12	4 11	syl	|- ( ph -> S C_ ( Base ` G ) )
13	5 12	fssd	|- ( ph -> F : A --> ( Base ` G ) )
14	10 7 2 13	cntzcmnf	|- ( ph -> ran F C_ ( ( Cntz ` G ) ` ran F ) )
15	1 7 9 3 4 5 14 6	gsumzsubmcl	|- ( ph -> ( G gsum F ) e. S )