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	$$⊢\left(C\subseteq ℂ\wedge F:A\underset{cn}{⟶}B\right)\to \left(F:A\underset{cn}{⟶}C\leftrightarrow F:A⟶C\right)$$

Proof

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