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 
|- ( ph -> ( Scalar ` V ) = K )
Assertion bj-isrvec2 
|- ( ph -> ( V e. RRVec <-> ( V e. LVec /\ K = RRfld ) ) )

Proof

Step Hyp Ref Expression
1 bj-isrvec2.scal 
 |-  ( ph -> ( Scalar ` V ) = K )
2 bj-rvecvec 
 |-  ( V e. RRVec -> V e. LVec )
3 2 a1i 
 |-  ( ph -> ( V e. RRVec -> V e. LVec ) )
4 bj-rvecrr 
 |-  ( V e. RRVec -> ( Scalar ` V ) = RRfld )
5 1 eqeq1d 
 |-  ( ph -> ( ( Scalar ` V ) = RRfld <-> K = RRfld ) )
6 4 5 syl5ib 
 |-  ( ph -> ( V e. RRVec -> K = RRfld ) )
7 3 6 jcad 
 |-  ( ph -> ( V e. RRVec -> ( V e. LVec /\ K = RRfld ) ) )
8 bj-vecssmodel 
 |-  ( V e. LVec -> V e. LMod )
9 8 anim1i 
 |-  ( ( V e. LVec /\ K = RRfld ) -> ( V e. LMod /\ K = RRfld ) )
10 1 bj-isrvecd 
 |-  ( ph -> ( V e. RRVec <-> ( V e. LMod /\ K = RRfld ) ) )
11 9 10 syl5ibr 
 |-  ( ph -> ( ( V e. LVec /\ K = RRfld ) -> V e. RRVec ) )
12 7 11 impbid 
 |-  ( ph -> ( V e. RRVec <-> ( V e. LVec /\ K = RRfld ) ) )