Theorem phllvec

Description: A pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Assertion	phllvec	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LVec}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
2		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
3		eqid	$$⊢{\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(W\right)$$
4		eqid	$$⊢0_W=0_W$$
5		eqid	$$⊢{\mathrm{*}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{*}}_{\mathrm{Scalar}\left(W\right)}$$
6		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
7	1 2 3 4 5 6	isphl	$$⊢W\in \mathrm{PreHil}\leftrightarrow \left(W\in \mathrm{LVec}\wedge \mathrm{Scalar}\left(W\right)\in \mathrm{*-Ring}\wedge \forall x\in {\mathrm{Base}}_W\left(\left(y\in {\mathrm{Base}}_W⟼y{\cdot }_{𝑖}\left(W\right)x\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left(W\right)\right)\right)\wedge \left(x{\cdot }_{𝑖}\left(W\right)x=0_{\mathrm{Scalar}\left(W\right)}\to x=0_W\right)\wedge \forall y\in {\mathrm{Base}}_W{\left(x{\cdot }_{𝑖}\left(W\right)y\right)}^{{\mathrm{*}}_{\mathrm{Scalar}\left(W\right)}}=y{\cdot }_{𝑖}\left(W\right)x\right)\right)$$
8	7	simp1bi	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LVec}$$