Definition df-va

Description: Define vector addition on a normed complex vector space. (Contributed by NM, 23-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	df-va	$$⊢{+}_v=1^{st}\circ 1^{st}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpv	$$class{+}_v$$
1		c1st	$$class{1}^{st}$$
2	1 1	ccom	$$class\left(1^{st}\circ 1^{st}\right)$$
3	0 2	wceq	$$wff{+}_v=1^{st}\circ 1^{st}$$