Theorem negfcncf

Description: The negative of a continuous complex function is continuous. (Contributed by Paul Chapman, 21-Jan-2008) (Revised by Mario Carneiro, 25-Aug-2014)

	Ref	Expression
Hypothesis	negfcncf.1	|- G = ( x e. A |-> -u ( F ` x ) )
Assertion	negfcncf	|- ( F e. ( A -cn-> CC ) -> G e. ( A -cn-> CC ) )

Proof

Step	Hyp	Ref	Expression
1		negfcncf.1	|- G = ( x e. A |-> -u ( F ` x ) )
2		cncff	|- ( F e. ( A -cn-> CC ) -> F : A --> CC )
3	2	ffvelcdmda	|- ( ( F e. ( A -cn-> CC ) /\ x e. A ) -> ( F ` x ) e. CC )
4	2	feqmptd	|- ( F e. ( A -cn-> CC ) -> F = ( x e. A |-> ( F ` x ) ) )
5		eqidd	|- ( F e. ( A -cn-> CC ) -> ( y e. CC |-> -u y ) = ( y e. CC |-> -u y ) )
6		negeq	|- ( y = ( F ` x ) -> -u y = -u ( F ` x ) )
7	3 4 5 6	fmptco	|- ( F e. ( A -cn-> CC ) -> ( ( y e. CC |-> -u y ) o. F ) = ( x e. A |-> -u ( F ` x ) ) )
8	7 1	eqtr4di	|- ( F e. ( A -cn-> CC ) -> ( ( y e. CC |-> -u y ) o. F ) = G )
9		id	|- ( F e. ( A -cn-> CC ) -> F e. ( A -cn-> CC ) )
10		ssid	|- CC C_ CC
11		eqid	|- ( y e. CC |-> -u y ) = ( y e. CC |-> -u y )
12	11	negcncf	|- ( CC C_ CC -> ( y e. CC |-> -u y ) e. ( CC -cn-> CC ) )
13	10 12	mp1i	|- ( F e. ( A -cn-> CC ) -> ( y e. CC |-> -u y ) e. ( CC -cn-> CC ) )
14	9 13	cncfco	|- ( F e. ( A -cn-> CC ) -> ( ( y e. CC |-> -u y ) o. F ) e. ( A -cn-> CC ) )
15	8 14	eqeltrrd	|- ( F e. ( A -cn-> CC ) -> G e. ( A -cn-> CC ) )