Metamath Proof Explorer


Theorem cncfmet

Description: Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007) (Revised by Mario Carneiro, 7-Sep-2015)

Ref Expression
Hypotheses cncfmet.1 𝐶 = ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) )
cncfmet.2 𝐷 = ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) )
cncfmet.3 𝐽 = ( MetOpen ‘ 𝐶 )
cncfmet.4 𝐾 = ( MetOpen ‘ 𝐷 )
Assertion cncfmet ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐴cn𝐵 ) = ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 cncfmet.1 𝐶 = ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) )
2 cncfmet.2 𝐷 = ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) )
3 cncfmet.3 𝐽 = ( MetOpen ‘ 𝐶 )
4 cncfmet.4 𝐾 = ( MetOpen ‘ 𝐷 )
5 simplll ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → 𝐴 ⊆ ℂ )
6 simprl ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → 𝑥𝐴 )
7 simprr ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → 𝑤𝐴 )
8 1 oveqi ( 𝑥 𝐶 𝑤 ) = ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 𝑤 )
9 ovres ( ( 𝑥𝐴𝑤𝐴 ) → ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 𝑤 ) = ( 𝑥 ( abs ∘ − ) 𝑤 ) )
10 8 9 syl5eq ( ( 𝑥𝐴𝑤𝐴 ) → ( 𝑥 𝐶 𝑤 ) = ( 𝑥 ( abs ∘ − ) 𝑤 ) )
11 10 ad2ant2l ( ( ( 𝐴 ⊆ ℂ ∧ 𝑥𝐴 ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑤𝐴 ) ) → ( 𝑥 𝐶 𝑤 ) = ( 𝑥 ( abs ∘ − ) 𝑤 ) )
12 ssel2 ( ( 𝐴 ⊆ ℂ ∧ 𝑥𝐴 ) → 𝑥 ∈ ℂ )
13 ssel2 ( ( 𝐴 ⊆ ℂ ∧ 𝑤𝐴 ) → 𝑤 ∈ ℂ )
14 eqid ( abs ∘ − ) = ( abs ∘ − )
15 14 cnmetdval ( ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 𝑤 ) = ( abs ‘ ( 𝑥𝑤 ) ) )
16 12 13 15 syl2an ( ( ( 𝐴 ⊆ ℂ ∧ 𝑥𝐴 ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑤𝐴 ) ) → ( 𝑥 ( abs ∘ − ) 𝑤 ) = ( abs ‘ ( 𝑥𝑤 ) ) )
17 11 16 eqtrd ( ( ( 𝐴 ⊆ ℂ ∧ 𝑥𝐴 ) ∧ ( 𝐴 ⊆ ℂ ∧ 𝑤𝐴 ) ) → ( 𝑥 𝐶 𝑤 ) = ( abs ‘ ( 𝑥𝑤 ) ) )
18 5 6 5 7 17 syl22anc ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( 𝑥 𝐶 𝑤 ) = ( abs ‘ ( 𝑥𝑤 ) ) )
19 18 breq1d ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( ( 𝑥 𝐶 𝑤 ) < 𝑧 ↔ ( abs ‘ ( 𝑥𝑤 ) ) < 𝑧 ) )
20 ffvelrn ( ( 𝑓 : 𝐴𝐵𝑥𝐴 ) → ( 𝑓𝑥 ) ∈ 𝐵 )
21 20 ad2ant2lr ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( 𝑓𝑥 ) ∈ 𝐵 )
22 ffvelrn ( ( 𝑓 : 𝐴𝐵𝑤𝐴 ) → ( 𝑓𝑤 ) ∈ 𝐵 )
23 22 ad2ant2l ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( 𝑓𝑤 ) ∈ 𝐵 )
24 2 oveqi ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) = ( ( 𝑓𝑥 ) ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ( 𝑓𝑤 ) )
25 ovres ( ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑓𝑤 ) ∈ 𝐵 ) → ( ( 𝑓𝑥 ) ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ( 𝑓𝑤 ) ) = ( ( 𝑓𝑥 ) ( abs ∘ − ) ( 𝑓𝑤 ) ) )
26 24 25 syl5eq ( ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑓𝑤 ) ∈ 𝐵 ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) = ( ( 𝑓𝑥 ) ( abs ∘ − ) ( 𝑓𝑤 ) ) )
27 21 23 26 syl2anc ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) = ( ( 𝑓𝑥 ) ( abs ∘ − ) ( 𝑓𝑤 ) ) )
28 simpllr ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → 𝐵 ⊆ ℂ )
29 28 21 sseldd ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( 𝑓𝑥 ) ∈ ℂ )
30 28 23 sseldd ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( 𝑓𝑤 ) ∈ ℂ )
31 14 cnmetdval ( ( ( 𝑓𝑥 ) ∈ ℂ ∧ ( 𝑓𝑤 ) ∈ ℂ ) → ( ( 𝑓𝑥 ) ( abs ∘ − ) ( 𝑓𝑤 ) ) = ( abs ‘ ( ( 𝑓𝑥 ) − ( 𝑓𝑤 ) ) ) )
32 29 30 31 syl2anc ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( ( 𝑓𝑥 ) ( abs ∘ − ) ( 𝑓𝑤 ) ) = ( abs ‘ ( ( 𝑓𝑥 ) − ( 𝑓𝑤 ) ) ) )
33 27 32 eqtrd ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) = ( abs ‘ ( ( 𝑓𝑥 ) − ( 𝑓𝑤 ) ) ) )
34 33 breq1d ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝑓𝑥 ) − ( 𝑓𝑤 ) ) ) < 𝑦 ) )
35 19 34 imbi12d ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ ( 𝑥𝐴𝑤𝐴 ) ) → ( ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑥𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓𝑥 ) − ( 𝑓𝑤 ) ) ) < 𝑦 ) ) )
36 35 anassrs ( ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ 𝑥𝐴 ) ∧ 𝑤𝐴 ) → ( ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑥𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓𝑥 ) − ( 𝑓𝑤 ) ) ) < 𝑦 ) ) )
37 36 ralbidva ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ 𝑥𝐴 ) → ( ∀ 𝑤𝐴 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑤𝐴 ( ( abs ‘ ( 𝑥𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓𝑥 ) − ( 𝑓𝑤 ) ) ) < 𝑦 ) ) )
38 37 rexbidv ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ 𝑥𝐴 ) → ( ∃ 𝑧 ∈ ℝ+𝑤𝐴 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ↔ ∃ 𝑧 ∈ ℝ+𝑤𝐴 ( ( abs ‘ ( 𝑥𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓𝑥 ) − ( 𝑓𝑤 ) ) ) < 𝑦 ) ) )
39 38 ralbidv ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) ∧ 𝑥𝐴 ) → ( ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ( ( abs ‘ ( 𝑥𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓𝑥 ) − ( 𝑓𝑤 ) ) ) < 𝑦 ) ) )
40 39 ralbidva ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴𝐵 ) → ( ∀ 𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ( ( abs ‘ ( 𝑥𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓𝑥 ) − ( 𝑓𝑤 ) ) ) < 𝑦 ) ) )
41 40 pm5.32da ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( ( 𝑓 : 𝐴𝐵 ∧ ∀ 𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ) ↔ ( 𝑓 : 𝐴𝐵 ∧ ∀ 𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ( ( abs ‘ ( 𝑥𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓𝑥 ) − ( 𝑓𝑤 ) ) ) < 𝑦 ) ) ) )
42 cnxmet ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
43 xmetres2 ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐴 ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( ∞Met ‘ 𝐴 ) )
44 42 43 mpan ( 𝐴 ⊆ ℂ → ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( ∞Met ‘ 𝐴 ) )
45 1 44 eqeltrid ( 𝐴 ⊆ ℂ → 𝐶 ∈ ( ∞Met ‘ 𝐴 ) )
46 xmetres2 ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐵 ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ∈ ( ∞Met ‘ 𝐵 ) )
47 42 46 mpan ( 𝐵 ⊆ ℂ → ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ∈ ( ∞Met ‘ 𝐵 ) )
48 2 47 eqeltrid ( 𝐵 ⊆ ℂ → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
49 3 4 metcn ( ( 𝐶 ∈ ( ∞Met ‘ 𝐴 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑓 : 𝐴𝐵 ∧ ∀ 𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ) ) )
50 45 48 49 syl2an ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑓 : 𝐴𝐵 ∧ ∀ 𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ) ) )
51 elcncf ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝑓 ∈ ( 𝐴cn𝐵 ) ↔ ( 𝑓 : 𝐴𝐵 ∧ ∀ 𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ( ( abs ‘ ( 𝑥𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓𝑥 ) − ( 𝑓𝑤 ) ) ) < 𝑦 ) ) ) )
52 41 50 51 3bitr4rd ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝑓 ∈ ( 𝐴cn𝐵 ) ↔ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) )
53 52 eqrdv ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐴cn𝐵 ) = ( 𝐽 Cn 𝐾 ) )