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}\leftrightarrow \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)}\forall z\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall x\in {\mathrm{Base}}_W\forall y\in {\mathrm{Base}}_W\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}$$