Metamath Proof Explorer

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	⊢ +_𝑣 = ( 1^st ∘ 1^st )

Step	Hyp	Ref	Expression
0		cpv	⊢ +_𝑣
1		c1st	⊢ 1^st
2	1 1	ccom	⊢ ( 1^st ∘ 1^st )
3	0 2	wceq	⊢ +_𝑣 = ( 1^st ∘ 1^st )