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=\mathrm{Scalar}\left(W\right)$$
Assertion	lvecdrng	$$⊢W\in \mathrm{LVec}\to F\in \mathrm{DivRing}$$

Proof

Step	Hyp	Ref	Expression
1		islvec.1	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2	1	islvec	$$⊢W\in \mathrm{LVec}\leftrightarrow \left(W\in \mathrm{LMod}\wedge F\in \mathrm{DivRing}\right)$$
3	2	simprbi	$$⊢W\in \mathrm{LVec}\to F\in \mathrm{DivRing}$$