Metamath Proof Explorer


Theorem slmdmcl

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 · ˙ = F
Assertion slmdmcl W SLMod X K Y K X · ˙ Y K

Proof

Step Hyp Ref Expression
1 slmdmcl.f F = Scalar W
2 slmdmcl.k K = Base F
3 slmdmcl.t · ˙ = F
4 1 slmdsrg W SLMod F SRing
5 2 3 srgcl F SRing X K Y K X · ˙ Y K
6 4 5 syl3an1 W SLMod X K Y K X · ˙ Y K