Metamath Proof Explorer

Theorem cnflddiv

Description: The division operation in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion cnflddiv 
|- / = ( /r ` CCfld )

Proof

Step Hyp Ref Expression
1 cnring 
 |-  CCfld e. Ring
2 cnfldbas 
 |-  CC = ( Base ` CCfld )
3 cnfld0 
 |-  0 = ( 0g ` CCfld )
4 cndrng 
 |-  CCfld e. DivRing
5 2 3 4 drngui 
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
6 eqid 
 |-  ( /r ` CCfld ) = ( /r ` CCfld )
7 cnfldmul 
 |-  x. = ( .r ` CCfld )
8 2 5 6 7 dvrcan1 
 |-  ( ( CCfld e. Ring /\ x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( x ( /r ` CCfld ) y ) x. y ) = x )
9 1 8 mp3an1 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( x ( /r ` CCfld ) y ) x. y ) = x )
10 9 oveq1d 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( ( x ( /r ` CCfld ) y ) x. y ) / y ) = ( x / y ) )
11 2 5 6 dvrcl 
 |-  ( ( CCfld e. Ring /\ x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( x ( /r ` CCfld ) y ) e. CC )
12 1 11 mp3an1 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( x ( /r ` CCfld ) y ) e. CC )
13 simpr 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> y e. ( CC \ { 0 } ) )
14 eldifsn 
 |-  ( y e. ( CC \ { 0 } ) <-> ( y e. CC /\ y =/= 0 ) )
15 13 14 sylib 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( y e. CC /\ y =/= 0 ) )
16 15 simpld 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> y e. CC )
17 15 simprd 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> y =/= 0 )
18 12 16 17 divcan4d 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( ( x ( /r ` CCfld ) y ) x. y ) / y ) = ( x ( /r ` CCfld ) y ) )
19 10 18 eqtr3d 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( x / y ) = ( x ( /r ` CCfld ) y ) )
20 simpl 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> x e. CC )
21 divval 
 |-  ( ( x e. CC /\ y e. CC /\ y =/= 0 ) -> ( x / y ) = ( iota_ z e. CC ( y x. z ) = x ) )
22 20 16 17 21 syl3anc 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( x / y ) = ( iota_ z e. CC ( y x. z ) = x ) )
23 19 22 eqtr3d 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( x ( /r ` CCfld ) y ) = ( iota_ z e. CC ( y x. z ) = x ) )
24 eqid 
 |-  ( invr ` CCfld ) = ( invr ` CCfld )
25 2 7 5 24 6 dvrval 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( x ( /r ` CCfld ) y ) = ( x x. ( ( invr ` CCfld ) ` y ) ) )
26 23 25 eqtr3d 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( iota_ z e. CC ( y x. z ) = x ) = ( x x. ( ( invr ` CCfld ) ` y ) ) )
27 26 mpoeq3ia 
 |-  ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) ) = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( x x. ( ( invr ` CCfld ) ` y ) ) )
28 df-div 
 |-  / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
29 2 7 5 24 6 dvrfval 
 |-  ( /r ` CCfld ) = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( x x. ( ( invr ` CCfld ) ` y ) ) )
30 27 28 29 3eqtr4i 
 |-  / = ( /r ` CCfld )