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 WCPreHilWNrmVec

Proof

Step Hyp Ref Expression
1 cphnlm WCPreHilWNrmMod
2 cphlvec WCPreHilWLVec
3 isnvc WNrmVecWNrmModWLVec
4 1 2 3 sylanbrc WCPreHilWNrmVec