# Metamath Proof Explorer

## 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{Scalar}\left({W}\right)}={*}_{\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}↔\left({W}\in \mathrm{LVec}\wedge \mathrm{Scalar}\left({W}\right)\in \mathrm{*-Ring}\wedge \forall {x}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\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}}\phantom{\rule{.4em}{0ex}}{\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\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}$