Metamath Proof Explorer

Theorem bj-rvecvec

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

Ref Expression
Assertion bj-rvecvec ⊢ V ∈ ℝVec → V ∈ LVec

Proof

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