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