Metamath Proof Explorer

Theorem negcncfg

Description: The opposite of a continuous function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis negcncfg.1 
|- ( ph -> ( x e. A |-> B ) e. ( A -cn-> CC ) )
Assertion negcncfg 
|- ( ph -> ( x e. A |-> -u B ) e. ( A -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 negcncfg.1 
 |-  ( ph -> ( x e. A |-> B ) e. ( A -cn-> CC ) )
2 df-neg 
 |-  -u B = ( 0 - B )
3 2 a1i 
 |-  ( ( ph /\ x e. A ) -> -u B = ( 0 - B ) )
4 3 mpteq2dva 
 |-  ( ph -> ( x e. A |-> -u B ) = ( x e. A |-> ( 0 - B ) ) )
5 eqid 
 |-  ( x e. CC |-> 0 ) = ( x e. CC |-> 0 )
6 0cn 
 |-  0 e. CC
7 ssidd 
 |-  ( 0 e. CC -> CC C_ CC )
8 id 
 |-  ( 0 e. CC -> 0 e. CC )
9 7 8 7 constcncfg 
 |-  ( 0 e. CC -> ( x e. CC |-> 0 ) e. ( CC -cn-> CC ) )
10 6 9 mp1i 
 |-  ( ph -> ( x e. CC |-> 0 ) e. ( CC -cn-> CC ) )
11 cncfrss 
 |-  ( ( x e. A |-> B ) e. ( A -cn-> CC ) -> A C_ CC )
12 1 11 syl 
 |-  ( ph -> A C_ CC )
13 ssidd 
 |-  ( ph -> CC C_ CC )
14 6 a1i 
 |-  ( ( ph /\ x e. A ) -> 0 e. CC )
15 5 10 12 13 14 cncfmptssg 
 |-  ( ph -> ( x e. A |-> 0 ) e. ( A -cn-> CC ) )
16 15 1 subcncf 
 |-  ( ph -> ( x e. A |-> ( 0 - B ) ) e. ( A -cn-> CC ) )
17 4 16 eqeltrd 
 |-  ( ph -> ( x e. A |-> -u B ) e. ( A -cn-> CC ) )