Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-rvec Structured version   Visualization version   GIF version

Definition df-bj-rvec 35472
Description: Definition of the class of real vector spaces. The previous definition, ℝ-Vec = {𝑥 ∈ LMod ∣ (Scalar‘𝑥) = ℝfld}, can be recovered using bj-isrvec 35473. 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 35479. (Contributed by BJ, 9-Jun-2019.)
Assertion
Ref Expression
df-bj-rvec ℝ-Vec = (LMod ∩ (Scalar “ {ℝfld}))

Detailed syntax breakdown of Definition df-bj-rvec
StepHypRef Expression
1 crrvec 35471 . 2 class ℝ-Vec
2 clmod 20133 . . 3 class LMod
3 csca 16975 . . . . 5 class Scalar
43ccnv 5583 . . . 4 class Scalar
5 crefld 20819 . . . . 5 class fld
65csn 4561 . . . 4 class {ℝfld}
74, 6cima 5587 . . 3 class (Scalar “ {ℝfld})
82, 7cin 3885 . 2 class (LMod ∩ (Scalar “ {ℝfld}))
91, 8wceq 1539 1 wff ℝ-Vec = (LMod ∩ (Scalar “ {ℝfld}))
Colors of variables: wff setvar class
This definition is referenced by:  bj-isrvec  35473
  Copyright terms: Public domain W3C validator