This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hlnvi

Description: Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 6-Jun-2008) (New usage is discouraged.)

Ref Expression
Hypothesis hlnvi.1 ⊢ 𝑈 ∈ CHilOLD
Assertion hlnvi 𝑈 ∈ NrmCVec

Proof

Step Hyp Ref Expression
1 hlnvi.1 ⊢ 𝑈 ∈ CHilOLD
2 hlnv ⊢ ( 𝑈 ∈ CHilOLD → 𝑈 ∈ NrmCVec )
3 1 2 ax-mp ⊢ 𝑈 ∈ NrmCVec