This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Thierry Arnoux Algebra Vector Space Dimension df-dim
Description: Define the dimension of a vector space as the cardinality of its bases.
Note that by lvecdim , all bases are equinumerous. (Contributed by Thierry Arnoux , 6-May-2023)
Ref
Expression
Assertion
df-dim ⊢ dim = ( 𝑓 ∈ V ↦ ∪ ( ♯ “ ( LBasis ‘ 𝑓 ) ) )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cldim ⊢ dim
1
vf ⊢ 𝑓
2
cvv ⊢ V
3
chash ⊢ ♯
4
clbs ⊢ LBasis
5
1
cv ⊢ 𝑓
6
5 4
cfv ⊢ ( LBasis ‘ 𝑓 )
7
3 6
cima ⊢ ( ♯ “ ( LBasis ‘ 𝑓 ) )
8
7
cuni ⊢ ∪ ( ♯ “ ( LBasis ‘ 𝑓 ) )
9
1 2 8
cmpt ⊢ ( 𝑓 ∈ V ↦ ∪ ( ♯ “ ( LBasis ‘ 𝑓 ) ) )
10
0 9
wceq ⊢ dim = ( 𝑓 ∈ V ↦ ∪ ( ♯ “ ( LBasis ‘ 𝑓 ) ) )