Metamath Proof Explorer

Theorem hlnv

Description: Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 17-Mar-2007) (New usage is discouraged.)

Ref Expression
Assertion hlnv 
|- ( U e. CHilOLD -> U e. NrmCVec )

Proof

Step Hyp Ref Expression
1 hlobn 
 |-  ( U e. CHilOLD -> U e. CBan )
2 bnnv 
 |-  ( U e. CBan -> U e. NrmCVec )
3 1 2 syl 
 |-  ( U e. CHilOLD -> U e. NrmCVec )