Theorem cnfldsub

Description: The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Assertion	cnfldsub	|- - = ( -g ` CCfld )

Proof

Step	Hyp	Ref	Expression
1		cnfldbas	|- CC = ( Base ` CCfld )
2		cnfldadd	|- + = ( +g ` CCfld )
3		eqid	|- ( invg ` CCfld ) = ( invg ` CCfld )
4		eqid	|- ( -g ` CCfld ) = ( -g ` CCfld )
5	1 2 3 4	grpsubval	|- ( ( x e. CC /\ y e. CC ) -> ( x ( -g ` CCfld ) y ) = ( x + ( ( invg ` CCfld ) ` y ) ) )
6		cnfldneg	|- ( y e. CC -> ( ( invg ` CCfld ) ` y ) = -u y )
7	6	adantl	|- ( ( x e. CC /\ y e. CC ) -> ( ( invg ` CCfld ) ` y ) = -u y )
8	7	oveq2d	|- ( ( x e. CC /\ y e. CC ) -> ( x + ( ( invg ` CCfld ) ` y ) ) = ( x + -u y ) )
9		negsub	|- ( ( x e. CC /\ y e. CC ) -> ( x + -u y ) = ( x - y ) )
10	5 8 9	3eqtrrd	|- ( ( x e. CC /\ y e. CC ) -> ( x - y ) = ( x ( -g ` CCfld ) y ) )
11	10	mpoeq3ia	|- ( x e. CC , y e. CC |-> ( x - y ) ) = ( x e. CC , y e. CC |-> ( x ( -g ` CCfld ) y ) )
12		subf	|- - : ( CC X. CC ) --> CC
13		ffn	|- ( - : ( CC X. CC ) --> CC -> - Fn ( CC X. CC ) )
14	12 13	ax-mp	|- - Fn ( CC X. CC )
15		fnov	|- ( - Fn ( CC X. CC ) <-> - = ( x e. CC , y e. CC |-> ( x - y ) ) )
16	14 15	mpbi	|- - = ( x e. CC , y e. CC |-> ( x - y ) )
17		cnring	|- CCfld e. Ring
18		ringgrp	|- ( CCfld e. Ring -> CCfld e. Grp )
19	17 18	ax-mp	|- CCfld e. Grp
20	1 4	grpsubf	|- ( CCfld e. Grp -> ( -g ` CCfld ) : ( CC X. CC ) --> CC )
21		ffn	|- ( ( -g ` CCfld ) : ( CC X. CC ) --> CC -> ( -g ` CCfld ) Fn ( CC X. CC ) )
22	19 20 21	mp2b	|- ( -g ` CCfld ) Fn ( CC X. CC )
23		fnov	|- ( ( -g ` CCfld ) Fn ( CC X. CC ) <-> ( -g ` CCfld ) = ( x e. CC , y e. CC |-> ( x ( -g ` CCfld ) y ) ) )
24	22 23	mpbi	|- ( -g ` CCfld ) = ( x e. CC , y e. CC |-> ( x ( -g ` CCfld ) y ) )
25	11 16 24	3eqtr4i	|- - = ( -g ` CCfld )