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
|- +v = ( 1st o. 1st )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpv
 |-  +v
1 c1st
 |-  1st
2 1 1 ccom
 |-  ( 1st o. 1st )
3 0 2 wceq
 |-  +v = ( 1st o. 1st )