Metamath Proof Explorer

Theorem bj-rvecmod

Description: Real vector spaces are modules (elemental version). (Contributed by BJ, 6-Jan-2024)

Ref Expression
Assertion bj-rvecmod 
|- ( V e. RRVec -> V e. LMod )

Proof

Step Hyp Ref Expression
1 bj-isrvec 
 |-  ( V e. RRVec <-> ( V e. LMod /\ ( Scalar ` V ) = RRfld ) )
2 1 simplbi 
 |-  ( V e. RRVec -> V e. LMod )