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	$⊢ C = {(abs \circ -) ↾}_{(A \times A)}$
	cncfmet.2	$⊢ D = {(abs \circ -) ↾}_{(B \times B)}$
	cncfmet.3	$⊢ J = MetOpen (C)$
	cncfmet.4	$⊢ K = MetOpen (D)$
Assertion	cncfmet	$⊢ (A \subseteq ℂ \land B \subseteq ℂ) \to A \underset{cn}{⟶} B = J Cn K$

Proof

Step	Hyp	Ref	Expression
1		cncfmet.1	$⊢ C = {(abs \circ -) ↾}_{(A \times A)}$
2		cncfmet.2	$⊢ D = {(abs \circ -) ↾}_{(B \times B)}$
3		cncfmet.3	$⊢ J = MetOpen (C)$
4		cncfmet.4	$⊢ K = MetOpen (D)$
5		simplll	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to A \subseteq ℂ$
6		simprl	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to x \in A$
7		simprr	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to w \in A$
8	1	oveqi	$⊢ x C w = x ({(abs \circ -) ↾}_{(A \times A)}) w$
9		ovres	$⊢ (x \in A \land w \in A) \to x ({(abs \circ -) ↾}_{(A \times A)}) w = x (abs \circ -) w$
10	8 9	syl5eq	$⊢ (x \in A \land w \in A) \to x C w = x (abs \circ -) w$
11	10	ad2ant2l	$⊢ ((A \subseteq ℂ \land x \in A) \land (A \subseteq ℂ \land w \in A)) \to x C w = x (abs \circ -) w$
12		ssel2	$⊢ (A \subseteq ℂ \land x \in A) \to x \in ℂ$
13		ssel2	$⊢ (A \subseteq ℂ \land w \in A) \to w \in ℂ$
14		eqid	$⊢ abs \circ - = abs \circ -$
15	14	cnmetdval	$⊢ (x \in ℂ \land w \in ℂ) \to x (abs \circ -) w = \|x - w\|$
16	12 13 15	syl2an	$⊢ ((A \subseteq ℂ \land x \in A) \land (A \subseteq ℂ \land w \in A)) \to x (abs \circ -) w = \|x - w\|$
17	11 16	eqtrd	$⊢ ((A \subseteq ℂ \land x \in A) \land (A \subseteq ℂ \land w \in A)) \to x C w = \|x - w\|$
18	5 6 5 7 17	syl22anc	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to x C w = \|x - w\|$
19	18	breq1d	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to (x C w < z \leftrightarrow \|x - w\| < z)$
20		ffvelrn	$⊢ (f : A ⟶ B \land x \in A) \to f (x) \in B$
21	20	ad2ant2lr	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to f (x) \in B$
22		ffvelrn	$⊢ (f : A ⟶ B \land w \in A) \to f (w) \in B$
23	22	ad2ant2l	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to f (w) \in B$
24	2	oveqi	$⊢ f (x) D f (w) = f (x) ({(abs \circ -) ↾}_{(B \times B)}) f (w)$
25		ovres	$⊢ (f (x) \in B \land f (w) \in B) \to f (x) ({(abs \circ -) ↾}_{(B \times B)}) f (w) = f (x) (abs \circ -) f (w)$
26	24 25	syl5eq	$⊢ (f (x) \in B \land f (w) \in B) \to f (x) D f (w) = f (x) (abs \circ -) f (w)$
27	21 23 26	syl2anc	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to f (x) D f (w) = f (x) (abs \circ -) f (w)$
28		simpllr	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to B \subseteq ℂ$
29	28 21	sseldd	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to f (x) \in ℂ$
30	28 23	sseldd	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to f (w) \in ℂ$
31	14	cnmetdval	$⊢ (f (x) \in ℂ \land f (w) \in ℂ) \to f (x) (abs \circ -) f (w) = \|f (x) - f (w)\|$
32	29 30 31	syl2anc	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to f (x) (abs \circ -) f (w) = \|f (x) - f (w)\|$
33	27 32	eqtrd	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to f (x) D f (w) = \|f (x) - f (w)\|$
34	33	breq1d	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to (f (x) D f (w) < y \leftrightarrow \|f (x) - f (w)\| < y)$
35	19 34	imbi12d	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land (x \in A \land w \in A)) \to ((x C w < z \to f (x) D f (w) < y) \leftrightarrow (\|x - w\| < z \to \|f (x) - f (w)\| < y))$
36	35	anassrs	$⊢ ((((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land x \in A) \land w \in A) \to ((x C w < z \to f (x) D f (w) < y) \leftrightarrow (\|x - w\| < z \to \|f (x) - f (w)\| < y))$
37	36	ralbidva	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land x \in A) \to (\forall w \in A (x C w < z \to f (x) D f (w) < y) \leftrightarrow \forall w \in A (\|x - w\| < z \to \|f (x) - f (w)\| < y))$
38	37	rexbidv	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land x \in A) \to (\exists z \in ℝ^{+} \forall w \in A (x C w < z \to f (x) D f (w) < y) \leftrightarrow \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|f (x) - f (w)\| < y))$
39	38	ralbidv	$⊢ (((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \land x \in A) \to (\forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (x C w < z \to f (x) D f (w) < y) \leftrightarrow \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|f (x) - f (w)\| < y))$
40	39	ralbidva	$⊢ ((A \subseteq ℂ \land B \subseteq ℂ) \land f : A ⟶ B) \to (\forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (x C w < z \to f (x) D f (w) < y) \leftrightarrow \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|f (x) - f (w)\| < y))$
41	40	pm5.32da	$⊢ (A \subseteq ℂ \land B \subseteq ℂ) \to ((f : A ⟶ B \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (x C w < z \to f (x) D f (w) < y)) \leftrightarrow (f : A ⟶ B \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|f (x) - f (w)\| < y)))$
42		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
43		xmetres2	$⊢ (abs \circ - \in ∞Met (ℂ) \land A \subseteq ℂ) \to {(abs \circ -) ↾}_{(A \times A)} \in ∞Met (A)$
44	42 43	mpan	$⊢ A \subseteq ℂ \to {(abs \circ -) ↾}_{(A \times A)} \in ∞Met (A)$
45	1 44	eqeltrid	$⊢ A \subseteq ℂ \to C \in ∞Met (A)$
46		xmetres2	$⊢ (abs \circ - \in ∞Met (ℂ) \land B \subseteq ℂ) \to {(abs \circ -) ↾}_{(B \times B)} \in ∞Met (B)$
47	42 46	mpan	$⊢ B \subseteq ℂ \to {(abs \circ -) ↾}_{(B \times B)} \in ∞Met (B)$
48	2 47	eqeltrid	$⊢ B \subseteq ℂ \to D \in ∞Met (B)$
49	3 4	metcn	$⊢ (C \in ∞Met (A) \land D \in ∞Met (B)) \to (f \in (J Cn K) \leftrightarrow (f : A ⟶ B \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (x C w < z \to f (x) D f (w) < y)))$
50	45 48 49	syl2an	$⊢ (A \subseteq ℂ \land B \subseteq ℂ) \to (f \in (J Cn K) \leftrightarrow (f : A ⟶ B \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (x C w < z \to f (x) D f (w) < y)))$
51		elcncf	$⊢ (A \subseteq ℂ \land B \subseteq ℂ) \to (f : A \underset{cn}{⟶} B \leftrightarrow (f : A ⟶ B \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|f (x) - f (w)\| < y)))$
52	41 50 51	3bitr4rd	$⊢ (A \subseteq ℂ \land B \subseteq ℂ) \to (f : A \underset{cn}{⟶} B \leftrightarrow f \in (J Cn K))$
53	52	eqrdv	$⊢ (A \subseteq ℂ \land B \subseteq ℂ) \to A \underset{cn}{⟶} B = J Cn K$

Metamath Proof Explorer

Theorem cncfmet

Proof