rlmlvec

Description: The ring module over a division ring is a vector space. (Contributed by Mario Carneiro, 4-Oct-2015)

		Ref	Expression
	Assertion	rlmlvec	$⊢ R \in DivRing \to ringLMod (R) \in LVec$

Step	Hyp	Ref	Expression
1		drngring	$⊢ R \in DivRing \to R \in Ring$
2		rlmlmod	$⊢ R \in Ring \to ringLMod (R) \in LMod$
3	1 2	syl	$⊢ R \in DivRing \to ringLMod (R) \in LMod$
4		rlmsca	$⊢ R \in DivRing \to R = Scalar (ringLMod (R))$
5		id	$⊢ R \in DivRing \to R \in DivRing$
6	4 5	eqeltrrd	$⊢ R \in DivRing \to Scalar (ringLMod (R)) \in DivRing$
7		eqid	$⊢ Scalar (ringLMod (R)) = Scalar (ringLMod (R))$
8	7	islvec	$⊢ ringLMod (R) \in LVec \leftrightarrow (ringLMod (R) \in LMod \land Scalar (ringLMod (R)) \in DivRing)$
9	3 6 8	sylanbrc	$⊢ R \in DivRing \to ringLMod (R) \in LVec$

Metamath Proof Explorer