Definition df-bj-rvec 36477

Description: Definition of the class of real vector spaces. The previous definition, ⊢ ℝ-Vec = {𝑥 ∈ LMod ∣ (Scalar‘𝑥) = ℝ_fld}, can be recovered using bj-isrvec 36478. The present one is preferred since it does not use any dummy variable. That ℝ-Vec could be defined with LVec in place of LMod is a consequence of bj-isrvec2 36484. (Contributed by BJ, 9-Jun-2019.)

Assertion

Ref	Expression
df-bj-rvec	⊢ ℝ-Vec = (LMod ∩ (◡Scalar “ {ℝfld}))

Detailed syntax breakdown of Definition df-bj-rvec

Step	Hyp	Ref	Expression
1		crrvec 36476	. 2 class ℝ-Vec
2		clmod 20614	. . 3 class LMod
3		csca 17204	. . . . 5 class Scalar
4	3	ccnv 5674	. . . 4 class ◡Scalar
5		crefld 21376	. . . . 5 class ℝfld
6	5	csn 4627	. . . 4 class {ℝfld}
7	4, 6	cima 5678	. . 3 class (◡Scalar “ {ℝfld})
8	2, 7	cin 3946	. 2 class (LMod ∩ (◡Scalar “ {ℝfld}))
9	1, 8	wceq 1539	1 wff ℝ-Vec = (LMod ∩ (◡Scalar “ {ℝfld}))

This definition is referenced by:  bj-isrvec  36478