Theorem cphlvec

Description: A subcomplex pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Assertion	cphlvec	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ LVec )

Proof

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