Definition df-vs

Description: Define vector subtraction on a normed complex vector space. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	df-vs	⊢ −𝑣 = ( /𝑔 ∘ +𝑣 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnsb	⊢ −𝑣
1		cgs	⊢ /𝑔
2		cpv	⊢ +𝑣
3	1 2	ccom	⊢ ( /𝑔 ∘ +𝑣 )
4	0 3	wceq	⊢ −𝑣 = ( /𝑔 ∘ +𝑣 )