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 ) |
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 ) |