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_{\mathrm{vec}}=\mathrm{GId}\circ {+}_v$$

Detailed syntax breakdown

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