Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Algebra
Semiring left modules
slmdmcl
Metamath Proof Explorer
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