This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cvslvec

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

		Ref	Expression
	Hypothesis	cvslvec.1	$⊢ φ \to W \in ℂVec$
	Assertion	cvslvec	$⊢ φ \to W \in LVec$

Step	Hyp	Ref	Expression
1		cvslvec.1	$⊢ φ \to W \in ℂVec$
2		df-cvs	$⊢ ℂVec = CMod \cap LVec$
3	2	elin2	$⊢ W \in ℂVec \leftrightarrow (W \in CMod \land W \in LVec)$
4	3	simprbi	$⊢ W \in ℂVec \to W \in LVec$
5	1 4	syl	$⊢ φ \to W \in LVec$