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 ( π‘Š ∈ β„‚Hil β†’ π‘Š ∈ Ban )

Proof

Step Hyp Ref Expression
1 ishl ⊒ ( π‘Š ∈ β„‚Hil ↔ ( π‘Š ∈ Ban ∧ π‘Š ∈ β„‚PreHil ) )
2 1 simplbi ⊒ ( π‘Š ∈ β„‚Hil β†’ π‘Š ∈ Ban )