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 20429, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.) |
Ref | Expression |
---|---|
df-dim | ⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cldim 31692 | . 2 class dim | |
2 | vf | . . 3 setvar 𝑓 | |
3 | cvv 3429 | . . 3 class V | |
4 | chash 14054 | . . . . 5 class ♯ | |
5 | 2 | cv 1538 | . . . . . 6 class 𝑓 |
6 | clbs 20346 | . . . . . 6 class LBasis | |
7 | 5, 6 | cfv 6426 | . . . . 5 class (LBasis‘𝑓) |
8 | 4, 7 | cima 5587 | . . . 4 class (♯ “ (LBasis‘𝑓)) |
9 | 8 | cuni 4839 | . . 3 class ∪ (♯ “ (LBasis‘𝑓)) |
10 | 2, 3, 9 | cmpt 5156 | . 2 class (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓))) |
11 | 1, 10 | wceq 1539 | 1 wff dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓))) |
Colors of variables: wff setvar class |
This definition is referenced by: dimval 31694 dimvalfi 31695 |
Copyright terms: Public domain | W3C validator |