![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-dim | Structured version Visualization version GIF version |
Description: Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 20663, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.) |
Ref | Expression |
---|---|
df-dim | ⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cldim 32360 | . 2 class dim | |
2 | vf | . . 3 setvar 𝑓 | |
3 | cvv 3447 | . . 3 class V | |
4 | chash 14239 | . . . . 5 class ♯ | |
5 | 2 | cv 1541 | . . . . . 6 class 𝑓 |
6 | clbs 20579 | . . . . . 6 class LBasis | |
7 | 5, 6 | cfv 6500 | . . . . 5 class (LBasis‘𝑓) |
8 | 4, 7 | cima 5640 | . . . 4 class (♯ “ (LBasis‘𝑓)) |
9 | 8 | cuni 4869 | . . 3 class ∪ (♯ “ (LBasis‘𝑓)) |
10 | 2, 3, 9 | cmpt 5192 | . 2 class (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓))) |
11 | 1, 10 | wceq 1542 | 1 wff dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓))) |
Colors of variables: wff setvar class |
This definition is referenced by: dimval 32362 dimvalfi 32363 |
Copyright terms: Public domain | W3C validator |