Theorem bj-rvecmod

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

	Ref	Expression
Assertion	bj-rvecmod	⊢ ( 𝑉 ∈ ℝ-Vec → 𝑉 ∈ LMod )

Proof

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