This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) )
Assertion negcncfg ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 negcncfg.1 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) )
2 df-neg ⊢ - 𝐵 = ( 0 − 𝐵 )
3 2 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 = ( 0 − 𝐵 ) )
4 3 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ ( 0 − 𝐵 ) ) )
5 eqid ⊢ ( 𝑥 ∈ ℂ ↦ 0 ) = ( 𝑥 ∈ ℂ ↦ 0 )
6 0cn ⊢ 0 ∈ ℂ
7 ssidd ⊢ ( 0 ∈ ℂ → ℂ ⊆ ℂ )
8 id ⊢ ( 0 ∈ ℂ → 0 ∈ ℂ )
9 7 8 7 constcncfg ⊢ ( 0 ∈ ℂ → ( 𝑥 ∈ ℂ ↦ 0 ) ∈ ( ℂ –cn→ ℂ ) )
10 6 9 mp1i ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ 0 ) ∈ ( ℂ –cn→ ℂ ) )
11 cncfrss ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) → 𝐴 ⊆ ℂ )
12 1 11 syl ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
13 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
14 6 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ∈ ℂ )
15 5 10 12 13 14 cncfmptssg ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 0 ) ∈ ( 𝐴 –cn→ ℂ ) )
16 15 1 subcncf ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 0 − 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
17 4 16 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) )