Theorem cncfcn

Description: Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015)

	Ref	Expression
Hypotheses	cncfcn.2	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	cncfcn.3	$$⊢K=J{\upharpoonright }_{𝑡}A$$
	cncfcn.4	$$⊢L=J{\upharpoonright }_{𝑡}B$$
Assertion	cncfcn	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to A\underset{cn}{⟶}B=K\mathrm{Cn}L$$

Proof

Step	Hyp	Ref	Expression
1		cncfcn.2	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		cncfcn.3	$$⊢K=J{\upharpoonright }_{𝑡}A$$
3		cncfcn.4	$$⊢L=J{\upharpoonright }_{𝑡}B$$
4		eqid	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}$$
5		eqid	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(B\times B\right)}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(B\times B\right)}$$
6		eqid	$$⊢\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}\right)=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}\right)$$
7		eqid	$$⊢\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(B\times B\right)}\right)=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(B\times B\right)}\right)$$
8	4 5 6 7	cncfmet	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to A\underset{cn}{⟶}B=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}\right)\mathrm{Cn}\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(B\times B\right)}\right)$$
9		cnxmet	$$⊢\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$$
10		simpl	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to A\subseteq ℂ$$
11	1	cnfldtopn	$$⊢J=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$$
12	4 11 6	metrest	$$⊢\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge A\subseteq ℂ\right)\to J{\upharpoonright }_{𝑡}A=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}\right)$$
13	9 10 12	sylancr	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to J{\upharpoonright }_{𝑡}A=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}\right)$$
14	2 13	syl5eq	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to K=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}\right)$$
15		simpr	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to B\subseteq ℂ$$
16	5 11 7	metrest	$$⊢\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge B\subseteq ℂ\right)\to J{\upharpoonright }_{𝑡}B=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(B\times B\right)}\right)$$
17	9 15 16	sylancr	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to J{\upharpoonright }_{𝑡}B=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(B\times B\right)}\right)$$
18	3 17	syl5eq	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to L=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(B\times B\right)}\right)$$
19	14 18	oveq12d	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to K\mathrm{Cn}L=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}\right)\mathrm{Cn}\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(B\times B\right)}\right)$$
20	8 19	eqtr4d	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to A\underset{cn}{⟶}B=K\mathrm{Cn}L$$