Theorem lmodmcl

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

	Ref	Expression
Hypotheses	lmodmcl.f	|- F = ( Scalar ` W )
	lmodmcl.k	|- K = ( Base ` F )
	lmodmcl.t	|- .x. = ( .r ` F )
Assertion	lmodmcl	|- ( ( W e. LMod /\ X e. K /\ Y e. K ) -> ( X .x. Y ) e. K )

Proof

Step	Hyp	Ref	Expression
1		lmodmcl.f	|- F = ( Scalar ` W )
2		lmodmcl.k	|- K = ( Base ` F )
3		lmodmcl.t	|- .x. = ( .r ` F )
4	1	lmodring	|- ( W e. LMod -> F e. Ring )
5	2 3	ringcl	|- ( ( F e. Ring /\ X e. K /\ Y e. K ) -> ( X .x. Y ) e. K )
6	4 5	syl3an1	|- ( ( W e. LMod /\ X e. K /\ Y e. K ) -> ( X .x. Y ) e. K )