Metamath Proof Explorer

Theorem hlcph

Description: Every subcomplex Hilbert space is a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion hlcph ( π‘Š ∈ β„‚Hil β†’ π‘Š ∈ β„‚PreHil )

Proof

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