Metamath Proof Explorer


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 ffvelrnda
 |-  ( ( 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 ) )