Theorem hlnvi 28675

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

Hypothesis

Ref	Expression
hlnvi.1	⊢ 𝑈 ∈ CHilOLD

Assertion

Ref	Expression
hlnvi	⊢ 𝑈 ∈ NrmCVec

Proof of Theorem hlnvi

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

Syntax hints:   ∈ wcel 2111  NrmCVeccnv 28367  CHil_OLDchlo 28668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-cbn 28646  df-hlo 28669

This theorem is referenced by:  htthlem  28700  axhfvadd-zf  28765  axhvcom-zf  28766  axhvass-zf  28767  axhvaddid-zf  28769  axhfvmul-zf  28770  axhvmulid-zf  28771  axhvmulass-zf  28772  axhvdistr1-zf  28773  axhvdistr2-zf  28774  axhvmul0-zf  28775  axhis2-zf  28778  axhis3-zf  28779  axhcompl-zf  28781  hilcompl  28984