Metamath Proof Explorer

Theorem hlbn

Description: Every subcomplex Hilbert space is a Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007)

Ref Expression
Assertion hlbn ⊢ W ∈ ℂHil → W ∈ Ban

Proof

Step Hyp Ref Expression
1 ishl ⊢ W ∈ ℂHil ↔ W ∈ Ban ∧ W ∈ CPreHil
2 1 simplbi ⊢ W ∈ ℂHil → W ∈ Ban