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		ffvelrn	⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
21	20	ad2ant2lr	⊢ ( ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) ∧ 𝑓 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
22		ffvelrn	⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑤 ) ∈ 𝐵 )
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 𝐾 ) )