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

Metamath Proof Explorer

Definition df-lvec

Description: Define the class of all left vector spaces. A left vector space over a division ring is an Abelian group (vectors) together with a division ring (scalars) and a left scalar product connecting them. Some authors call this a "left module over a division ring", reserving "vector space" for those where the division ring is commutative, i.e., is a field. (Contributed by NM, 11-Nov-2013)

		Ref	Expression
	Assertion	df-lvec	$⊢ LVec = \{f \in LMod \| Scalar (f) \in DivRing\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clvec	$class LVec$
1		vf	$setvar f$
2		clmod	$class LMod$
3		csca	$class Scalar$
4	1	cv	$setvar f$
5	4 3	cfv	$class Scalar (f)$
6		cdr	$class DivRing$
7	5 6	wcel	$wff Scalar (f) \in DivRing$
8	7 1 2	crab	$class \{f \in LMod \| Scalar (f) \in DivRing\}$
9	0 8	wceq	$wff LVec = \{f \in LMod \| Scalar (f) \in DivRing\}$