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