This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in LVec \to F \in DivRing$

Step	Hyp	Ref	Expression
1		islvec.1	$⊢ F = Scalar (W)$
2	1	islvec	$⊢ W \in LVec \leftrightarrow (W \in LMod \land F \in DivRing)$
3	2	simprbi	$⊢ W \in LVec \to F \in DivRing$