frlmlvec

Description: The free module over a division ring is a left vector space. (Contributed by Steven Nguyen, 29-Apr-2023)

		Ref	Expression
	Hypothesis	frlmlvec.1	$⊢ F = R freeLMod I$
	Assertion	frlmlvec	$⊢ (R \in DivRing \land I \in W) \to F \in LVec$

Step	Hyp	Ref	Expression
1		frlmlvec.1	$⊢ F = R freeLMod I$
2		drngring	$⊢ R \in DivRing \to R \in Ring$
3	1	frlmlmod	$⊢ (R \in Ring \land I \in W) \to F \in LMod$
4	2 3	sylan	$⊢ (R \in DivRing \land I \in W) \to F \in LMod$
5	1	frlmsca	$⊢ (R \in DivRing \land I \in W) \to R = Scalar (F)$
6		simpl	$⊢ (R \in DivRing \land I \in W) \to R \in DivRing$
7	5 6	eqeltrrd	$⊢ (R \in DivRing \land I \in W) \to Scalar (F) \in DivRing$
8		eqid	$⊢ Scalar (F) = Scalar (F)$
9	8	islvec	$⊢ F \in LVec \leftrightarrow (F \in LMod \land Scalar (F) \in DivRing)$
10	4 7 9	sylanbrc	$⊢ (R \in DivRing \land I \in W) \to F \in LVec$

Metamath Proof Explorer