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=\left(x\in A⟼-F\left(x\right)\right)$$
Assertion	negfcncf	$$⊢F:A\underset{cn}{⟶}ℂ\to G:A\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		negfcncf.1	$$⊢G=\left(x\in A⟼-F\left(x\right)\right)$$
2		cncff	$$⊢F:A\underset{cn}{⟶}ℂ\to F:A⟶ℂ$$
3	2	ffvelrnda	$$⊢\left(F:A\underset{cn}{⟶}ℂ\wedge x\in A\right)\to F\left(x\right)\in ℂ$$
4	2	feqmptd	$$⊢F:A\underset{cn}{⟶}ℂ\to F=\left(x\in A⟼F\left(x\right)\right)$$
5		eqidd	$$⊢F:A\underset{cn}{⟶}ℂ\to \left(y\in ℂ⟼-y\right)=\left(y\in ℂ⟼-y\right)$$
6		negeq	$$⊢y=F\left(x\right)\to -y=-F\left(x\right)$$
7	3 4 5 6	fmptco	$$⊢F:A\underset{cn}{⟶}ℂ\to \left(y\in ℂ⟼-y\right)\circ F=\left(x\in A⟼-F\left(x\right)\right)$$
8	7 1	eqtr4di	$$⊢F:A\underset{cn}{⟶}ℂ\to \left(y\in ℂ⟼-y\right)\circ F=G$$
9		id	$$⊢F:A\underset{cn}{⟶}ℂ\to F:A\underset{cn}{⟶}ℂ$$
10		ssid	$$⊢ℂ\subseteq ℂ$$
11		eqid	$$⊢\left(y\in ℂ⟼-y\right)=\left(y\in ℂ⟼-y\right)$$
12	11	negcncf	$$⊢ℂ\subseteq ℂ\to \left(y\in ℂ⟼-y\right):ℂ\underset{cn}{⟶}ℂ$$
13	10 12	mp1i	$$⊢F:A\underset{cn}{⟶}ℂ\to \left(y\in ℂ⟼-y\right):ℂ\underset{cn}{⟶}ℂ$$
14	9 13	cncfco	$$⊢F:A\underset{cn}{⟶}ℂ\to \left(\left(y\in ℂ⟼-y\right)\circ F\right):A\underset{cn}{⟶}ℂ$$
15	8 14	eqeltrrd	$$⊢F:A\underset{cn}{⟶}ℂ\to G:A\underset{cn}{⟶}ℂ$$