This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = <. <. + , x. >. , abs >.
Assertion cnnvm 
|- - = ( -v ` U )

Proof

Step Hyp Ref Expression
1 cnnvm.6 
 |-  U = <. <. + , x. >. , abs >.
2 mulm1 
 |-  ( y e. CC -> ( -u 1 x. y ) = -u y )
3 2 adantl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( -u 1 x. y ) = -u y )
4 3 oveq2d 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + ( -u 1 x. y ) ) = ( x + -u y ) )
5 negsub 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + -u y ) = ( x - y ) )
6 4 5 eqtr2d 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x - y ) = ( x + ( -u 1 x. y ) ) )
7 6 mpoeq3ia 
 |-  ( x e. CC , y e. CC |-> ( x - y ) ) = ( x e. CC , y e. CC |-> ( x + ( -u 1 x. y ) ) )
8 subf 
 |-  - : ( CC X. CC ) --> CC
9 ffn 
 |-  ( - : ( CC X. CC ) --> CC -> - Fn ( CC X. CC ) )
10 8 9 ax-mp 
 |-  - Fn ( CC X. CC )
11 fnov 
 |-  ( - Fn ( CC X. CC ) <-> - = ( x e. CC , y e. CC |-> ( x - y ) ) )
12 10 11 mpbi 
 |-  - = ( x e. CC , y e. CC |-> ( x - y ) )
13 1 cnnv 
 |-  U e. NrmCVec
14 1 cnnvba 
 |-  CC = ( BaseSet ` U )
15 1 cnnvg 
 |-  + = ( +v ` U )
16 1 cnnvs 
 |-  x. = ( .sOLD ` U )
17 eqid 
 |-  ( -v ` U ) = ( -v ` U )
18 14 15 16 17 nvmfval 
 |-  ( U e. NrmCVec -> ( -v ` U ) = ( x e. CC , y e. CC |-> ( x + ( -u 1 x. y ) ) ) )
19 13 18 ax-mp 
 |-  ( -v ` U ) = ( x e. CC , y e. CC |-> ( x + ( -u 1 x. y ) ) )
20 7 12 19 3eqtr4i 
 |-  - = ( -v ` U )