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	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ - ( 𝐹 ‘ 𝑥 ) )
Assertion	negfcncf	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → 𝐺 ∈ ( 𝐴 –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		negfcncf.1	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ - ( 𝐹 ‘ 𝑥 ) )
2		cncff	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
3	2	ffvelrnda	⊢ ( ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
4	2	feqmptd	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
5		eqidd	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → ( 𝑦 ∈ ℂ ↦ - 𝑦 ) = ( 𝑦 ∈ ℂ ↦ - 𝑦 ) )
6		negeq	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → - 𝑦 = - ( 𝐹 ‘ 𝑥 ) )
7	3 4 5 6	fmptco	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → ( ( 𝑦 ∈ ℂ ↦ - 𝑦 ) ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ - ( 𝐹 ‘ 𝑥 ) ) )
8	7 1	eqtr4di	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → ( ( 𝑦 ∈ ℂ ↦ - 𝑦 ) ∘ 𝐹 ) = 𝐺 )
9		id	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )
10		ssid	⊢ ℂ ⊆ ℂ
11		eqid	⊢ ( 𝑦 ∈ ℂ ↦ - 𝑦 ) = ( 𝑦 ∈ ℂ ↦ - 𝑦 )
12	11	negcncf	⊢ ( ℂ ⊆ ℂ → ( 𝑦 ∈ ℂ ↦ - 𝑦 ) ∈ ( ℂ –cn→ ℂ ) )
13	10 12	mp1i	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → ( 𝑦 ∈ ℂ ↦ - 𝑦 ) ∈ ( ℂ –cn→ ℂ ) )
14	9 13	cncfco	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → ( ( 𝑦 ∈ ℂ ↦ - 𝑦 ) ∘ 𝐹 ) ∈ ( 𝐴 –cn→ ℂ ) )
15	8 14	eqeltrrd	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → 𝐺 ∈ ( 𝐴 –cn→ ℂ ) )