Description: The vector subtraction operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cnnvm.6 | |
|
Assertion | cnnvm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnnvm.6 | |
|
2 | mulm1 | |
|
3 | 2 | adantl | |
4 | 3 | oveq2d | |
5 | negsub | |
|
6 | 4 5 | eqtr2d | |
7 | 6 | mpoeq3ia | |
8 | subf | |
|
9 | ffn | |
|
10 | 8 9 | ax-mp | |
11 | fnov | |
|
12 | 10 11 | mpbi | |
13 | 1 | cnnv | |
14 | 1 | cnnvba | |
15 | 1 | cnnvg | |
16 | 1 | cnnvs | |
17 | eqid | |
|
18 | 14 15 16 17 | nvmfval | |
19 | 13 18 | ax-mp | |
20 | 7 12 19 | 3eqtr4i | |