Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Algebra
Semiring left modules
slmdmnd
Next ⟩
slmdsrg
Metamath Proof Explorer
Ascii
Unicode
Theorem
slmdmnd
Description:
A semimodule is a monoid.
(Contributed by
Thierry Arnoux
, 1-Apr-2018)
Ref
Expression
Assertion
slmdmnd
⊢
W
∈
SLMod
→
W
∈
Mnd
Proof
Step
Hyp
Ref
Expression
1
slmdcmn
⊢
W
∈
SLMod
→
W
∈
CMnd
2
cmnmnd
⊢
W
∈
CMnd
→
W
∈
Mnd
3
1
2
syl
⊢
W
∈
SLMod
→
W
∈
Mnd