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 )