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 ℝVec Scalar V = fld

Proof

Step Hyp Ref Expression
1 bj-isrvec V ℝVec V LMod Scalar V = fld
2 1 simprbi V ℝVec Scalar V = fld