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 = { 𝑓 ∈ 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 }