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 )