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	⊢ ( 𝑉 ∈ ℝ-Vec → ( Scalar ‘ 𝑉 ) = ℝfld )

Proof

Step	Hyp	Ref	Expression
1		bj-isrvec	⊢ ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) = ℝfld ) )
2	1	simprbi	⊢ ( 𝑉 ∈ ℝ-Vec → ( Scalar ‘ 𝑉 ) = ℝfld )