![]() |
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 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.) |
Ref | Expression |
---|---|
df-bj-rvec | β’ β-Vec = (LMod β© (β‘Scalar β {βfld})) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crrvec 36168 | . 2 class β-Vec | |
2 | clmod 20470 | . . 3 class LMod | |
3 | csca 17199 | . . . . 5 class Scalar | |
4 | 3 | ccnv 5675 | . . . 4 class β‘Scalar |
5 | crefld 21156 | . . . . 5 class βfld | |
6 | 5 | csn 4628 | . . . 4 class {βfld} |
7 | 4, 6 | cima 5679 | . . 3 class (β‘Scalar β {βfld}) |
8 | 2, 7 | cin 3947 | . 2 class (LMod β© (β‘Scalar β {βfld})) |
9 | 1, 8 | wceq 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 |