Metamath Proof Explorer

Theorem bj-isrvec

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

Ref Expression
Assertion bj-isrvec 
|- ( V e. RRVec <-> ( V e. LMod /\ ( Scalar ` V ) = RRfld ) )

Proof

Step Hyp Ref Expression
1 df-bj-rvec 
 |-  RRVec = ( LMod i^i ( `' Scalar " { RRfld } ) )
2 1 elin2 
 |-  ( V e. RRVec <-> ( V e. LMod /\ V e. ( `' Scalar " { RRfld } ) ) )
3 bj-evalfun 
 |-  Fun Slot 5
4 df-sca 
 |-  Scalar = Slot 5
5 4 funeqi 
 |-  ( Fun Scalar <-> Fun Slot 5 )
6 3 5 mpbir 
 |-  Fun Scalar
7 0re 
 |-  0 e. RR
8 7 n0ii 
 |-  -. RR = (/)
9 eqcom 
 |-  ( (/) = RR <-> RR = (/) )
10 8 9 mtbir 
 |-  -. (/) = RR
11 fveq2 
 |-  ( (/) = RRfld -> ( Base ` (/) ) = ( Base ` RRfld ) )
12 base0 
 |-  (/) = ( Base ` (/) )
13 rebase 
 |-  RR = ( Base ` RRfld )
14 11 12 13 3eqtr4g 
 |-  ( (/) = RRfld -> (/) = RR )
15 10 14 mto 
 |-  -. (/) = RRfld
16 elsni 
 |-  ( (/) e. { RRfld } -> (/) = RRfld )
17 15 16 mto 
 |-  -. (/) e. { RRfld }
18 bj-fvimacnv0 
 |-  ( ( Fun Scalar /\ -. (/) e. { RRfld } ) -> ( ( Scalar ` V ) e. { RRfld } <-> V e. ( `' Scalar " { RRfld } ) ) )
19 6 17 18 mp2an 
 |-  ( ( Scalar ` V ) e. { RRfld } <-> V e. ( `' Scalar " { RRfld } ) )
20 fvex 
 |-  ( Scalar ` V ) e. _V
21 20 elsn 
 |-  ( ( Scalar ` V ) e. { RRfld } <-> ( Scalar ` V ) = RRfld )
22 19 21 bitr3i 
 |-  ( V e. ( `' Scalar " { RRfld } ) <-> ( Scalar ` V ) = RRfld )
23 22 anbi2i 
 |-  ( ( V e. LMod /\ V e. ( `' Scalar " { RRfld } ) ) <-> ( V e. LMod /\ ( Scalar ` V ) = RRfld ) )
24 2 23 bitri 
 |-  ( V e. RRVec <-> ( V e. LMod /\ ( Scalar ` V ) = RRfld ) )