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