Theorem cvslvec

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

	Ref	Expression
Hypothesis	cvslvec.1	|- ( ph -> W e. CVec )
Assertion	cvslvec	|- ( ph -> W e. LVec )

Proof

Step	Hyp	Ref	Expression
1		cvslvec.1	|- ( ph -> W e. CVec )
2		df-cvs	|- CVec = ( CMod i^i LVec )
3	2	elin2	|- ( W e. CVec <-> ( W e. CMod /\ W e. LVec ) )
4	3	simprbi	|- ( W e. CVec -> W e. LVec )
5	1 4	syl	|- ( ph -> W e. LVec )