Metamath Proof Explorer


Theorem bj-isvec

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

Ref Expression
Hypothesis bj-isvec.scal φ K = Scalar V
Assertion bj-isvec φ V LVec V LMod K DivRing

Proof

Step Hyp Ref Expression
1 bj-isvec.scal φ K = Scalar V
2 eqid Scalar V = Scalar V
3 2 islvec V LVec V LMod Scalar V DivRing
4 1 eqcomd φ Scalar V = K
5 4 eleq1d φ Scalar V DivRing K DivRing
6 5 anbi2d φ V LMod Scalar V DivRing V LMod K DivRing
7 3 6 syl5bb φ V LVec V LMod K DivRing