Theorem cvslvec

Description: A subcomplex vector space is a (left) vector space. (Contributed by Thierry Arnoux, 22-May-2019)

	Ref	Expression
Hypothesis	cvslvec.1	⊢ ( 𝜑 → 𝑊 ∈ ℂVec )
Assertion	cvslvec	⊢ ( 𝜑 → 𝑊 ∈ LVec )

Proof

Step	Hyp	Ref	Expression
1		cvslvec.1	⊢ ( 𝜑 → 𝑊 ∈ ℂVec )
2		df-cvs	⊢ ℂVec = ( ℂMod ∩ LVec )
3	2	elin2	⊢ ( 𝑊 ∈ ℂVec ↔ ( 𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec ) )
4	3	simprbi	⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ LVec )
5	1 4	syl	⊢ ( 𝜑 → 𝑊 ∈ LVec )