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	⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ PreHil )

Proof

Step	Hyp	Ref	Expression
1		hlcph	⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ ℂPreHil )
2		cphphl	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
3	1 2	syl	⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ PreHil )