Metamath Proof Explorer

Definition df-bj-rvec

Description: Definition of the class of real vector spaces. The previous definition, |- RRVec = { x e. LMod | ( Scalarx ) = RRfld } , can be recovered using bj-isrvec . The present one is preferred since it does not use any dummy variable. That RRVec could be defined with LVec in place of LMod is a consequence of bj-isrvec2 . (Contributed by BJ, 9-Jun-2019)

Ref Expression
Assertion df-bj-rvec 
|- RRVec = ( LMod i^i ( `' Scalar " { RRfld } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crrvec 
 |-  RRVec
1 clmod 
 |-  LMod
2 csca 
 |-  Scalar
3 2 ccnv 
 |-  `' Scalar
4 crefld 
 |-  RRfld
5 4 csn 
 |-  { RRfld }
6 3 5 cima 
 |-  ( `' Scalar " { RRfld } )
7 1 6 cin 
 |-  ( LMod i^i ( `' Scalar " { RRfld } ) )
8 0 7 wceq 
 |-  RRVec = ( LMod i^i ( `' Scalar " { RRfld } ) )