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 e. LVec -> F e. DivRing )

Proof

Step Hyp Ref Expression
1 islvec.1 
 |-  F = ( Scalar ` W )
2 1 islvec 
 |-  ( W e. LVec <-> ( W e. LMod /\ F e. DivRing ) )
3 2 simprbi 
 |-  ( W e. LVec -> F e. DivRing )