Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dim Structured version   Visualization version   GIF version

Definition df-dim 31092
Description: Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 19926, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.)
Assertion
Ref Expression
df-dim dim = (𝑓 ∈ V ↦ (♯ “ (LBasis‘𝑓)))

Detailed syntax breakdown of Definition df-dim
StepHypRef Expression
1 cldim 31091 . 2 class dim
2 vf . . 3 setvar 𝑓
3 cvv 3444 . . 3 class V
4 chash 13690 . . . . 5 class
52cv 1537 . . . . . 6 class 𝑓
6 clbs 19843 . . . . . 6 class LBasis
75, 6cfv 6328 . . . . 5 class (LBasis‘𝑓)
84, 7cima 5526 . . . 4 class (♯ “ (LBasis‘𝑓))
98cuni 4803 . . 3 class (♯ “ (LBasis‘𝑓))
102, 3, 9cmpt 5113 . 2 class (𝑓 ∈ V ↦ (♯ “ (LBasis‘𝑓)))
111, 10wceq 1538 1 wff dim = (𝑓 ∈ V ↦ (♯ “ (LBasis‘𝑓)))
Colors of variables: wff setvar class
This definition is referenced by:  dimval  31093  dimvalfi  31094
  Copyright terms: Public domain W3C validator