Theorem negcncfg

Description: The opposite of a continuous function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypothesis	negcncfg.1	$$⊢\phi \to \left(x\in A⟼B\right):A\underset{cn}{⟶}ℂ$$
Assertion	negcncfg	$$⊢\phi \to \left(x\in A⟼-B\right):A\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		negcncfg.1	$$⊢\phi \to \left(x\in A⟼B\right):A\underset{cn}{⟶}ℂ$$
2		df-neg	$$⊢-B=0-B$$
3	2	a1i	$$⊢\left(\phi \wedge x\in A\right)\to -B=0-B$$
4	3	mpteq2dva	$$⊢\phi \to \left(x\in A⟼-B\right)=\left(x\in A⟼0-B\right)$$
5		eqid	$$⊢\left(x\in ℂ⟼0\right)=\left(x\in ℂ⟼0\right)$$
6		0cn	$$⊢0\in ℂ$$
7		ssidd	$$⊢0\in ℂ\to ℂ\subseteq ℂ$$
8		id	$$⊢0\in ℂ\to 0\in ℂ$$
9	7 8 7	constcncfg	$$⊢0\in ℂ\to \left(x\in ℂ⟼0\right):ℂ\underset{cn}{⟶}ℂ$$
10	6 9	mp1i	$$⊢\phi \to \left(x\in ℂ⟼0\right):ℂ\underset{cn}{⟶}ℂ$$
11		cncfrss	$$⊢\left(x\in A⟼B\right):A\underset{cn}{⟶}ℂ\to A\subseteq ℂ$$
12	1 11	syl	$$⊢\phi \to A\subseteq ℂ$$
13		ssidd	$$⊢\phi \to ℂ\subseteq ℂ$$
14	6	a1i	$$⊢\left(\phi \wedge x\in A\right)\to 0\in ℂ$$
15	5 10 12 13 14	cncfmptssg	$$⊢\phi \to \left(x\in A⟼0\right):A\underset{cn}{⟶}ℂ$$
16	15 1	subcncf	$$⊢\phi \to \left(x\in A⟼0-B\right):A\underset{cn}{⟶}ℂ$$
17	4 16	eqeltrd	$$⊢\phi \to \left(x\in A⟼-B\right):A\underset{cn}{⟶}ℂ$$