Theorem lmodacl

Description: Closure of ring addition for a left module. (Contributed by NM, 14-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lmodacl.f	|- F = ( Scalar ` W )
	lmodacl.k	|- K = ( Base ` F )
	lmodacl.p	|- .+ = ( +g ` F )
Assertion	lmodacl	|- ( ( W e. LMod /\ X e. K /\ Y e. K ) -> ( X .+ Y ) e. K )

Proof

Step	Hyp	Ref	Expression
1		lmodacl.f	|- F = ( Scalar ` W )
2		lmodacl.k	|- K = ( Base ` F )
3		lmodacl.p	|- .+ = ( +g ` F )
4	1	lmodfgrp	|- ( W e. LMod -> F e. Grp )
5	2 3	grpcl	|- ( ( F e. Grp /\ X e. K /\ Y e. K ) -> ( X .+ Y ) e. K )
6	4 5	syl3an1	|- ( ( W e. LMod /\ X e. K /\ Y e. K ) -> ( X .+ Y ) e. K )