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