Metamath Proof Explorer

Theorem cncrng

Description: The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015)

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 cnfldmul 
 |-  x. = ( .r ` CCfld )
6 5 a1i 
 |-  ( T. -> x. = ( .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 addid2 
 |-  ( x e. CC -> ( 0 + x ) = x )
11 negcl 
 |-  ( x e. CC -> -u x e. CC )
12 addcom 
 |-  ( ( -u x e. CC /\ x e. CC ) -> ( -u x + x ) = ( x + -u x ) )
13 11 12 mpancom 
 |-  ( 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 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
19 18 3adant1 
 |-  ( ( T. /\ x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
20 mulass 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x x. y ) x. z ) = ( x x. ( y x. z ) ) )
21 20 adantl 
 |-  ( ( T. /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( ( x x. y ) x. z ) = ( x x. ( y x. z ) ) )
22 adddi 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( x x. ( y + z ) ) = ( ( x x. y ) + ( x x. z ) ) )
23 22 adantl 
 |-  ( ( T. /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( x x. ( y + z ) ) = ( ( x x. y ) + ( x x. z ) ) )
24 adddir 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x + y ) x. z ) = ( ( x x. z ) + ( y x. z ) ) )
25 24 adantl 
 |-  ( ( T. /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( ( x + y ) x. z ) = ( ( x x. z ) + ( y x. z ) ) )
26 1cnd 
 |-  ( T. -> 1 e. CC )
27 mulid2 
 |-  ( x e. CC -> ( 1 x. x ) = x )
28 27 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( 1 x. x ) = x )
29 mulid1 
 |-  ( x e. CC -> ( x x. 1 ) = x )
30 29 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( x x. 1 ) = x )
31 mulcom 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) = ( y x. x ) )
32 31 3adant1 
 |-  ( ( T. /\ x e. CC /\ y e. CC ) -> ( x x. y ) = ( y x. x ) )
33 2 4 6 17 19 21 23 25 26 28 30 32 iscrngd 
 |-  ( T. -> CCfld e. CRing )
34 33 mptru 
 |-  CCfld e. CRing