Theorem bj-rvecvec

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

	Ref	Expression
Assertion	bj-rvecvec	⊢ ( 𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec )

Proof

Step	Hyp	Ref	Expression
1		bj-rvecmod	⊢ ( 𝑉 ∈ ℝ-Vec → 𝑉 ∈ LMod )
2		bj-rrdrg	⊢ ℝfld ∈ DivRing
3	2	a1i	⊢ ( 𝑉 ∈ ℝ-Vec → ℝfld ∈ DivRing )
4		bj-rvecrr	⊢ ( 𝑉 ∈ ℝ-Vec → ( Scalar ‘ 𝑉 ) = ℝfld )
5	4	eqcomd	⊢ ( 𝑉 ∈ ℝ-Vec → ℝfld = ( Scalar ‘ 𝑉 ) )
6	5	bj-isvec	⊢ ( 𝑉 ∈ ℝ-Vec → ( 𝑉 ∈ LVec ↔ ( 𝑉 ∈ LMod ∧ ℝfld ∈ DivRing ) ) )
7	1 3 6	mpbir2and	⊢ ( 𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec )