Description: Closure of ring multiplication for a semimodule. (Contributed by NM, 14-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | slmdmcl.f | |- F = ( Scalar ` W ) |
|
| slmdmcl.k | |- K = ( Base ` F ) |
||
| slmdmcl.t | |- .x. = ( .r ` F ) |
||
| Assertion | slmdmcl | |- ( ( W e. SLMod /\ X e. K /\ Y e. K ) -> ( X .x. Y ) e. K ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | slmdmcl.f | |- F = ( Scalar ` W ) |
|
| 2 | slmdmcl.k | |- K = ( Base ` F ) |
|
| 3 | slmdmcl.t | |- .x. = ( .r ` F ) |
|
| 4 | 1 | slmdsrg | |- ( W e. SLMod -> F e. SRing ) |
| 5 | 2 3 | srgcl | |- ( ( F e. SRing /\ X e. K /\ Y e. K ) -> ( X .x. Y ) e. K ) |
| 6 | 4 5 | syl3an1 | |- ( ( W e. SLMod /\ X e. K /\ Y e. K ) -> ( X .x. Y ) e. K ) |