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 RDivRingringLModRLVec

Proof

Step Hyp Ref Expression
1 drngring RDivRingRRing
2 rlmlmod RRingringLModRLMod
3 1 2 syl RDivRingringLModRLMod
4 rlmsca RDivRingR=ScalarringLModR
5 id RDivRingRDivRing
6 4 5 eqeltrrd RDivRingScalarringLModRDivRing
7 eqid ScalarringLModR=ScalarringLModR
8 7 islvec ringLModRLVecringLModRLModScalarringLModRDivRing
9 3 6 8 sylanbrc RDivRingringLModRLVec