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 ) |
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 ) |