# Metamath Proof Explorer

## 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}{↾}_{𝑡}{A}$
cncfcn.4 ${⊢}{L}={J}{↾}_{𝑡}{B}$
Assertion cncfcn

### Proof

Step Hyp Ref Expression
1 cncfcn.2 ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 cncfcn.3 ${⊢}{K}={J}{↾}_{𝑡}{A}$
3 cncfcn.4 ${⊢}{L}={J}{↾}_{𝑡}{B}$
4 eqid ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{\left({A}×{A}\right)}={\left(\mathrm{abs}\circ -\right)↾}_{\left({A}×{A}\right)}$
5 eqid ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{\left({B}×{B}\right)}={\left(\mathrm{abs}\circ -\right)↾}_{\left({B}×{B}\right)}$
6 eqid ${⊢}\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left({A}×{A}\right)}\right)=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left({A}×{A}\right)}\right)$
7 eqid ${⊢}\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left({B}×{B}\right)}\right)=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left({B}×{B}\right)}\right)$
8 4 5 6 7 cncfmet
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}{↾}_{𝑡}{A}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left({A}×{A}\right)}\right)$
13 9 10 12 sylancr ${⊢}\left({A}\subseteq ℂ\wedge {B}\subseteq ℂ\right)\to {J}{↾}_{𝑡}{A}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left({A}×{A}\right)}\right)$
14 2 13 syl5eq ${⊢}\left({A}\subseteq ℂ\wedge {B}\subseteq ℂ\right)\to {K}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left({A}×{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}{↾}_{𝑡}{B}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left({B}×{B}\right)}\right)$
17 9 15 16 sylancr ${⊢}\left({A}\subseteq ℂ\wedge {B}\subseteq ℂ\right)\to {J}{↾}_{𝑡}{B}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left({B}×{B}\right)}\right)$
18 3 17 syl5eq ${⊢}\left({A}\subseteq ℂ\wedge {B}\subseteq ℂ\right)\to {L}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left({B}×{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)↾}_{\left({A}×{A}\right)}\right)\mathrm{Cn}\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left({B}×{B}\right)}\right)$
20 8 19 eqtr4d