This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnsrng

Description: The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Assertion cnsrng 
|- CCfld e. *Ring

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 cnfldcj 
 |-  * = ( *r ` CCfld )
8 7 a1i 
 |-  ( T. -> * = ( *r ` CCfld ) )
9 cnring 
 |-  CCfld e. Ring
10 9 a1i 
 |-  ( T. -> CCfld e. Ring )
11 cjcl 
 |-  ( x e. CC -> ( * ` x ) e. CC )
12 11 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( * ` x ) e. CC )
13 cjadd 
 |-  ( ( x e. CC /\ y e. CC ) -> ( * ` ( x + y ) ) = ( ( * ` x ) + ( * ` y ) ) )
14 13 3adant1 
 |-  ( ( T. /\ x e. CC /\ y e. CC ) -> ( * ` ( x + y ) ) = ( ( * ` x ) + ( * ` y ) ) )
15 mulcom 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) = ( y x. x ) )
16 15 fveq2d 
 |-  ( ( x e. CC /\ y e. CC ) -> ( * ` ( x x. y ) ) = ( * ` ( y x. x ) ) )
17 cjmul 
 |-  ( ( y e. CC /\ x e. CC ) -> ( * ` ( y x. x ) ) = ( ( * ` y ) x. ( * ` x ) ) )
18 17 ancoms 
 |-  ( ( x e. CC /\ y e. CC ) -> ( * ` ( y x. x ) ) = ( ( * ` y ) x. ( * ` x ) ) )
19 16 18 eqtrd 
 |-  ( ( x e. CC /\ y e. CC ) -> ( * ` ( x x. y ) ) = ( ( * ` y ) x. ( * ` x ) ) )
20 19 3adant1 
 |-  ( ( T. /\ x e. CC /\ y e. CC ) -> ( * ` ( x x. y ) ) = ( ( * ` y ) x. ( * ` x ) ) )
21 cjcj 
 |-  ( x e. CC -> ( * ` ( * ` x ) ) = x )
22 21 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( * ` ( * ` x ) ) = x )
23 2 4 6 8 10 12 14 20 22 issrngd 
 |-  ( T. -> CCfld e. *Ring )
24 23 mptru 
 |-  CCfld e. *Ring