Metamath Proof Explorer


Theorem bj-isrvec2

Description: The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024)

Ref Expression
Hypothesis bj-isrvec2.scal φ Scalar V = K
Assertion bj-isrvec2 φ V ℝVec V LVec K = fld

Proof

Step Hyp Ref Expression
1 bj-isrvec2.scal φ Scalar V = K
2 bj-rvecvec V ℝVec V LVec
3 2 a1i φ V ℝVec V LVec
4 bj-rvecrr V ℝVec Scalar V = fld
5 1 eqeq1d φ Scalar V = fld K = fld
6 4 5 syl5ib φ V ℝVec K = fld
7 3 6 jcad φ V ℝVec V LVec K = fld
8 bj-vecssmodel V LVec V LMod
9 8 anim1i V LVec K = fld V LMod K = fld
10 1 bj-isrvecd φ V ℝVec V LMod K = fld
11 9 10 syl5ibr φ V LVec K = fld V ℝVec
12 7 11 impbid φ V ℝVec V LVec K = fld