Theorem hlnv 30853

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 30850	. 2 ⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ CBan)
2		bnnv 30828	. 2 ⊢ (𝑈 ∈ CBan → 𝑈 ∈ NrmCVec)
3	1, 2	syl 17	1 ⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ NrmCVec)

Syntax hints:   → wi 4   ∈ wcel 2109  NrmCVeccnv 30546  CBanccbn 30824  CHil_OLDchlo 30847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-cbn 30825  df-hlo 30848

This theorem is referenced by:  hlnvi  30854  hlvc  30855  hladdf  30861  hlcom  30862  hlass  30863  hl0cl  30864  hladdid  30865  hlmulf  30866  hlmulid  30867  hlmulass  30868  hldi  30869  hldir  30870  hlmul0  30871  hlipf  30872  hlipcj  30873  hlipgt0  30876