Metamath Proof Explorer

Theorem cncrng

Description: The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015) Avoid ax-mulf . (Revised by GG, 31-Mar-2025)

Ref Expression
Assertion cncrng 
|- CCfld e. CRing

Proof

Step Hyp Ref Expression
1 cnfldbas 
 |-  CC = ( Base ` CCfld )
2 1 a1i 
 |-  ( T. -> CC = ( Base ` CCfld ) )
3 cnfldadd 
 |-  + = ( +g ` CCfld )
4 3 a1i 
 |-  ( T. -> + = ( +g ` CCfld ) )
5 mpocnfldmul 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) = ( .r ` CCfld )
6 5 a1i 
 |-  ( T. -> ( u e. CC , v e. CC |-> ( u x. v ) ) = ( .r ` CCfld ) )
7 addcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
8 addass 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x + y ) + z ) = ( x + ( y + z ) ) )
9 0cn 
 |-  0 e. CC
10 addlid 
 |-  ( x e. CC -> ( 0 + x ) = x )
11 negcl 
 |-  ( x e. CC -> -u x e. CC )
12 id 
 |-  ( x e. CC -> x e. CC )
13 11 12 addcomd 
 |-  ( x e. CC -> ( -u x + x ) = ( x + -u x ) )
14 negid 
 |-  ( x e. CC -> ( x + -u x ) = 0 )
15 13 14 eqtrd 
 |-  ( x e. CC -> ( -u x + x ) = 0 )
16 1 3 7 8 9 10 11 15 isgrpi 
 |-  CCfld e. Grp
17 16 a1i 
 |-  ( T. -> CCfld e. Grp )
18 mpomulf 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) : ( CC X. CC ) --> CC
19 18 fovcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) e. CC )
20 19 3adant1 
 |-  ( ( T. /\ x e. CC /\ y e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) e. CC )
21 mulass 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x x. y ) x. z ) = ( x x. ( y x. z ) ) )
22 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
23 ovmpot 
 |-  ( ( ( x x. y ) e. CC /\ z e. CC ) -> ( ( x x. y ) ( u e. CC , v e. CC |-> ( u x. v ) ) z ) = ( ( x x. y ) x. z ) )
24 22 23 stoic3 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x x. y ) ( u e. CC , v e. CC |-> ( u x. v ) ) z ) = ( ( x x. y ) x. z ) )
25 simp1 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> x e. CC )
26 mulcl 
 |-  ( ( y e. CC /\ z e. CC ) -> ( y x. z ) e. CC )
27 26 3adant1 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( y x. z ) e. CC )
28 ovmpot 
 |-  ( ( x e. CC /\ ( y x. z ) e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) ( y x. z ) ) = ( x x. ( y x. z ) ) )
29 25 27 28 syl2anc 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) ( y x. z ) ) = ( x x. ( y x. z ) ) )
30 21 24 29 3eqtr4d 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x x. y ) ( u e. CC , v e. CC |-> ( u x. v ) ) z ) = ( x ( u e. CC , v e. CC |-> ( u x. v ) ) ( y x. z ) ) )
31 ovmpot 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( x x. y ) )
32 31 3adant3 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( x x. y ) )
33 32 oveq1d 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ( u e. CC , v e. CC |-> ( u x. v ) ) z ) = ( ( x x. y ) ( u e. CC , v e. CC |-> ( u x. v ) ) z ) )
34 ovmpot 
 |-  ( ( y e. CC /\ z e. CC ) -> ( y ( u e. CC , v e. CC |-> ( u x. v ) ) z ) = ( y x. z ) )
35 34 3adant1 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( y ( u e. CC , v e. CC |-> ( u x. v ) ) z ) = ( y x. z ) )
36 35 oveq2d 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) ( y ( u e. CC , v e. CC |-> ( u x. v ) ) z ) ) = ( x ( u e. CC , v e. CC |-> ( u x. v ) ) ( y x. z ) ) )
37 30 33 36 3eqtr4d 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ( u e. CC , v e. CC |-> ( u x. v ) ) z ) = ( x ( u e. CC , v e. CC |-> ( u x. v ) ) ( y ( u e. CC , v e. CC |-> ( u x. v ) ) z ) ) )
38 37 adantl 
 |-  ( ( T. /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ( u e. CC , v e. CC |-> ( u x. v ) ) z ) = ( x ( u e. CC , v e. CC |-> ( u x. v ) ) ( y ( u e. CC , v e. CC |-> ( u x. v ) ) z ) ) )
39 adddi 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( x x. ( y + z ) ) = ( ( x x. y ) + ( x x. z ) ) )
40 addcl 
 |-  ( ( y e. CC /\ z e. CC ) -> ( y + z ) e. CC )
41 40 3adant1 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( y + z ) e. CC )
42 ovmpot 
 |-  ( ( x e. CC /\ ( y + z ) e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) ( y + z ) ) = ( x x. ( y + z ) ) )
43 25 41 42 syl2anc 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) ( y + z ) ) = ( x x. ( y + z ) ) )
44 ovmpot 
 |-  ( ( x e. CC /\ z e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) z ) = ( x x. z ) )
45 44 3adant2 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) z ) = ( x x. z ) )
46 32 45 oveq12d 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) + ( x ( u e. CC , v e. CC |-> ( u x. v ) ) z ) ) = ( ( x x. y ) + ( x x. z ) ) )
47 39 43 46 3eqtr4d 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) ( y + z ) ) = ( ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) + ( x ( u e. CC , v e. CC |-> ( u x. v ) ) z ) ) )
48 47 adantl 
 |-  ( ( T. /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) ( y + z ) ) = ( ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) + ( x ( u e. CC , v e. CC |-> ( u x. v ) ) z ) ) )
49 adddir 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x + y ) x. z ) = ( ( x x. z ) + ( y x. z ) ) )
50 ovmpot 
 |-  ( ( ( x + y ) e. CC /\ z e. CC ) -> ( ( x + y ) ( u e. CC , v e. CC |-> ( u x. v ) ) z ) = ( ( x + y ) x. z ) )
51 7 50 stoic3 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x + y ) ( u e. CC , v e. CC |-> ( u x. v ) ) z ) = ( ( x + y ) x. z ) )
52 45 35 oveq12d 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x ( u e. CC , v e. CC |-> ( u x. v ) ) z ) + ( y ( u e. CC , v e. CC |-> ( u x. v ) ) z ) ) = ( ( x x. z ) + ( y x. z ) ) )
53 49 51 52 3eqtr4d 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x + y ) ( u e. CC , v e. CC |-> ( u x. v ) ) z ) = ( ( x ( u e. CC , v e. CC |-> ( u x. v ) ) z ) + ( y ( u e. CC , v e. CC |-> ( u x. v ) ) z ) ) )
54 53 adantl 
 |-  ( ( T. /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( ( x + y ) ( u e. CC , v e. CC |-> ( u x. v ) ) z ) = ( ( x ( u e. CC , v e. CC |-> ( u x. v ) ) z ) + ( y ( u e. CC , v e. CC |-> ( u x. v ) ) z ) ) )
55 1cnd 
 |-  ( T. -> 1 e. CC )
56 ax-1cn 
 |-  1 e. CC
57 ovmpot 
 |-  ( ( 1 e. CC /\ x e. CC ) -> ( 1 ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = ( 1 x. x ) )
58 56 57 mpan 
 |-  ( x e. CC -> ( 1 ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = ( 1 x. x ) )
59 mullid 
 |-  ( x e. CC -> ( 1 x. x ) = x )
60 58 59 eqtrd 
 |-  ( x e. CC -> ( 1 ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = x )
61 60 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( 1 ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = x )
62 ovmpot 
 |-  ( ( x e. CC /\ 1 e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) 1 ) = ( x x. 1 ) )
63 56 62 mpan2 
 |-  ( x e. CC -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) 1 ) = ( x x. 1 ) )
64 mulrid 
 |-  ( x e. CC -> ( x x. 1 ) = x )
65 63 64 eqtrd 
 |-  ( x e. CC -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) 1 ) = x )
66 65 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) 1 ) = x )
67 mulcom 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) = ( y x. x ) )
68 ovmpot 
 |-  ( ( y e. CC /\ x e. CC ) -> ( y ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = ( y x. x ) )
69 68 ancoms 
 |-  ( ( x e. CC /\ y e. CC ) -> ( y ( u e. CC , v e. CC |-> ( u x. v ) ) x ) = ( y x. x ) )
70 67 31 69 3eqtr4d 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( y ( u e. CC , v e. CC |-> ( u x. v ) ) x ) )
71 70 3adant1 
 |-  ( ( T. /\ x e. CC /\ y e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( y ( u e. CC , v e. CC |-> ( u x. v ) ) x ) )
72 2 4 6 17 20 38 48 54 55 61 66 71 iscrngd 
 |-  ( T. -> CCfld e. CRing )
73 72 mptru 
 |-  CCfld e. CRing