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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	lvecdrng	⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing )

Proof

Step	Hyp	Ref	Expression
1		islvec.1	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2	1	islvec	⊢ ( 𝑊 ∈ LVec ↔ ( 𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing ) )
3	2	simprbi	⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing )