Metamath Proof Explorer


Theorem cnnvm

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 U=+×abs
Assertion cnnvm =-vU

Proof

Step Hyp Ref Expression
1 cnnvm.6 U=+×abs
2 mulm1 y-1y=y
3 2 adantl xy-1y=y
4 3 oveq2d xyx+-1y=x+y
5 negsub xyx+y=xy
6 4 5 eqtr2d xyxy=x+-1y
7 6 mpoeq3ia x,yxy=x,yx+-1y
8 subf :×
9 ffn :×Fn×
10 8 9 ax-mp Fn×
11 fnov Fn×=x,yxy
12 10 11 mpbi =x,yxy
13 1 cnnv UNrmCVec
14 1 cnnvba =BaseSetU
15 1 cnnvg +=+vU
16 1 cnnvs ×=𝑠OLDU
17 eqid -vU=-vU
18 14 15 16 17 nvmfval UNrmCVec-vU=x,yx+-1y
19 13 18 ax-mp -vU=x,yx+-1y
20 7 12 19 3eqtr4i =-vU