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
|- ( ph -> K = ( Scalar ` V ) )
Assertion bj-isvec
|- ( ph -> ( V e. LVec <-> ( V e. LMod /\ K e. DivRing ) ) )

Proof

Step Hyp Ref Expression
1 bj-isvec.scal
 |-  ( ph -> K = ( Scalar ` V ) )
2 eqid
 |-  ( Scalar ` V ) = ( Scalar ` V )
3 2 islvec
 |-  ( V e. LVec <-> ( V e. LMod /\ ( Scalar ` V ) e. DivRing ) )
4 1 eqcomd
 |-  ( ph -> ( Scalar ` V ) = K )
5 4 eleq1d
 |-  ( ph -> ( ( Scalar ` V ) e. DivRing <-> K e. DivRing ) )
6 5 anbi2d
 |-  ( ph -> ( ( V e. LMod /\ ( Scalar ` V ) e. DivRing ) <-> ( V e. LMod /\ K e. DivRing ) ) )
7 3 6 syl5bb
 |-  ( ph -> ( V e. LVec <-> ( V e. LMod /\ K e. DivRing ) ) )