Theorem lmodring

Description: The scalar component of a left module is a ring. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypothesis	lmodring.1	$$⊢F=\mathrm{Scalar}\left(W\right)$$
Assertion	lmodring	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		lmodring.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	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
6		eqid	$$⊢{+}_F={+}_F$$
7		eqid	$$⊢{\cdot }_F={\cdot }_F$$
8		eqid	$$⊢1_F=1_F$$
9	2 3 4 1 5 6 7 8	islmod	$$⊢W\in \mathrm{LMod}\leftrightarrow \left(W\in \mathrm{Grp}\wedge F\in \mathrm{Ring}\wedge \forall q\in {\mathrm{Base}}_F\forall r\in {\mathrm{Base}}_F\forall x\in {\mathrm{Base}}_W\forall w\in {\mathrm{Base}}_W\left(\left(r{\cdot }_{W}w\in {\mathrm{Base}}_W\wedge r{\cdot }_W\left(w{+}_{W}x\right)=\left(r{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}x\right)\wedge \left(q{+}_{F}r\right){\cdot }_{W}w=\left(q{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}w\right)\right)\wedge \left(\left(q{\cdot }_{F}r\right){\cdot }_{W}w=q{\cdot }_W\left(r{\cdot }_{W}w\right)\wedge 1_F{\cdot }_{W}w=w\right)\right)\right)$$
10	9	simp2bi	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Ring}$$