Metamath Proof Explorer

Theorem cphnvc

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

Ref Expression
Assertion cphnvc ⊢ W ∈ CPreHil → W ∈ NrmVec

Proof

Step Hyp Ref Expression
1 cphnlm ⊢ W ∈ CPreHil → W ∈ NrmMod
2 cphlvec ⊢ W ∈ CPreHil → W ∈ LVec
3 isnvc ⊢ W ∈ NrmVec ↔ W ∈ NrmMod ∧ W ∈ LVec
4 1 2 3 sylanbrc ⊢ W ∈ CPreHil → W ∈ NrmVec