Theorem hlnv 31051

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

Assertion

Ref	Expression
hlnv	⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ NrmCVec)

Proof of Theorem hlnv

Step	Hyp	Ref	Expression
1		hlobn 31048	. 2 ⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ CBan)
2		bnnv 31026	. 2 ⊢ (𝑈 ∈ CBan → 𝑈 ∈ NrmCVec)
3	1, 2	syl 17	1 ⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ NrmCVec)

Syntax hints:   → wi 4   ∈ wcel 2141  NrmCVeccnv 30744  CBanccbn 31022  CHil_OLDchlo 31045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524  df-cbn 31023  df-hlo 31046

This theorem is referenced by:  hlnvi  31052  hlvc  31053  hladdf  31059  hlcom  31060  hlass  31061  hl0cl  31062  hladdid  31063  hlmulf  31064  hlmulid  31065  hlmulass  31066  hldi  31067  hldir  31068  hlmul0  31069  hlipf  31070  hlipcj  31071  hlipgt0  31074