This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hlphl

Description: Every subcomplex Hilbert space is an inner product space (also called a pre-Hilbert space). (Contributed by NM, 28-Apr-2007) (Revised by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion hlphl ⊢ W ∈ ℂHil → W ∈ PreHil

Proof

Step Hyp Ref Expression
1 hlcph ⊢ W ∈ ℂHil → W ∈ CPreHil
2 cphphl ⊢ W ∈ CPreHil → W ∈ PreHil
3 1 2 syl ⊢ W ∈ ℂHil → W ∈ PreHil