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

Proof

Step Hyp Ref Expression
1 negfcncf.1 ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ - ( 𝐹 ‘ 𝑥 ) )
2 cncff ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
3 2 ffvelcdmda ⊢ ( ( 𝐹 ∈ ( 𝐴 –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→ ℂ ) )