Metamath Proof Explorer


Theorem bj-isrvecd

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

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

Proof

Step Hyp Ref Expression
1 bj-isrvecd.scal φ Scalar V = K
2 bj-isrvec V ℝVec V LMod Scalar V = fld
3 1 eqeq1d φ Scalar V = fld K = fld
4 3 anbi2d φ V LMod Scalar V = fld V LMod K = fld
5 2 4 syl5bb φ V ℝVec V LMod K = fld