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 e. DivRing /\ I e. W ) -> F e. LVec )

Proof

Step Hyp Ref Expression
1 frlmlvec.1 
 |-  F = ( R freeLMod I )
2 drngring 
 |-  ( R e. DivRing -> R e. Ring )
3 1 frlmlmod 
 |-  ( ( R e. Ring /\ I e. W ) -> F e. LMod )
4 2 3 sylan 
 |-  ( ( R e. DivRing /\ I e. W ) -> F e. LMod )
5 1 frlmsca 
 |-  ( ( R e. DivRing /\ I e. W ) -> R = ( Scalar ` F ) )
6 simpl 
 |-  ( ( R e. DivRing /\ I e. W ) -> R e. DivRing )
7 5 6 eqeltrrd 
 |-  ( ( R e. DivRing /\ I e. W ) -> ( Scalar ` F ) e. DivRing )
8 eqid 
 |-  ( Scalar ` F ) = ( Scalar ` F )
9 8 islvec 
 |-  ( F e. LVec <-> ( F e. LMod /\ ( Scalar ` F ) e. DivRing ) )
10 4 7 9 sylanbrc 
 |-  ( ( R e. DivRing /\ I e. W ) -> F e. LVec )