Metamath Proof Explorer

Definition df-vs

Description: Define vector subtraction on a normed complex vector space. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

Ref Expression
Assertion df-vs 
|- -v = ( /g o. +v )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnsb 
 |-  -v
1 cgs 
 |-  /g
2 cpv 
 |-  +v
3 1 2 ccom 
 |-  ( /g o. +v )
4 0 3 wceq 
 |-  -v = ( /g o. +v )