Theorem nlmlmod

Description: A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Assertion	nlmlmod	$$⊢W\in \mathrm{NrmMod}\to W\in \mathrm{LMod}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
2		eqid	$$⊢\mathrm{norm}\left(W\right)=\mathrm{norm}\left(W\right)$$
3		eqid	$$⊢{\cdot }_W={\cdot }_W$$
4		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
5		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
6		eqid	$$⊢\mathrm{norm}\left(\mathrm{Scalar}\left(W\right)\right)=\mathrm{norm}\left(\mathrm{Scalar}\left(W\right)\right)$$
7	1 2 3 4 5 6	isnlm	$$⊢W\in \mathrm{NrmMod}\leftrightarrow \left(\left(W\in \mathrm{NrmGrp}\wedge W\in \mathrm{LMod}\wedge \mathrm{Scalar}\left(W\right)\in \mathrm{NrmRing}\right)\wedge \forall x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall y\in {\mathrm{Base}}_W\mathrm{norm}\left(W\right)\left(x{\cdot }_{W}y\right)=\mathrm{norm}\left(\mathrm{Scalar}\left(W\right)\right)\left(x\right)\mathrm{norm}\left(W\right)\left(y\right)\right)$$
8	7	simplbi	$$⊢W\in \mathrm{NrmMod}\to \left(W\in \mathrm{NrmGrp}\wedge W\in \mathrm{LMod}\wedge \mathrm{Scalar}\left(W\right)\in \mathrm{NrmRing}\right)$$
9	8	simp2d	$$⊢W\in \mathrm{NrmMod}\to W\in \mathrm{LMod}$$