Metamath Proof Explorer

Theorem 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 ∈ DivRing → ringLMod ⁡ R ∈ LVec

Proof

Step Hyp Ref Expression
1 drngring ⊢ R ∈ DivRing → R ∈ Ring
2 rlmlmod ⊢ R ∈ Ring → ringLMod ⁡ R ∈ LMod
3 1 2 syl ⊢ R ∈ DivRing → ringLMod ⁡ R ∈ LMod
4 rlmsca ⊢ R ∈ DivRing → R = Scalar ⁡ ringLMod ⁡ R
5 id ⊢ R ∈ DivRing → R ∈ DivRing
6 4 5 eqeltrrd ⊢ R ∈ DivRing → Scalar ⁡ ringLMod ⁡ R ∈ DivRing
7 eqid ⊢ Scalar ⁡ ringLMod ⁡ R = Scalar ⁡ ringLMod ⁡ R
8 7 islvec ⊢ ringLMod ⁡ R ∈ LVec ↔ ringLMod ⁡ R ∈ LMod ∧ Scalar ⁡ ringLMod ⁡ R ∈ DivRing
9 3 6 8 sylanbrc ⊢ R ∈ DivRing → ringLMod ⁡ R ∈ LVec