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 = ( ℂMod ∩ LVec )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccvs	⊢ ℂVec
1		cclm	⊢ ℂMod
2		clvec	⊢ LVec
3	1 2	cin	⊢ ( ℂMod ∩ LVec )
4	0 3	wceq	⊢ ℂVec = ( ℂMod ∩ LVec )