Theorem 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	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
Assertion	frlmlvec	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ LVec )

Proof

Step	Hyp	Ref	Expression
1		frlmlvec.1	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
3	1	frlmlmod	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ LMod )
4	2 3	sylan	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ LMod )
5	1	frlmsca	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊 ) → 𝑅 = ( Scalar ‘ 𝐹 ) )
6		simpl	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ DivRing )
7	5 6	eqeltrrd	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊 ) → ( Scalar ‘ 𝐹 ) ∈ DivRing )
8		eqid	⊢ ( Scalar ‘ 𝐹 ) = ( Scalar ‘ 𝐹 )
9	8	islvec	⊢ ( 𝐹 ∈ LVec ↔ ( 𝐹 ∈ LMod ∧ ( Scalar ‘ 𝐹 ) ∈ DivRing ) )
10	4 7 9	sylanbrc	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ LVec )