Definition df-dim 31010

Description: Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 19912, 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

Step	Hyp	Ref	Expression
1		cldim 31009	. 2 class dim
2		vf	. . 3 setvar 𝑓
3		cvv 3486	. . 3 class V
4		chash 13680	. . . . 5 class ♯
5	2	cv 1536	. . . . . 6 class 𝑓
6		clbs 19829	. . . . . 6 class LBasis
7	5, 6	cfv 6341	. . . . 5 class (LBasis‘𝑓)
8	4, 7	cima 5544	. . . 4 class (♯ “ (LBasis‘𝑓))
9	8	cuni 4824	. . 3 class ∪ (♯ “ (LBasis‘𝑓))
10	2, 3, 9	cmpt 5132	. 2 class (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓)))
11	1, 10	wceq 1537	1 wff dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓)))

This definition is referenced by:  dimval  31011  dimvalfi  31012