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 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cpv | ⊢ +𝑣 | |
1 | c1st | ⊢ 1st | |
2 | 1 1 | ccom | ⊢ ( 1st ∘ 1st ) |
3 | 0 2 | wceq | ⊢ +𝑣 = ( 1st ∘ 1st ) |