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\in \mathrm{ℂHil}\to W\in \mathrm{PreHil}$$

Proof

Step	Hyp	Ref	Expression
1		hlcph	$$⊢W\in \mathrm{ℂHil}\to W\in \mathrm{CPreHil}$$
2		cphphl	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{PreHil}$$
3	1 2	syl	$$⊢W\in \mathrm{ℂHil}\to W\in \mathrm{PreHil}$$