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 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
cncfcn.3 ⊢ 𝐾 = ( 𝐽 ↾t 𝐴 )
cncfcn.4 ⊢ 𝐿 = ( 𝐽 ↾t 𝐵 )
Assertion cncfcn ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐴 –cn→ 𝐵 ) = ( 𝐾 Cn 𝐿 ) )

Proof

Step Hyp Ref Expression
1 cncfcn.2 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 cncfcn.3 ⊢ 𝐾 = ( 𝐽 ↾t 𝐴 )
3 cncfcn.4 ⊢ 𝐿 = ( 𝐽 ↾t 𝐵 )
4 eqid ⊢ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) )
5 eqid ⊢ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) )
6 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) )
7 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) )
8 4 5 6 7 cncfmet ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐴 –cn→ 𝐵 ) = ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) Cn ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ) ) )
9 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
10 simpl ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → 𝐴 ⊆ ℂ )
11 1 cnfldtopn ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
12 4 11 6 metrest ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐴 ⊆ ℂ ) → ( 𝐽 ↾t 𝐴 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) )
13 9 10 12 sylancr ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐽 ↾t 𝐴 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) )
14 2 13 syl5eq ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → 𝐾 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) )
15 simpr ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → 𝐵 ⊆ ℂ )
16 5 11 7 metrest ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐵 ⊆ ℂ ) → ( 𝐽 ↾t 𝐵 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ) )
17 9 15 16 sylancr ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐽 ↾t 𝐵 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ) )
18 3 17 syl5eq ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → 𝐿 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ) )
19 14 18 oveq12d ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐾 Cn 𝐿 ) = ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) Cn ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ) ) )
20 8 19 eqtr4d ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐴 –cn→ 𝐵 ) = ( 𝐾 Cn 𝐿 ) )