This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑥 𝐶 𝑤 ) = ( 𝑥 ( 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 ffvelcdm ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
21 20 ad2ant2lr ⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
22 ffvelcdm ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑤 ) ∈ 𝐵 )
23 22 ad2ant2l ⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑓 ‘ 𝑤 ) ∈ 𝐵 )
24 2 oveqi ⊢ ( ( 𝑓 ‘ 𝑥 ) 𝐷 ( 𝑓 ‘ 𝑤 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ( 𝑓 ‘ 𝑤 ) )
25 ovres ⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑤 ) ∈ 𝐵 ) → ( ( 𝑓 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ( 𝑓 ‘ 𝑤 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑓 ‘ 𝑤 ) ) )
26 24 25 eqtrid ⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑤 ) ∈ 𝐵 ) → ( ( 𝑓 ‘ 𝑥 ) 𝐷 ( 𝑓 ‘ 𝑤 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 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 𝐾 ) )