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

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