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

Metamath Proof Explorer

Theorem cnfldsub

Description: The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Assertion cnfldsub 
|- - = ( -g ` CCfld )

Proof

Step Hyp Ref Expression
1 cnfldbas 
 |-  CC = ( Base ` CCfld )
2 cnfldadd 
 |-  + = ( +g ` CCfld )
3 eqid 
 |-  ( invg ` CCfld ) = ( invg ` CCfld )
4 eqid 
 |-  ( -g ` CCfld ) = ( -g ` CCfld )
5 1 2 3 4 grpsubval 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x ( -g ` CCfld ) y ) = ( x + ( ( invg ` CCfld ) ` y ) ) )
6 cnfldneg 
 |-  ( y e. CC -> ( ( invg ` CCfld ) ` y ) = -u y )
7 6 adantl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( ( invg ` CCfld ) ` y ) = -u y )
8 7 oveq2d 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + ( ( invg ` CCfld ) ` y ) ) = ( x + -u y ) )
9 negsub 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + -u y ) = ( x - y ) )
10 5 8 9 3eqtrrd 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x - y ) = ( x ( -g ` CCfld ) y ) )
11 10 mpoeq3ia 
 |-  ( x e. CC , y e. CC |-> ( x - y ) ) = ( x e. CC , y e. CC |-> ( x ( -g ` CCfld ) y ) )
12 subf 
 |-  - : ( CC X. CC ) --> CC
13 ffn 
 |-  ( - : ( CC X. CC ) --> CC -> - Fn ( CC X. CC ) )
14 12 13 ax-mp 
 |-  - Fn ( CC X. CC )
15 fnov 
 |-  ( - Fn ( CC X. CC ) <-> - = ( x e. CC , y e. CC |-> ( x - y ) ) )
16 14 15 mpbi 
 |-  - = ( x e. CC , y e. CC |-> ( x - y ) )
17 cnring 
 |-  CCfld e. Ring
18 ringgrp 
 |-  ( CCfld e. Ring -> CCfld e. Grp )
19 17 18 ax-mp 
 |-  CCfld e. Grp
20 1 4 grpsubf 
 |-  ( CCfld e. Grp -> ( -g ` CCfld ) : ( CC X. CC ) --> CC )
21 ffn 
 |-  ( ( -g ` CCfld ) : ( CC X. CC ) --> CC -> ( -g ` CCfld ) Fn ( CC X. CC ) )
22 19 20 21 mp2b 
 |-  ( -g ` CCfld ) Fn ( CC X. CC )
23 fnov 
 |-  ( ( -g ` CCfld ) Fn ( CC X. CC ) <-> ( -g ` CCfld ) = ( x e. CC , y e. CC |-> ( x ( -g ` CCfld ) y ) ) )
24 22 23 mpbi 
 |-  ( -g ` CCfld ) = ( x e. CC , y e. CC |-> ( x ( -g ` CCfld ) y ) )
25 11 16 24 3eqtr4i 
 |-  - = ( -g ` CCfld )