Theorem cvsclm

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

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

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	simplbi	|- ( W e. CVec -> W e. CMod )
5	1 4	syl	|- ( ph -> W e. CMod )