Definition 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 = ( f e. _V |-> U. ( # " ( LBasis ` f ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cldim	|- dim
1		vf	|- f
2		cvv	|- _V
3		chash	|- #
4		clbs	|- LBasis
5	1	cv	|- f
6	5 4	cfv	|- ( LBasis ` f )
7	3 6	cima	|- ( # " ( LBasis ` f ) )
8	7	cuni	|- U. ( # " ( LBasis ` f ) )
9	1 2 8	cmpt	|- ( f e. _V |-> U. ( # " ( LBasis ` f ) ) )
10	0 9	wceq	|- dim = ( f e. _V |-> U. ( # " ( LBasis ` f ) ) )