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

Metamath Proof Explorer

Definition df-cvs

Description: Define the class of subcomplex vector spaces, which are the subcomplex modules which are also vector spaces. (Contributed by Thierry Arnoux, 22-May-2019)

		Ref	Expression
	Assertion	df-cvs	$⊢ ℂVec = CMod \cap LVec$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccvs	$class ℂVec$
1		cclm	$class CMod$
2		clvec	$class LVec$
3	1 2	cin	$class (CMod \cap LVec)$
4	0 3	wceq	$wff ℂVec = CMod \cap LVec$