Theorem slmdsrg

Description: The scalar component of a semimodule is a semiring. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

	Ref	Expression
Hypothesis	slmdsrg.1	$$⊢F=\mathrm{Scalar}\left(W\right)$$
Assertion	slmdsrg	$$⊢W\in \mathrm{SLMod}\to F\in \mathrm{SRing}$$

Proof

Step	Hyp	Ref	Expression
1		slmdsrg.1	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
3		eqid	$$⊢{+}_W={+}_W$$
4		eqid	$$⊢{\cdot }_W={\cdot }_W$$
5		eqid	$$⊢0_W=0_W$$
6		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
7		eqid	$$⊢{+}_F={+}_F$$
8		eqid	$$⊢{\cdot }_F={\cdot }_F$$
9		eqid	$$⊢1_F=1_F$$
10		eqid	$$⊢0_F=0_F$$
11	2 3 4 5 1 6 7 8 9 10	isslmd	$$⊢W\in \mathrm{SLMod}\leftrightarrow \left(W\in \mathrm{CMnd}\wedge F\in \mathrm{SRing}\wedge \forall w\in {\mathrm{Base}}_F\forall z\in {\mathrm{Base}}_F\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{+}_{F}z\right){\cdot }_{W}y=\left(w{\cdot }_{W}y\right){+}_W\left(z{\cdot }_{W}y\right)\right)\wedge \left(\left(w{\cdot }_{F}z\right){\cdot }_{W}y=w{\cdot }_W\left(z{\cdot }_{W}y\right)\wedge 1_F{\cdot }_{W}y=y\wedge 0_F{\cdot }_{W}y=0_W\right)\right)\right)$$
12	11	simp2bi	$$⊢W\in \mathrm{SLMod}\to F\in \mathrm{SRing}$$