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

Detailed syntax breakdown

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