Metamath Proof Explorer

Theorem cndrng

Description: The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014) Avoid ax-mulf . (Revised by GG, 30-Apr-2025)

Ref Expression
Assertion cndrng 
|- CCfld e. DivRing

Proof

Step Hyp Ref Expression
1 cnfldbas 
 |-  CC = ( Base ` CCfld )
2 1 a1i 
 |-  ( T. -> CC = ( Base ` CCfld ) )
3 mpocnfldmul 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) = ( .r ` CCfld )
4 3 a1i 
 |-  ( T. -> ( u e. CC , v e. CC |-> ( u x. v ) ) = ( .r ` CCfld ) )
5 cnfld0 
 |-  0 = ( 0g ` CCfld )
6 5 a1i 
 |-  ( T. -> 0 = ( 0g ` CCfld ) )
7 cnfld1 
 |-  1 = ( 1r ` CCfld )
8 7 a1i 
 |-  ( T. -> 1 = ( 1r ` CCfld ) )
9 cnring 
 |-  CCfld e. Ring
10 9 a1i 
 |-  ( T. -> CCfld e. Ring )
11 ovmpot 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( x x. y ) )
12 11 ad2ant2r 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( x x. y ) )
13 mulne0 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( x x. y ) =/= 0 )
14 12 13 eqnetrd 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) =/= 0 )
15 14 3adant1 
 |-  ( ( T. /\ ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) =/= 0 )
16 ax-1ne0 
 |-  1 =/= 0
17 16 a1i 
 |-  ( T. -> 1 =/= 0 )
18 reccl 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( 1 / x ) e. CC )
19 18 adantl 
 |-  ( ( T. /\ ( x e. CC /\ x =/= 0 ) ) -> ( 1 / x ) e. CC )
20 simpl 
 |-  ( ( x e. CC /\ x =/= 0 ) -> x e. CC )
21 ovmpot 
 |-  ( ( ( 1 / x ) e. CC /\ x e. CC ) -> ( ( 1 / x ) ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = ( ( 1 / x ) x. x ) )
22 18 20 21 syl2anc 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( ( 1 / x ) ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = ( ( 1 / x ) x. x ) )
23 recid2 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( ( 1 / x ) x. x ) = 1 )
24 22 23 eqtrd 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( ( 1 / x ) ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = 1 )
25 24 adantl 
 |-  ( ( T. /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( 1 / x ) ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = 1 )
26 2 4 6 8 10 15 17 19 25 isdrngd 
 |-  ( T. -> CCfld e. DivRing )
27 26 mptru 
 |-  CCfld e. DivRing