Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-rvec | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-bj-rvec | ⊢ ℝ-Vec = (LMod ∩ (◡Scalar “ {ℝfld})) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crrvec 35471 | . 2 class ℝ-Vec | |
2 | clmod 20133 | . . 3 class LMod | |
3 | csca 16975 | . . . . 5 class Scalar | |
4 | 3 | ccnv 5583 | . . . 4 class ◡Scalar |
5 | crefld 20819 | . . . . 5 class ℝfld | |
6 | 5 | csn 4561 | . . . 4 class {ℝfld} |
7 | 4, 6 | cima 5587 | . . 3 class (◡Scalar “ {ℝfld}) |
8 | 2, 7 | cin 3885 | . 2 class (LMod ∩ (◡Scalar “ {ℝfld})) |
9 | 1, 8 | wceq 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 |