Metamath Proof Explorer

Theorem cphlvec

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

Ref Expression
Assertion cphlvec ⊢W∈CPreHil→W∈LVec

Proof

Step Hyp Ref Expression
1 cphphl ⊢W∈CPreHil→W∈PreHil
2 phllvec ⊢W∈PreHil→W∈LVec
3 1 2 syl ⊢W∈CPreHil→W∈LVec