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

Metamath Proof Explorer

Definition df-0v

Description: Define the zero vector in a normed complex vector space. (Contributed by NM, 24-Apr-2007) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-0v	$⊢ 0_{vec} = GId \circ +_{v}$

Step	Hyp	Ref	Expression
0		cn0v	$class 0_{vec}$
1		cgi	$class GId$
2		cpv	$class +_{v}$
3	1 2	ccom	$class (GId \circ +_{v})$
4	0 3	wceq	$wff 0_{vec} = GId \circ +_{v}$