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	$$⊢{-}_v={/}_g\circ {+}_v$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnsb	$$class{-}_v$$
1		cgs	$$class{/}_g$$
2		cpv	$$class{+}_v$$
3	1 2	ccom	$$class\left({/}_g\circ {+}_v\right)$$
4	0 3	wceq	$$wff{-}_v={/}_g\circ {+}_v$$