Metamath Proof Explorer

Theorem bj-rvecrr

Description: The field of scalars of a real vector space is the field of real numbers. (Contributed by BJ, 6-Jan-2024)

Ref Expression
Assertion bj-rvecrr 
|- ( V e. RRVec -> ( Scalar ` V ) = RRfld )

Proof

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