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 ⊢W∈ℂHil→W∈CPreHil

Proof

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