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 ℝVec = LMod Scalar -1 fld

Detailed syntax breakdown

Step Hyp Ref Expression
0 crrvec class ℝVec
1 clmod class LMod
2 csca class Scalar
3 2 ccnv class Scalar -1
4 crefld class fld
5 4 csn class fld
6 3 5 cima class Scalar -1 fld
7 1 6 cin class LMod Scalar -1 fld
8 0 7 wceq wff ℝVec = LMod Scalar -1 fld