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 = { 𝑓 ∈ LMod ∣ ( Scalar ‘ 𝑓 ) ∈ DivRing }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clvec	⊢ LVec
1		vf	⊢ 𝑓
2		clmod	⊢ LMod
3		csca	⊢ Scalar
4	1	cv	⊢ 𝑓
5	4 3	cfv	⊢ ( Scalar ‘ 𝑓 )
6		cdr	⊢ DivRing
7	5 6	wcel	⊢ ( Scalar ‘ 𝑓 ) ∈ DivRing
8	7 1 2	crab	⊢ { 𝑓 ∈ LMod ∣ ( Scalar ‘ 𝑓 ) ∈ DivRing }
9	0 8	wceq	⊢ LVec = { 𝑓 ∈ LMod ∣ ( Scalar ‘ 𝑓 ) ∈ DivRing }