Metamath Proof Explorer

Theorem lvecdrng

Description: The set of scalars of a left vector space is a division ring. (Contributed by NM, 17-Apr-2014)

Ref Expression
Hypothesis islvec.1 F = Scalar W
Assertion lvecdrng W LVec F DivRing


Step Hyp Ref Expression
1 islvec.1 F = Scalar W
2 1 islvec W LVec W LMod F DivRing
3 2 simprbi W LVec F DivRing