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