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	$⊢ G = (x \in A ⟼ - F (x))$
	Assertion	negfcncf	$⊢ F : A \underset{cn}{⟶} ℂ \to G : A \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		negfcncf.1	$⊢ G = (x \in A ⟼ - F (x))$
2		cncff	$⊢ F : A \underset{cn}{⟶} ℂ \to F : A ⟶ ℂ$
3	2	ffvelcdmda	$⊢ (F : A \underset{cn}{⟶} ℂ \land x \in A) \to F (x) \in ℂ$
4	2	feqmptd	$⊢ F : A \underset{cn}{⟶} ℂ \to F = (x \in A ⟼ F (x))$
5		eqidd	$⊢ F : A \underset{cn}{⟶} ℂ \to (y \in ℂ ⟼ - y) = (y \in ℂ ⟼ - y)$
6		negeq	$⊢ y = F (x) \to - y = - F (x)$
7	3 4 5 6	fmptco	$⊢ F : A \underset{cn}{⟶} ℂ \to (y \in ℂ ⟼ - y) \circ F = (x \in A ⟼ - F (x))$
8	7 1	eqtr4di	$⊢ F : A \underset{cn}{⟶} ℂ \to (y \in ℂ ⟼ - y) \circ F = G$
9		id	$⊢ F : A \underset{cn}{⟶} ℂ \to F : A \underset{cn}{⟶} ℂ$
10		ssid	$⊢ ℂ \subseteq ℂ$
11		eqid	$⊢ (y \in ℂ ⟼ - y) = (y \in ℂ ⟼ - y)$
12	11	negcncf	$⊢ ℂ \subseteq ℂ \to (y \in ℂ ⟼ - y) : ℂ \underset{cn}{⟶} ℂ$
13	10 12	mp1i	$⊢ F : A \underset{cn}{⟶} ℂ \to (y \in ℂ ⟼ - y) : ℂ \underset{cn}{⟶} ℂ$
14	9 13	cncfco	$⊢ F : A \underset{cn}{⟶} ℂ \to ((y \in ℂ ⟼ - y) \circ F) : A \underset{cn}{⟶} ℂ$
15	8 14	eqeltrrd	$⊢ F : A \underset{cn}{⟶} ℂ \to G : A \underset{cn}{⟶} ℂ$