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	$$⊢\mathrm{ℝVec}=\mathrm{LMod}\cap {\mathrm{Scalar}}^{-1}\left[\left\{{ℝ}_{\mathrm{fld}}\right\}\right]$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrvec	$$class\mathrm{ℝVec}$$
1		clmod	$$class\mathrm{LMod}$$
2		csca	$$class\mathrm{Scalar}$$
3	2	ccnv	$$class{\mathrm{Scalar}}^{-1}$$
4		crefld	$$class{ℝ}_{\mathrm{fld}}$$
5	4	csn	$$class\left\{{ℝ}_{\mathrm{fld}}\right\}$$
6	3 5	cima	$$class{\mathrm{Scalar}}^{-1}\left[\left\{{ℝ}_{\mathrm{fld}}\right\}\right]$$
7	1 6	cin	$$class\left(\mathrm{LMod}\cap {\mathrm{Scalar}}^{-1}\left[\left\{{ℝ}_{\mathrm{fld}}\right\}\right]\right)$$
8	0 7	wceq	$$wff\mathrm{ℝVec}=\mathrm{LMod}\cap {\mathrm{Scalar}}^{-1}\left[\left\{{ℝ}_{\mathrm{fld}}\right\}\right]$$