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