dvlip2

	Ref	Expression
Hypotheses	dvlip2.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvlip2.j	$⊢ J = {(abs \circ -) ↾}_{(S \times S)}$
	dvlip2.x	$⊢ φ \to X \subseteq S$
	dvlip2.f	$⊢ φ \to F : X ⟶ ℂ$
	dvlip2.a	$⊢ φ \to A \in S$
	dvlip2.r	$⊢ φ \to R \in ℝ^{*}$
	dvlip2.b	$⊢ B = A ball (J) R$
	dvlip2.d	$⊢ φ \to B \subseteq dom F_{S}^{'}$
	dvlip2.m	$⊢ φ \to M \in ℝ$
	dvlip2.l	$⊢ (φ \land x \in B) \to \|F_{S}^{'} (x)\| \leq M$
Assertion	dvlip2	$⊢ (φ \land (Y \in B \land Z \in B)) \to \|F (Y) - F (Z)\| \leq M \|Y - Z\|$

Proof

Step	Hyp	Ref	Expression
1		dvlip2.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvlip2.j	$⊢ J = {(abs \circ -) ↾}_{(S \times S)}$
3		dvlip2.x	$⊢ φ \to X \subseteq S$
4		dvlip2.f	$⊢ φ \to F : X ⟶ ℂ$
5		dvlip2.a	$⊢ φ \to A \in S$
6		dvlip2.r	$⊢ φ \to R \in ℝ^{*}$
7		dvlip2.b	$⊢ B = A ball (J) R$
8		dvlip2.d	$⊢ φ \to B \subseteq dom F_{S}^{'}$
9		dvlip2.m	$⊢ φ \to M \in ℝ$
10		dvlip2.l	$⊢ (φ \land x \in B) \to \|F_{S}^{'} (x)\| \leq M$
11		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
12		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
13	1 12	syl	$⊢ φ \to S \subseteq ℂ$
14		xmetres2	$⊢ (abs \circ - \in ∞Met (ℂ) \land S \subseteq ℂ) \to {(abs \circ -) ↾}_{(S \times S)} \in ∞Met (S)$
15	11 13 14	sylancr	$⊢ φ \to {(abs \circ -) ↾}_{(S \times S)} \in ∞Met (S)$
16	2 15	eqeltrid	$⊢ φ \to J \in ∞Met (S)$
17	16	ad2antrr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to J \in ∞Met (S)$
18	5	ad2antrr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to A \in S$
19		simplrr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to Z \in B$
20	19 7	eleqtrdi	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to Z \in (A ball (J) R)$
21	6	ad2antrr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to R \in ℝ^{*}$
22		elbl	$⊢ (J \in ∞Met (S) \land A \in S \land R \in ℝ^{*}) \to (Z \in (A ball (J) R) \leftrightarrow (Z \in S \land A J Z < R))$
23	17 18 21 22	syl3anc	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to (Z \in (A ball (J) R) \leftrightarrow (Z \in S \land A J Z < R))$
24	20 23	mpbid	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to (Z \in S \land A J Z < R)$
25	24	simpld	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to Z \in S$
26		xmetcl	$⊢ (J \in ∞Met (S) \land A \in S \land Z \in S) \to A J Z \in ℝ^{*}$
27	17 18 25 26	syl3anc	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to A J Z \in ℝ^{*}$
28		simplrl	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to Y \in B$
29	28 7	eleqtrdi	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to Y \in (A ball (J) R)$
30		elbl	$⊢ (J \in ∞Met (S) \land A \in S \land R \in ℝ^{*}) \to (Y \in (A ball (J) R) \leftrightarrow (Y \in S \land A J Y < R))$
31	17 18 21 30	syl3anc	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to (Y \in (A ball (J) R) \leftrightarrow (Y \in S \land A J Y < R))$
32	29 31	mpbid	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to (Y \in S \land A J Y < R)$
33	32	simpld	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to Y \in S$
34		xmetcl	$⊢ (J \in ∞Met (S) \land A \in S \land Y \in S) \to A J Y \in ℝ^{*}$
35	17 18 33 34	syl3anc	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to A J Y \in ℝ^{*}$
36	27 35	ifcld	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to if (A J Y \leq A J Z, A J Z, A J Y) \in ℝ^{*}$
37	24	simprd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to A J Z < R$
38	32	simprd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to A J Y < R$
39		breq1	$⊢ A J Z = if (A J Y \leq A J Z, A J Z, A J Y) \to (A J Z < R \leftrightarrow if (A J Y \leq A J Z, A J Z, A J Y) < R)$
40		breq1	$⊢ A J Y = if (A J Y \leq A J Z, A J Z, A J Y) \to (A J Y < R \leftrightarrow if (A J Y \leq A J Z, A J Z, A J Y) < R)$
41	39 40	ifboth	$⊢ (A J Z < R \land A J Y < R) \to if (A J Y \leq A J Z, A J Z, A J Y) < R$
42	37 38 41	syl2anc	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to if (A J Y \leq A J Z, A J Z, A J Y) < R$
43		qbtwnxr	$⊢ (if (A J Y \leq A J Z, A J Z, A J Y) \in ℝ^{} \land R \in ℝ^{} \land if (A J Y \leq A J Z, A J Z, A J Y) < R) \to \exists r \in ℚ (if (A J Y \leq A J Z, A J Z, A J Y) < r \land r < R)$
44	36 21 42 43	syl3anc	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to \exists r \in ℚ (if (A J Y \leq A J Z, A J Z, A J Y) < r \land r < R)$
45		qre	$⊢ r \in ℚ \to r \in ℝ$
46		rexr	$⊢ r \in ℝ \to r \in ℝ^{*}$
47		xrmaxlt	$⊢ (A J Y \in ℝ^{} \land A J Z \in ℝ^{} \land r \in ℝ^{*}) \to (if (A J Y \leq A J Z, A J Z, A J Y) < r \leftrightarrow (A J Y < r \land A J Z < r))$
48	35 27 46 47	syl2an3an	$⊢ (((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \to (if (A J Y \leq A J Z, A J Z, A J Y) < r \leftrightarrow (A J Y < r \land A J Z < r))$
49		ioossicc	$⊢ (A - r, A + r) \subseteq [A - r, A + r]$
50		simpr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to S = ℝ$
51	33 50	eleqtrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to Y \in ℝ$
52	51	ad2antrr	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to Y \in ℝ$
53		xmetsym	$⊢ (J \in ∞Met (S) \land A \in S \land Y \in S) \to A J Y = Y J A$
54	17 18 33 53	syl3anc	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to A J Y = Y J A$
55	50	sqxpeqd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to S \times S = ℝ^{2}$
56	55	reseq2d	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to {(abs \circ -) ↾}_{(S \times S)} = {(abs \circ -) ↾}_{ℝ^{2}}$
57	2 56	syl5eq	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to J = {(abs \circ -) ↾}_{ℝ^{2}}$
58	57	oveqd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to Y J A = Y ({(abs \circ -) ↾}_{ℝ^{2}}) A$
59	18 50	eleqtrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to A \in ℝ$
60		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
61	60	remetdval	$⊢ (Y \in ℝ \land A \in ℝ) \to Y ({(abs \circ -) ↾}_{ℝ^{2}}) A = \|Y - A\|$
62	51 59 61	syl2anc	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to Y ({(abs \circ -) ↾}_{ℝ^{2}}) A = \|Y - A\|$
63	54 58 62	3eqtrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to A J Y = \|Y - A\|$
64	63	ad2antrr	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to A J Y = \|Y - A\|$
65		simprll	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to A J Y < r$
66	64 65	eqbrtrrd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to \|Y - A\| < r$
67	59	ad2antrr	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to A \in ℝ$
68		simplr	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to r \in ℝ$
69	52 67 68	absdifltd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to (\|Y - A\| < r \leftrightarrow (A - r < Y \land Y < A + r))$
70	66 69	mpbid	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to (A - r < Y \land Y < A + r)$
71	70	simpld	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to A - r < Y$
72	70	simprd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to Y < A + r$
73	67 68	resubcld	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to A - r \in ℝ$
74	73	rexrd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to A - r \in ℝ^{*}$
75	67 68	readdcld	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to A + r \in ℝ$
76	75	rexrd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to A + r \in ℝ^{*}$
77		elioo2	$⊢ (A - r \in ℝ^{} \land A + r \in ℝ^{}) \to (Y \in (A - r, A + r) \leftrightarrow (Y \in ℝ \land A - r < Y \land Y < A + r))$
78	74 76 77	syl2anc	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to (Y \in (A - r, A + r) \leftrightarrow (Y \in ℝ \land A - r < Y \land Y < A + r))$
79	52 71 72 78	mpbir3and	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to Y \in (A - r, A + r)$
80	49 79	sselid	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to Y \in [A - r, A + r]$
81	80	fvresd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to ({F ↾}_{[A - r, A + r]}) (Y) = F (Y)$
82	25 50	eleqtrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to Z \in ℝ$
83	82	ad2antrr	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to Z \in ℝ$
84		xmetsym	$⊢ (J \in ∞Met (S) \land A \in S \land Z \in S) \to A J Z = Z J A$
85	17 18 25 84	syl3anc	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to A J Z = Z J A$
86	57	oveqd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to Z J A = Z ({(abs \circ -) ↾}_{ℝ^{2}}) A$
87	60	remetdval	$⊢ (Z \in ℝ \land A \in ℝ) \to Z ({(abs \circ -) ↾}_{ℝ^{2}}) A = \|Z - A\|$
88	82 59 87	syl2anc	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to Z ({(abs \circ -) ↾}_{ℝ^{2}}) A = \|Z - A\|$
89	85 86 88	3eqtrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to A J Z = \|Z - A\|$
90	89	ad2antrr	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to A J Z = \|Z - A\|$
91		simprlr	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to A J Z < r$
92	90 91	eqbrtrrd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to \|Z - A\| < r$
93	83 67 68	absdifltd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to (\|Z - A\| < r \leftrightarrow (A - r < Z \land Z < A + r))$
94	92 93	mpbid	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to (A - r < Z \land Z < A + r)$
95	94	simpld	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to A - r < Z$
96	94	simprd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to Z < A + r$
97		elioo2	$⊢ (A - r \in ℝ^{} \land A + r \in ℝ^{}) \to (Z \in (A - r, A + r) \leftrightarrow (Z \in ℝ \land A - r < Z \land Z < A + r))$
98	74 76 97	syl2anc	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to (Z \in (A - r, A + r) \leftrightarrow (Z \in ℝ \land A - r < Z \land Z < A + r))$
99	83 95 96 98	mpbir3and	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to Z \in (A - r, A + r)$
100	49 99	sselid	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to Z \in [A - r, A + r]$
101	100	fvresd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to ({F ↾}_{[A - r, A + r]}) (Z) = F (Z)$
102	81 101	oveq12d	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to ({F ↾}_{[A - r, A + r]}) (Y) - ({F ↾}_{[A - r, A + r]}) (Z) = F (Y) - F (Z)$
103	102	fveq2d	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to \|({F ↾}_{[A - r, A + r]}) (Y) - ({F ↾}_{[A - r, A + r]}) (Z)\| = \|F (Y) - F (Z)\|$
104	17	ad3antrrr	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to J \in ∞Met (S)$
105		elicc2	$⊢ (A - r \in ℝ \land A + r \in ℝ) \to (x \in [A - r, A + r] \leftrightarrow (x \in ℝ \land A - r \leq x \land x \leq A + r))$
106	73 75 105	syl2anc	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to (x \in [A - r, A + r] \leftrightarrow (x \in ℝ \land A - r \leq x \land x \leq A + r))$
107	106	biimpa	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to (x \in ℝ \land A - r \leq x \land x \leq A + r)$
108	107	simp1d	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to x \in ℝ$
109	50	ad3antrrr	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to S = ℝ$
110	108 109	eleqtrrd	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to x \in S$
111	18	ad3antrrr	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to A \in S$
112		xmetcl	$⊢ (J \in ∞Met (S) \land x \in S \land A \in S) \to x J A \in ℝ^{*}$
113	104 110 111 112	syl3anc	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to x J A \in ℝ^{*}$
114	68	adantr	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to r \in ℝ$
115	114	rexrd	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to r \in ℝ^{*}$
116	21	ad3antrrr	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to R \in ℝ^{*}$
117	57	ad3antrrr	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to J = {(abs \circ -) ↾}_{ℝ^{2}}$
118	117	oveqd	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to x J A = x ({(abs \circ -) ↾}_{ℝ^{2}}) A$
119	67	adantr	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to A \in ℝ$
120	60	remetdval	$⊢ (x \in ℝ \land A \in ℝ) \to x ({(abs \circ -) ↾}_{ℝ^{2}}) A = \|x - A\|$
121	108 119 120	syl2anc	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to x ({(abs \circ -) ↾}_{ℝ^{2}}) A = \|x - A\|$
122	118 121	eqtrd	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to x J A = \|x - A\|$
123	107	simp2d	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to A - r \leq x$
124	107	simp3d	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to x \leq A + r$
125	108 119 114	absdifled	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to (\|x - A\| \leq r \leftrightarrow (A - r \leq x \land x \leq A + r))$
126	123 124 125	mpbir2and	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to \|x - A\| \leq r$
127	122 126	eqbrtrd	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to x J A \leq r$
128		simplrr	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to r < R$
129	113 115 116 127 128	xrlelttrd	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to x J A < R$
130		elbl3	$⊢ ((J \in ∞Met (S) \land R \in ℝ^{*}) \land (A \in S \land x \in S)) \to (x \in (A ball (J) R) \leftrightarrow x J A < R)$
131	104 116 111 110 130	syl22anc	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to (x \in (A ball (J) R) \leftrightarrow x J A < R)$
132	129 131	mpbird	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in [A - r, A + r]) \to x \in (A ball (J) R)$
133	132	ex	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to (x \in [A - r, A + r] \to x \in (A ball (J) R))$
134	133	ssrdv	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to [A - r, A + r] \subseteq A ball (J) R$
135	134 7	sseqtrrdi	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to [A - r, A + r] \subseteq B$
136	135	resabs1d	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to {({F ↾}_{B}) ↾}_{[A - r, A + r]} = {F ↾}_{[A - r, A + r]}$
137		ax-resscn	$⊢ ℝ \subseteq ℂ$
138	137	a1i	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to ℝ \subseteq ℂ$
139	4	ad4antr	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to F : X ⟶ ℂ$
140	13 4 3	dvbss	$⊢ φ \to dom F_{S}^{'} \subseteq X$
141	8 140	sstrd	$⊢ φ \to B \subseteq X$
142	141	ad4antr	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to B \subseteq X$
143	139 142	fssresd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to ({F ↾}_{B}) : B ⟶ ℂ$
144		blssm	$⊢ (J \in ∞Met (S) \land A \in S \land R \in ℝ^{*}) \to A ball (J) R \subseteq S$
145	17 18 21 144	syl3anc	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to A ball (J) R \subseteq S$
146	7 145	eqsstrid	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to B \subseteq S$
147	146 50	sseqtrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to B \subseteq ℝ$
148	147	ad2antrr	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to B \subseteq ℝ$
149	137	a1i	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to ℝ \subseteq ℂ$
150	4	ad2antrr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to F : X ⟶ ℂ$
151	3	ad2antrr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to X \subseteq S$
152	151 50	sseqtrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to X \subseteq ℝ$
153		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
154	153	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
155	153 154	dvres	$⊢ ((ℝ \subseteq ℂ \land F : X ⟶ ℂ) \land (X \subseteq ℝ \land B \subseteq ℝ)) \to ℝ D ({F ↾}_{B}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) (B)}$
156	149 150 152 147 155	syl22anc	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to ℝ D ({F ↾}_{B}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) (B)}$
157		retop	$⊢ topGen (ran (.)) \in Top$
158	57	fveq2d	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to ball (J) = ball ({(abs \circ -) ↾}_{ℝ^{2}})$
159	158	oveqd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to A ball (J) R = A ball ({(abs \circ -) ↾}_{ℝ^{2}}) R$
160	7 159	syl5eq	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to B = A ball ({(abs \circ -) ↾}_{ℝ^{2}}) R$
161	57 17	eqeltrrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (S)$
162		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
163	60 162	tgioo	$⊢ topGen (ran (.)) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
164	163	blopn	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (S) \land A \in S \land R \in ℝ^{*}) \to A ball ({(abs \circ -) ↾}_{ℝ^{2}}) R \in topGen (ran (.))$
165	161 18 21 164	syl3anc	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to A ball ({(abs \circ -) ↾}_{ℝ^{2}}) R \in topGen (ran (.))$
166	160 165	eqeltrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to B \in topGen (ran (.))$
167		isopn3i	$⊢ (topGen (ran (.)) \in Top \land B \in topGen (ran (.))) \to int (topGen (ran (.))) (B) = B$
168	157 166 167	sylancr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to int (topGen (ran (.))) (B) = B$
169	168	reseq2d	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) (B)} = {F_{ℝ}^{'} ↾}_{B}$
170	156 169	eqtrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to ℝ D ({F ↾}_{B}) = {F_{ℝ}^{'} ↾}_{B}$
171	170	dmeqd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to dom {({F ↾}_{B})}_{ℝ}^{'} = dom ({F_{ℝ}^{'} ↾}_{B})$
172		dmres	$⊢ dom ({F_{ℝ}^{'} ↾}_{B}) = B \cap dom F_{ℝ}^{'}$
173	8	ad2antrr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to B \subseteq dom F_{S}^{'}$
174	50	oveq1d	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to S D F = ℝ D F$
175	174	dmeqd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to dom F_{S}^{'} = dom F_{ℝ}^{'}$
176	173 175	sseqtrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to B \subseteq dom F_{ℝ}^{'}$
177		df-ss	$⊢ B \subseteq dom F_{ℝ}^{'} \leftrightarrow B \cap dom F_{ℝ}^{'} = B$
178	176 177	sylib	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to B \cap dom F_{ℝ}^{'} = B$
179	172 178	syl5eq	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to dom ({F_{ℝ}^{'} ↾}_{B}) = B$
180	171 179	eqtrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to dom {({F ↾}_{B})}_{ℝ}^{'} = B$
181	180	ad2antrr	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to dom {({F ↾}_{B})}_{ℝ}^{'} = B$
182		dvcn	$⊢ ((ℝ \subseteq ℂ \land ({F ↾}_{B}) : B ⟶ ℂ \land B \subseteq ℝ) \land dom {({F ↾}_{B})}_{ℝ}^{'} = B) \to ({F ↾}_{B}) : B \underset{cn}{⟶} ℂ$
183	138 143 148 181 182	syl31anc	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to ({F ↾}_{B}) : B \underset{cn}{⟶} ℂ$
184		rescncf	$⊢ [A - r, A + r] \subseteq B \to (({F ↾}_{B}) : B \underset{cn}{⟶} ℂ \to ({({F ↾}_{B}) ↾}_{[A - r, A + r]}) : [A - r, A + r] \underset{cn}{⟶} ℂ)$
185	135 183 184	sylc	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to ({({F ↾}_{B}) ↾}_{[A - r, A + r]}) : [A - r, A + r] \underset{cn}{⟶} ℂ$
186	136 185	eqeltrrd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to ({F ↾}_{[A - r, A + r]}) : [A - r, A + r] \underset{cn}{⟶} ℂ$
187	135 148	sstrd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to [A - r, A + r] \subseteq ℝ$
188	153 154	dvres	$⊢ ((ℝ \subseteq ℂ \land ({F ↾}_{B}) : B ⟶ ℂ) \land (B \subseteq ℝ \land [A - r, A + r] \subseteq ℝ)) \to ℝ D ({({F ↾}_{B}) ↾}_{[A - r, A + r]}) = {{({F ↾}_{B})}_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([A - r, A + r])}$
189	138 143 148 187 188	syl22anc	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to ℝ D ({({F ↾}_{B}) ↾}_{[A - r, A + r]}) = {{({F ↾}_{B})}_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([A - r, A + r])}$
190	136	oveq2d	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to ℝ D ({({F ↾}_{B}) ↾}_{[A - r, A + r]}) = ℝ D ({F ↾}_{[A - r, A + r]})$
191		iccntr	$⊢ (A - r \in ℝ \land A + r \in ℝ) \to int (topGen (ran (.))) ([A - r, A + r]) = (A - r, A + r)$
192	73 75 191	syl2anc	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to int (topGen (ran (.))) ([A - r, A + r]) = (A - r, A + r)$
193	192	reseq2d	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to {{({F ↾}_{B})}_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([A - r, A + r])} = {{({F ↾}_{B})}_{ℝ}^{'} ↾}_{(A - r, A + r)}$
194	189 190 193	3eqtr3d	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to ℝ D ({F ↾}_{[A - r, A + r]}) = {{({F ↾}_{B})}_{ℝ}^{'} ↾}_{(A - r, A + r)}$
195	194	dmeqd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to dom {({F ↾}_{[A - r, A + r]})}_{ℝ}^{'} = dom ({{({F ↾}_{B})}_{ℝ}^{'} ↾}_{(A - r, A + r)})$
196		dmres	$⊢ dom ({{({F ↾}_{B})}_{ℝ}^{'} ↾}_{(A - r, A + r)}) = (A - r, A + r) \cap dom {({F ↾}_{B})}_{ℝ}^{'}$
197	49 135	sstrid	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to (A - r, A + r) \subseteq B$
198	197 181	sseqtrrd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to (A - r, A + r) \subseteq dom {({F ↾}_{B})}_{ℝ}^{'}$
199		df-ss	$⊢ (A - r, A + r) \subseteq dom {({F ↾}_{B})}_{ℝ}^{'} \leftrightarrow (A - r, A + r) \cap dom {({F ↾}_{B})}_{ℝ}^{'} = (A - r, A + r)$
200	198 199	sylib	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to (A - r, A + r) \cap dom {({F ↾}_{B})}_{ℝ}^{'} = (A - r, A + r)$
201	196 200	syl5eq	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to dom ({{({F ↾}_{B})}_{ℝ}^{'} ↾}_{(A - r, A + r)}) = (A - r, A + r)$
202	195 201	eqtrd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to dom {({F ↾}_{[A - r, A + r]})}_{ℝ}^{'} = (A - r, A + r)$
203	9	ad4antr	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to M \in ℝ$
204	194	fveq1d	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to {({F ↾}_{[A - r, A + r]})}_{ℝ}^{'} (x) = ({{({F ↾}_{B})}_{ℝ}^{'} ↾}_{(A - r, A + r)}) (x)$
205		fvres	$⊢ x \in (A - r, A + r) \to ({{({F ↾}_{B})}_{ℝ}^{'} ↾}_{(A - r, A + r)}) (x) = {({F ↾}_{B})}_{ℝ}^{'} (x)$
206	204 205	sylan9eq	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in (A - r, A + r)) \to {({F ↾}_{[A - r, A + r]})}_{ℝ}^{'} (x) = {({F ↾}_{B})}_{ℝ}^{'} (x)$
207	174	reseq1d	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to {F_{S}^{'} ↾}_{B} = {F_{ℝ}^{'} ↾}_{B}$
208	170 207	eqtr4d	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to ℝ D ({F ↾}_{B}) = {F_{S}^{'} ↾}_{B}$
209	208	fveq1d	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to {({F ↾}_{B})}_{ℝ}^{'} (x) = ({F_{S}^{'} ↾}_{B}) (x)$
210	209	ad3antrrr	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in (A - r, A + r)) \to {({F ↾}_{B})}_{ℝ}^{'} (x) = ({F_{S}^{'} ↾}_{B}) (x)$
211	197	sselda	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in (A - r, A + r)) \to x \in B$
212	211	fvresd	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in (A - r, A + r)) \to ({F_{S}^{'} ↾}_{B}) (x) = F_{S}^{'} (x)$
213	206 210 212	3eqtrd	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in (A - r, A + r)) \to {({F ↾}_{[A - r, A + r]})}_{ℝ}^{'} (x) = F_{S}^{'} (x)$
214	213	fveq2d	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in (A - r, A + r)) \to \|{({F ↾}_{[A - r, A + r]})}_{ℝ}^{'} (x)\| = \|F_{S}^{'} (x)\|$
215		simp-4l	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to φ$
216	215 211 10	syl2an2r	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in (A - r, A + r)) \to \|F_{S}^{'} (x)\| \leq M$
217	214 216	eqbrtrd	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land x \in (A - r, A + r)) \to \|{({F ↾}_{[A - r, A + r]})}_{ℝ}^{'} (x)\| \leq M$
218	73 75 186 202 203 217	dvlip	$⊢ (((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \land (Y \in [A - r, A + r] \land Z \in [A - r, A + r])) \to \|({F ↾}_{[A - r, A + r]}) (Y) - ({F ↾}_{[A - r, A + r]}) (Z)\| \leq M \|Y - Z\|$
219	218	ex	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to ((Y \in [A - r, A + r] \land Z \in [A - r, A + r]) \to \|({F ↾}_{[A - r, A + r]}) (Y) - ({F ↾}_{[A - r, A + r]}) (Z)\| \leq M \|Y - Z\|)$
220	80 100 219	mp2and	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to \|({F ↾}_{[A - r, A + r]}) (Y) - ({F ↾}_{[A - r, A + r]}) (Z)\| \leq M \|Y - Z\|$
221	103 220	eqbrtrrd	$⊢ ((((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \land ((A J Y < r \land A J Z < r) \land r < R)) \to \|F (Y) - F (Z)\| \leq M \|Y - Z\|$
222	221	exp32	$⊢ (((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \to ((A J Y < r \land A J Z < r) \to (r < R \to \|F (Y) - F (Z)\| \leq M \|Y - Z\|))$
223	48 222	sylbid	$⊢ (((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \to (if (A J Y \leq A J Z, A J Z, A J Y) < r \to (r < R \to \|F (Y) - F (Z)\| \leq M \|Y - Z\|))$
224	223	impd	$⊢ (((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℝ) \to ((if (A J Y \leq A J Z, A J Z, A J Y) < r \land r < R) \to \|F (Y) - F (Z)\| \leq M \|Y - Z\|)$
225	45 224	sylan2	$⊢ (((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \land r \in ℚ) \to ((if (A J Y \leq A J Z, A J Z, A J Y) < r \land r < R) \to \|F (Y) - F (Z)\| \leq M \|Y - Z\|)$
226	225	rexlimdva	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to (\exists r \in ℚ (if (A J Y \leq A J Z, A J Z, A J Y) < r \land r < R) \to \|F (Y) - F (Z)\| \leq M \|Y - Z\|)$
227	44 226	mpd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℝ) \to \|F (Y) - F (Z)\| \leq M \|Y - Z\|$
228		simpr	$⊢ (φ \land S = ℂ) \to S = ℂ$
229	228	sqxpeqd	$⊢ (φ \land S = ℂ) \to S \times S = ℂ \times ℂ$
230	229	reseq2d	$⊢ (φ \land S = ℂ) \to {(abs \circ -) ↾}_{(S \times S)} = {(abs \circ -) ↾}_{(ℂ \times ℂ)}$
231		absf	$⊢ abs : ℂ ⟶ ℝ$
232		subf	$⊢ - : ℂ \times ℂ ⟶ ℂ$
233		fco	$⊢ (abs : ℂ ⟶ ℝ \land - : ℂ \times ℂ ⟶ ℂ) \to (abs \circ -) : ℂ \times ℂ ⟶ ℝ$
234	231 232 233	mp2an	$⊢ (abs \circ -) : ℂ \times ℂ ⟶ ℝ$
235		ffn	$⊢ (abs \circ -) : ℂ \times ℂ ⟶ ℝ \to (abs \circ -) Fn (ℂ \times ℂ)$
236		fnresdm	$⊢ (abs \circ -) Fn (ℂ \times ℂ) \to {(abs \circ -) ↾}_{(ℂ \times ℂ)} = abs \circ -$
237	234 235 236	mp2b	$⊢ {(abs \circ -) ↾}_{(ℂ \times ℂ)} = abs \circ -$
238	230 237	eqtrdi	$⊢ (φ \land S = ℂ) \to {(abs \circ -) ↾}_{(S \times S)} = abs \circ -$
239	2 238	syl5eq	$⊢ (φ \land S = ℂ) \to J = abs \circ -$
240	239	fveq2d	$⊢ (φ \land S = ℂ) \to ball (J) = ball (abs \circ -)$
241	240	oveqd	$⊢ (φ \land S = ℂ) \to A ball (J) R = A ball (abs \circ -) R$
242	7 241	syl5eq	$⊢ (φ \land S = ℂ) \to B = A ball (abs \circ -) R$
243	242	eleq2d	$⊢ (φ \land S = ℂ) \to (Y \in B \leftrightarrow Y \in (A ball (abs \circ -) R))$
244	242	eleq2d	$⊢ (φ \land S = ℂ) \to (Z \in B \leftrightarrow Z \in (A ball (abs \circ -) R))$
245	243 244	anbi12d	$⊢ (φ \land S = ℂ) \to ((Y \in B \land Z \in B) \leftrightarrow (Y \in (A ball (abs \circ -) R) \land Z \in (A ball (abs \circ -) R)))$
246	245	biimpa	$⊢ ((φ \land S = ℂ) \land (Y \in B \land Z \in B)) \to (Y \in (A ball (abs \circ -) R) \land Z \in (A ball (abs \circ -) R))$
247	3	adantr	$⊢ (φ \land S = ℂ) \to X \subseteq S$
248	247 228	sseqtrd	$⊢ (φ \land S = ℂ) \to X \subseteq ℂ$
249	4	adantr	$⊢ (φ \land S = ℂ) \to F : X ⟶ ℂ$
250	5	adantr	$⊢ (φ \land S = ℂ) \to A \in S$
251	250 228	eleqtrd	$⊢ (φ \land S = ℂ) \to A \in ℂ$
252	6	adantr	$⊢ (φ \land S = ℂ) \to R \in ℝ^{*}$
253		eqid	$⊢ A ball (abs \circ -) R = A ball (abs \circ -) R$
254	8	adantr	$⊢ (φ \land S = ℂ) \to B \subseteq dom F_{S}^{'}$
255	228	oveq1d	$⊢ (φ \land S = ℂ) \to S D F = ℂ D F$
256	255	dmeqd	$⊢ (φ \land S = ℂ) \to dom F_{S}^{'} = dom F_{ℂ}^{'}$
257	254 242 256	3sstr3d	$⊢ (φ \land S = ℂ) \to A ball (abs \circ -) R \subseteq dom F_{ℂ}^{'}$
258	9	adantr	$⊢ (φ \land S = ℂ) \to M \in ℝ$
259	10	ex	$⊢ φ \to (x \in B \to \|F_{S}^{'} (x)\| \leq M)$
260	259	adantr	$⊢ (φ \land S = ℂ) \to (x \in B \to \|F_{S}^{'} (x)\| \leq M)$
261	242	eleq2d	$⊢ (φ \land S = ℂ) \to (x \in B \leftrightarrow x \in (A ball (abs \circ -) R))$
262	255	fveq1d	$⊢ (φ \land S = ℂ) \to F_{S}^{'} (x) = F_{ℂ}^{'} (x)$
263	262	fveq2d	$⊢ (φ \land S = ℂ) \to \|F_{S}^{'} (x)\| = \|F_{ℂ}^{'} (x)\|$
264	263	breq1d	$⊢ (φ \land S = ℂ) \to (\|F_{S}^{'} (x)\| \leq M \leftrightarrow \|F_{ℂ}^{'} (x)\| \leq M)$
265	260 261 264	3imtr3d	$⊢ (φ \land S = ℂ) \to (x \in (A ball (abs \circ -) R) \to \|F_{ℂ}^{'} (x)\| \leq M)$
266	265	imp	$⊢ ((φ \land S = ℂ) \land x \in (A ball (abs \circ -) R)) \to \|F_{ℂ}^{'} (x)\| \leq M$
267	248 249 251 252 253 257 258 266	dvlipcn	$⊢ ((φ \land S = ℂ) \land (Y \in (A ball (abs \circ -) R) \land Z \in (A ball (abs \circ -) R))) \to \|F (Y) - F (Z)\| \leq M \|Y - Z\|$
268	246 267	syldan	$⊢ ((φ \land S = ℂ) \land (Y \in B \land Z \in B)) \to \|F (Y) - F (Z)\| \leq M \|Y - Z\|$
269	268	an32s	$⊢ ((φ \land (Y \in B \land Z \in B)) \land S = ℂ) \to \|F (Y) - F (Z)\| \leq M \|Y - Z\|$
270		elpri	$⊢ S \in \{ℝ, ℂ\} \to (S = ℝ \lor S = ℂ)$
271	1 270	syl	$⊢ φ \to (S = ℝ \lor S = ℂ)$
272	271	adantr	$⊢ (φ \land (Y \in B \land Z \in B)) \to (S = ℝ \lor S = ℂ)$
273	227 269 272	mpjaodan	$⊢ (φ \land (Y \in B \land Z \in B)) \to \|F (Y) - F (Z)\| \leq M \|Y - Z\|$

Metamath Proof Explorer

Theorem dvlip2

Proof