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

Metamath Proof Explorer

Theorem cncfcdm

Description: Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007) (Revised by Mario Carneiro, 1-May-2015)

		Ref	Expression
	Assertion	cncfcdm	$⊢ (C \subseteq ℂ \land F : A \underset{cn}{⟶} B) \to (F : A \underset{cn}{⟶} C \leftrightarrow F : A ⟶ C)$

Proof

Step	Hyp	Ref	Expression
1		cncfi	$⊢ (F : A \underset{cn}{⟶} B \land x \in A \land y \in ℝ^{+}) \to \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|F (w) - F (x)\| < y)$
2	1	3expb	$⊢ (F : A \underset{cn}{⟶} B \land (x \in A \land y \in ℝ^{+})) \to \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|F (w) - F (x)\| < y)$
3	2	ralrimivva	$⊢ F : A \underset{cn}{⟶} B \to \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|F (w) - F (x)\| < y)$
4	3	adantl	$⊢ (C \subseteq ℂ \land F : A \underset{cn}{⟶} B) \to \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|F (w) - F (x)\| < y)$
5		cncfrss	$⊢ F : A \underset{cn}{⟶} B \to A \subseteq ℂ$
6		simpl	$⊢ (C \subseteq ℂ \land F : A \underset{cn}{⟶} B) \to C \subseteq ℂ$
7		elcncf2	$⊢ (A \subseteq ℂ \land C \subseteq ℂ) \to (F : A \underset{cn}{⟶} C \leftrightarrow (F : A ⟶ C \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|F (w) - F (x)\| < y)))$
8	5 6 7	syl2an2	$⊢ (C \subseteq ℂ \land F : A \underset{cn}{⟶} B) \to (F : A \underset{cn}{⟶} C \leftrightarrow (F : A ⟶ C \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|w - x\| < z \to \|F (w) - F (x)\| < y)))$
9	4 8	mpbiran2d	$⊢ (C \subseteq ℂ \land F : A \underset{cn}{⟶} B) \to (F : A \underset{cn}{⟶} C \leftrightarrow F : A ⟶ C)$