Metamath Proof Explorer


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 )