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→ ℂ ) )