# Metamath Proof Explorer

## Theorem slmdcmn

Description: A semimodule is a commutative monoid. (Contributed by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Assertion slmdcmn ${⊢}{W}\in \mathrm{SLMod}\to {W}\in \mathrm{CMnd}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
2 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
3 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
4 eqid ${⊢}{0}_{{W}}={0}_{{W}}$
5 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
6 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
7 eqid ${⊢}{+}_{\mathrm{Scalar}\left({W}\right)}={+}_{\mathrm{Scalar}\left({W}\right)}$
8 eqid ${⊢}{\cdot }_{\mathrm{Scalar}\left({W}\right)}={\cdot }_{\mathrm{Scalar}\left({W}\right)}$
9 eqid ${⊢}{1}_{\mathrm{Scalar}\left({W}\right)}={1}_{\mathrm{Scalar}\left({W}\right)}$
10 eqid ${⊢}{0}_{\mathrm{Scalar}\left({W}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
11 1 2 3 4 5 6 7 8 9 10 isslmd ${⊢}{W}\in \mathrm{SLMod}↔\left({W}\in \mathrm{CMnd}\wedge \mathrm{Scalar}\left({W}\right)\in \mathrm{SRing}\wedge \forall {w}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\phantom{\rule{.4em}{0ex}}\forall {x}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\left(\left({z}{\cdot }_{{W}}{y}\in {\mathrm{Base}}_{{W}}\wedge {z}{\cdot }_{{W}}\left({y}{+}_{{W}}{x}\right)=\left({z}{\cdot }_{{W}}{y}\right){+}_{{W}}\left({z}{\cdot }_{{W}}{x}\right)\wedge \left({w}{+}_{\mathrm{Scalar}\left({W}\right)}{z}\right){\cdot }_{{W}}{y}=\left({w}{\cdot }_{{W}}{y}\right){+}_{{W}}\left({z}{\cdot }_{{W}}{y}\right)\right)\wedge \left(\left({w}{\cdot }_{\mathrm{Scalar}\left({W}\right)}{z}\right){\cdot }_{{W}}{y}={w}{\cdot }_{{W}}\left({z}{\cdot }_{{W}}{y}\right)\wedge {1}_{\mathrm{Scalar}\left({W}\right)}{\cdot }_{{W}}{y}={y}\wedge {0}_{\mathrm{Scalar}\left({W}\right)}{\cdot }_{{W}}{y}={0}_{{W}}\right)\right)\right)$
12 11 simp1bi ${⊢}{W}\in \mathrm{SLMod}\to {W}\in \mathrm{CMnd}$