Metamath Proof Explorer

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 ⊢ F = R freeLMod I
Assertion frlmlvec ⊢ R ∈ DivRing ∧ I ∈ W → F ∈ LVec

Proof

Step Hyp Ref Expression
1 frlmlvec.1 ⊢ F = R freeLMod I
2 drngring ⊢ R ∈ DivRing → R ∈ Ring
3 1 frlmlmod ⊢ R ∈ Ring ∧ I ∈ W → F ∈ LMod
4 2 3 sylan ⊢ R ∈ DivRing ∧ I ∈ W → F ∈ LMod
5 1 frlmsca ⊢ R ∈ DivRing ∧ I ∈ W → R = Scalar ⁡ F
6 simpl ⊢ R ∈ DivRing ∧ I ∈ W → R ∈ DivRing
7 5 6 eqeltrrd ⊢ R ∈ DivRing ∧ I ∈ W → Scalar ⁡ F ∈ DivRing
8 eqid ⊢ Scalar ⁡ F = Scalar ⁡ F
9 8 islvec ⊢ F ∈ LVec ↔ F ∈ LMod ∧ Scalar ⁡ F ∈ DivRing
10 4 7 9 sylanbrc ⊢ R ∈ DivRing ∧ I ∈ W → F ∈ LVec