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 “ { ℝfld } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrvec	⊢ ℝ-Vec
1		clmod	⊢ LMod
2		csca	⊢ Scalar
3	2	ccnv	⊢ ◡ Scalar
4		crefld	⊢ ℝfld
5	4	csn	⊢ { ℝfld }
6	3 5	cima	⊢ ( ◡ Scalar “ { ℝfld } )
7	1 6	cin	⊢ ( LMod ∩ ( ◡ Scalar “ { ℝfld } ) )
8	0 7	wceq	⊢ ℝ-Vec = ( LMod ∩ ( ◡ Scalar “ { ℝfld } ) )