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 36478
Description: Definition of the class of real vector spaces. The previous definition, ℝ-Vec = {π‘₯ ∈ LMod ∣ (Scalarβ€˜π‘₯) = ℝfld}, can be recovered using bj-isrvec 36479. 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 36485. (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 36477 . 2 class ℝ-Vec
2 clmod 20615 . . 3 class LMod
3 csca 17205 . . . . 5 class Scalar
43ccnv 5675 . . . 4 class β—‘Scalar
5 crefld 21377 . . . . 5 class ℝfld
65csn 4628 . . . 4 class {ℝfld}
74, 6cima 5679 . . 3 class (β—‘Scalar β€œ {ℝfld})
82, 7cin 3947 . 2 class (LMod ∩ (β—‘Scalar β€œ {ℝfld}))
91, 8wceq 1540 1 wff ℝ-Vec = (LMod ∩ (β—‘Scalar β€œ {ℝfld}))
Colors of variables: wff setvar class
This definition is referenced by:  bj-isrvec  36479
  Copyright terms: Public domain W3C validator