This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in V ⟼ ⋃ \|.\| [LBasis (f)])$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cldim	$class \dim$
1		vf	$setvar f$
2		cvv	$class V$
3		chash	$class \|.\|$
4		clbs	$class LBasis$
5	1	cv	$setvar f$
6	5 4	cfv	$class LBasis (f)$
7	3 6	cima	$class \|.\| [LBasis (f)]$
8	7	cuni	$class ⋃ \|.\| [LBasis (f)]$
9	1 2 8	cmpt	$class (f \in V ⟼ ⋃ \|.\| [LBasis (f)])$
10	0 9	wceq	$wff \dim = (f \in V ⟼ ⋃ \|.\| [LBasis (f)])$