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 36169
Description: Definition of the class of real vector spaces. The previous definition, ℝ-Vec = {π‘₯ ∈ LMod ∣ (Scalarβ€˜π‘₯) = ℝfld}, can be recovered using bj-isrvec 36170. 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 36176. (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 36168 . 2 class ℝ-Vec
2 clmod 20470 . . 3 class LMod
3 csca 17199 . . . . 5 class Scalar
43ccnv 5675 . . . 4 class β—‘Scalar
5 crefld 21156 . . . . 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 1541 1 wff ℝ-Vec = (LMod ∩ (β—‘Scalar β€œ {ℝfld}))
Colors of variables: wff setvar class
This definition is referenced by:  bj-isrvec  36170
  Copyright terms: Public domain W3C validator