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	$$⊢\mathrm{LVec}=\left\{f\in \mathrm{LMod}|\mathrm{Scalar}\left(f\right)\in \mathrm{DivRing}\right\}$$

Detailed syntax breakdown

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