df-va - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-va		Structured version Visualization version GIF version

Definition df-va 30614

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

**Assertion**
Ref	Expression
df-va	⊢ +_𝑣 = (1^st ∘ 1^st )

**Detailed syntax breakdown of Definition df-va**
Step	Hyp	Ref	Expression
1		cpv 30604	. 2 class +_𝑣
2		c1st 8012	. . 3 class 1^st
3	2, 2	ccom 5689	. 2 class (1^st ∘ 1^st )
4	1, 3	wceq 1540	1 wff +_𝑣 = (1^st ∘ 1^st )

Colors of variables: wff setvar class

This definition is referenced by: vafval 30622 0vfval 30625 vsfval 30652