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=xAFx
Assertion negfcncf F:AcnG:Acn

Proof

Step Hyp Ref Expression
1 negfcncf.1 G=xAFx
2 cncff F:AcnF:A
3 2 ffvelcdmda F:AcnxAFx
4 2 feqmptd F:AcnF=xAFx
5 eqidd F:Acnyy=yy
6 negeq y=Fxy=Fx
7 3 4 5 6 fmptco F:AcnyyF=xAFx
8 7 1 eqtr4di F:AcnyyF=G
9 id F:AcnF:Acn
10 ssid
11 eqid yy=yy
12 11 negcncf yy:cn
13 10 12 mp1i F:Acnyy:cn
14 9 13 cncfco F:AcnyyF:Acn
15 8 14 eqeltrrd F:AcnG:Acn