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	⊢ 0vec = ( GId ∘ +𝑣 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cn0v	⊢ 0vec
1		cgi	⊢ GId
2		cpv	⊢ +𝑣
3	1 2	ccom	⊢ ( GId ∘ +𝑣 )
4	0 3	wceq	⊢ 0vec = ( GId ∘ +𝑣 )