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) Avoid ax-mulf . (Revised by GG, 30-Apr-2025)

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 2 5 6 dvrcl 
 |-  ( ( CCfld e. Ring /\ x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( x ( /r ` CCfld ) y ) e. CC )
8 1 7 mp3an1 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( x ( /r ` CCfld ) y ) e. CC )
9 difssd 
 |-  ( x e. CC -> ( CC \ { 0 } ) C_ CC )
10 9 sselda 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> y e. CC )
11 ovmpot 
 |-  ( ( ( x ( /r ` CCfld ) y ) e. CC /\ y e. CC ) -> ( ( x ( /r ` CCfld ) y ) ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( ( x ( /r ` CCfld ) y ) x. y ) )
12 8 10 11 syl2anc 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( x ( /r ` CCfld ) y ) ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( ( x ( /r ` CCfld ) y ) x. y ) )
13 mpocnfldmul 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) = ( .r ` CCfld )
14 2 5 6 13 dvrcan1 
 |-  ( ( CCfld e. Ring /\ x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( x ( /r ` CCfld ) y ) ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = x )
15 1 14 mp3an1 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( x ( /r ` CCfld ) y ) ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = x )
16 12 15 eqtr3d 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( x ( /r ` CCfld ) y ) x. y ) = x )
17 16 oveq1d 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( ( x ( /r ` CCfld ) y ) x. y ) / y ) = ( x / y ) )
18 eldifsni 
 |-  ( y e. ( CC \ { 0 } ) -> y =/= 0 )
19 18 adantl 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> y =/= 0 )
20 8 10 19 divcan4d 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( ( x ( /r ` CCfld ) y ) x. y ) / y ) = ( x ( /r ` CCfld ) y ) )
21 17 20 eqtr3d 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( x / y ) = ( x ( /r ` CCfld ) y ) )
22 simpl 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> x e. CC )
23 divval 
 |-  ( ( x e. CC /\ y e. CC /\ y =/= 0 ) -> ( x / y ) = ( iota_ z e. CC ( y x. z ) = x ) )
24 22 10 19 23 syl3anc 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( x / y ) = ( iota_ z e. CC ( y x. z ) = x ) )
25 21 24 eqtr3d 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( x ( /r ` CCfld ) y ) = ( iota_ z e. CC ( y x. z ) = x ) )
26 eqid 
 |-  ( .r ` CCfld ) = ( .r ` CCfld )
27 eqid 
 |-  ( invr ` CCfld ) = ( invr ` CCfld )
28 2 26 5 27 6 dvrval 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( x ( /r ` CCfld ) y ) = ( x ( .r ` CCfld ) ( ( invr ` CCfld ) ` y ) ) )
29 25 28 eqtr3d 
 |-  ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( iota_ z e. CC ( y x. z ) = x ) = ( x ( .r ` CCfld ) ( ( invr ` CCfld ) ` y ) ) )
30 29 mpoeq3ia 
 |-  ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) ) = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( x ( .r ` CCfld ) ( ( invr ` CCfld ) ` y ) ) )
31 df-div 
 |-  / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
32 2 26 5 27 6 dvrfval 
 |-  ( /r ` CCfld ) = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( x ( .r ` CCfld ) ( ( invr ` CCfld ) ` y ) ) )
33 30 31 32 3eqtr4i 
 |-  / = ( /r ` CCfld )