dvlipcn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvlipcn		Structured version Visualization version GIF version

Theorem dvlipcn 26056

Description: A complex function with derivative bounded by 𝑀 on an open ball is 𝑀-Lipschitz continuous. (Contributed by Mario Carneiro, 18-Mar-2015.)

**Hypotheses**
Ref	Expression
dvlipcn.x	⊢ (𝜑 → 𝑋 ⊆ ℂ)
dvlipcn.f	⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
dvlipcn.a	⊢ (𝜑 → 𝐴 ∈ ℂ)
dvlipcn.r	⊢ (𝜑 → 𝑅 ∈ ℝ^*)
dvlipcn.b	⊢ 𝐵 = (𝐴(ball‘(abs ∘ − ))𝑅)
dvlipcn.d	⊢ (𝜑 → 𝐵 ⊆ dom (ℂ D 𝐹))
dvlipcn.m	⊢ (𝜑 → 𝑀 ∈ ℝ)
dvlipcn.l	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)

**Assertion**
Ref	Expression
dvlipcn	⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))

Distinct variable groups: 𝑥,𝐵 𝑥,𝐹 𝑥,𝑀 𝜑,𝑥 Allowed substitution hints: 𝐴(𝑥) 𝑅(𝑥) 𝑋(𝑥) 𝑌(𝑥) 𝑍(𝑥)

Proof of Theorem dvlipcn Dummy variables 𝑡 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1elunit 13474	. . 3 ⊢ 1 ∈ (0[,]1)
2		0elunit 13473	. . 3 ⊢ 0 ∈ (0[,]1)
3		0red 11184	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 0 ∈ ℝ)
4		1red 11182	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 1 ∈ ℝ)
5		dvlipcn.d	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ⊆ dom (ℂ D 𝐹))
6		ssidd 3959	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ℂ ⊆ ℂ)
7		dvlipcn.f	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
8		dvlipcn.x	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
9	6, 7, 8	dvbss 25963	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (ℂ D 𝐹) ⊆ 𝑋)
10	5, 9	sstrd 3946	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ⊆ 𝑋)
11	10, 8	sstrd 3946	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ⊆ ℂ)
12	11	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐵 ⊆ ℂ)
13		simprl 780	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
14	12, 13	sseldd 3937	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ ℂ)
15	14	adantr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑌 ∈ ℂ)
16		unitssre 13503	. . . . . . . . . . 11 ⊢ (0[,]1) ⊆ ℝ
17		ax-resscn 11130	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℂ
18	16, 17	sstri 3945	. . . . . . . . . 10 ⊢ (0[,]1) ⊆ ℂ
19		simpr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ (0[,]1))
20	18, 19	sselid 3934	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℂ)
21	15, 20	mulcomd 11203	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝑌 · 𝑡) = (𝑡 · 𝑌))
22		simprr 782	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
23	12, 22	sseldd 3937	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ ℂ)
24	23	adantr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑍 ∈ ℂ)
25		iirev 24991	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0[,]1) → (1 − 𝑡) ∈ (0[,]1))
26	25	adantl 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (1 − 𝑡) ∈ (0[,]1))
27	18, 26	sselid 3934	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (1 − 𝑡) ∈ ℂ)
28	24, 27	mulcomd 11203	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝑍 · (1 − 𝑡)) = ((1 − 𝑡) · 𝑍))
29	21, 28	oveq12d 7414	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)))
30		dvlipcn.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℂ)
31	30	ad2antrr 736	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐴 ∈ ℂ)
32		dvlipcn.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ ℝ^*)
33	32	ad2antrr 736	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑅 ∈ ℝ^*)
34	13	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑌 ∈ 𝐵)
35	22	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑍 ∈ 𝐵)
36		dvlipcn.b	. . . . . . . . 9 ⊢ 𝐵 = (𝐴(ball‘(abs ∘ − ))𝑅)
37	36	blcvx 24858	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)) ∈ 𝐵)
38	31, 33, 34, 35, 19, 37	syl23anc 1396	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)) ∈ 𝐵)
39	29, 38	eqeltrd 2862	. . . . . 6 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝐵)
40		eqidd 2763	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
41	7, 10	fssresd 6731	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶ℂ)
42	41	feqmptd 6935	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ ((𝐹 ↾ 𝐵)‘𝑧)))
43		fvres 6886	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑧) = (𝐹‘𝑧))
44	43	mpteq2ia 5195	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐵 ↦ ((𝐹 ↾ 𝐵)‘𝑧)) = (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧))
45	42, 44	eqtrdi 2813	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧)))
46	45	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹 ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧)))
47		fveq2 6867	. . . . . 6 ⊢ (𝑧 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → (𝐹‘𝑧) = (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
48	39, 40, 46, 47	fmptco 7111	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝐹 ↾ 𝐵) ∘ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
49	39	fmpttd 7096	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵)
50		eqid 2762	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
51	50	addcn 24926	. . . . . . . . . 10 ⊢ + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
52	51	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
53		ssid 3958	. . . . . . . . . . . 12 ⊢ ℂ ⊆ ℂ
54		cncfmptc 24974	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
55	18, 53, 54	mp3an23 1474	. . . . . . . . . . 11 ⊢ (𝑌 ∈ ℂ → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
56	14, 55	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
57		cncfmptid 24975	. . . . . . . . . . . 12 ⊢ (((0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
58	18, 53, 57	mp2an 702	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ)
59	58	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
60	56, 59	mulcncf 25508	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝑌 · 𝑡)) ∈ ((0[,]1)–cn→ℂ))
61		cncfmptc 24974	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
62	18, 53, 61	mp3an23 1474	. . . . . . . . . . 11 ⊢ (𝑍 ∈ ℂ → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
63	23, 62	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
64	50	subcn 24927	. . . . . . . . . . . 12 ⊢ − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
65	64	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
66		ax-1cn 11131	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
67		cncfmptc 24974	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
68	66, 18, 53, 67	mp3an 1482	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ)
69	68	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
70	50, 65, 69, 59	cncfmpt2f 24977	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (1 − 𝑡)) ∈ ((0[,]1)–cn→ℂ))
71	63, 70	mulcncf 25508	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝑍 · (1 − 𝑡))) ∈ ((0[,]1)–cn→ℂ))
72	50, 52, 60, 71	cncfmpt2f 24977	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→ℂ))
73		cncfcdm 24960	. . . . . . . 8 ⊢ ((𝐵 ⊆ ℂ ∧ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→ℂ)) → ((𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→𝐵) ↔ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵))
74	12, 72, 73	syl2anc 593	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→𝐵) ↔ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵))
75	49, 74	mpbird 259	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→𝐵))
76		ssidd 3959	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℂ ⊆ ℂ)
77	41	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹 ↾ 𝐵):𝐵⟶ℂ)
78	50	cnfldtopon 24842	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
79	78	toponrestid 22981	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
80	50, 79	dvres 25973	. . . . . . . . . . . 12 ⊢ (((ℂ ⊆ ℂ ∧ 𝐹:𝑋⟶ℂ) ∧ (𝑋 ⊆ ℂ ∧ 𝐵 ⊆ ℂ)) → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)))
81	6, 7, 8, 11, 80	syl22anc 849	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)))
82	50	cnfldtop 24843	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) ∈ Top
83		cnxmet 24832	. . . . . . . . . . . . . . 15 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
84	50	cnfldtopn 24841	. . . . . . . . . . . . . . . 16 ⊢ (TopOpen‘ℂ_fld) = (MetOpen‘(abs ∘ − ))
85	84	blopn 24560	. . . . . . . . . . . . . . 15 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (𝐴(ball‘(abs ∘ − ))𝑅) ∈ (TopOpen‘ℂ_fld))
86	83, 30, 32, 85	mp3an2i 1487	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(ball‘(abs ∘ − ))𝑅) ∈ (TopOpen‘ℂ_fld))
87	36, 86	eqeltrid 2866	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ (TopOpen‘ℂ_fld))
88		isopn3i 23142	. . . . . . . . . . . . 13 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ 𝐵 ∈ (TopOpen‘ℂ_fld)) → ((int‘(TopOpen‘ℂ_fld))‘𝐵) = 𝐵)
89	82, 87, 88	sylancr 596	. . . . . . . . . . . 12 ⊢ (𝜑 → ((int‘(TopOpen‘ℂ_fld))‘𝐵) = 𝐵)
90	89	reseq2d 5965	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
91	81, 90	eqtrd 2797	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
92	91	dmeqd 5881	. . . . . . . . 9 ⊢ (𝜑 → dom (ℂ D (𝐹 ↾ 𝐵)) = dom ((ℂ D 𝐹) ↾ 𝐵))
93		dmres 5998	. . . . . . . . . 10 ⊢ dom ((ℂ D 𝐹) ↾ 𝐵) = (𝐵 ∩ dom (ℂ D 𝐹))
94		dfss2 3922	. . . . . . . . . . 11 ⊢ (𝐵 ⊆ dom (ℂ D 𝐹) ↔ (𝐵 ∩ dom (ℂ D 𝐹)) = 𝐵)
95	5, 94	sylib 220	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 ∩ dom (ℂ D 𝐹)) = 𝐵)
96	93, 95	eqtrid 2809	. . . . . . . . 9 ⊢ (𝜑 → dom ((ℂ D 𝐹) ↾ 𝐵) = 𝐵)
97	92, 96	eqtrd 2797	. . . . . . . 8 ⊢ (𝜑 → dom (ℂ D (𝐹 ↾ 𝐵)) = 𝐵)
98	97	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (ℂ D (𝐹 ↾ 𝐵)) = 𝐵)
99		dvcn 25983	. . . . . . 7 ⊢ (((ℂ ⊆ ℂ ∧ (𝐹 ↾ 𝐵):𝐵⟶ℂ ∧ 𝐵 ⊆ ℂ) ∧ dom (ℂ D (𝐹 ↾ 𝐵)) = 𝐵) → (𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ))
100	76, 77, 12, 98, 99	syl31anc 1392	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ))
101	75, 100	cncfco 24969	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝐹 ↾ 𝐵) ∘ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ((0[,]1)–cn→ℂ))
102	48, 101	eqeltrrd 2863	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ((0[,]1)–cn→ℂ))
103	17	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℝ ⊆ ℂ)
104	16	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0[,]1) ⊆ ℝ)
105	7	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐹:𝑋⟶ℂ)
106	10	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐵 ⊆ 𝑋)
107	106, 39	sseldd 3937	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝑋)
108	105, 107	ffvelcdmd 7066	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
109		tgioo4 24865	. . . . . . . 8 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
110		1re 11181	. . . . . . . . 9 ⊢ 1 ∈ ℝ
111		iccntr 24882	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
112	3, 110, 111	sylancl 595	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
113	103, 104, 108, 109, 50, 112	dvmptntr 26033	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))))
114		reelprrecn 11165	. . . . . . . . 9 ⊢ ℝ ∈ {ℝ, ℂ}
115	114	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℝ ∈ {ℝ, ℂ})
116		cnelprrecn 11166	. . . . . . . . 9 ⊢ ℂ ∈ {ℝ, ℂ}
117	116	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℂ ∈ {ℝ, ℂ})
118		ioossicc 13437	. . . . . . . . . 10 ⊢ (0(,)1) ⊆ (0[,]1)
119	118	sseli 3932	. . . . . . . . 9 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ (0[,]1))
120	119, 39	sylan2 602	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝐵)
121	14, 23	subcld 11542	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 − 𝑍) ∈ ℂ)
122	121	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑌 − 𝑍) ∈ ℂ)
123	10	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐵 ⊆ 𝑋)
124	123	sselda 3936	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝑋)
125	7	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐹:𝑋⟶ℂ)
126	125	ffvelcdmda 7065	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℂ)
127	124, 126	syldan 600	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) ∈ ℂ)
128		fvexd 6882	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → ((ℂ D 𝐹)‘𝑧) ∈ V)
129	14	adantr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑌 ∈ ℂ)
130	119, 20	sylan2 602	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
131	129, 130	mulcld 11202	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑌 · 𝑡) ∈ ℂ)
132		1red 11182	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 1 ∈ ℝ)
133		simpr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
134	133	recnd 11210	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
135		1red 11182	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 1 ∈ ℝ)
136	115	dvmptid 26019	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1))
137		ioossre 13411	. . . . . . . . . . . . . 14 ⊢ (0(,)1) ⊆ ℝ
138	137	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0(,)1) ⊆ ℝ)
139		iooretop 24825	. . . . . . . . . . . . . 14 ⊢ (0(,)1) ∈ (topGen‘ran (,))
140	139	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0(,)1) ∈ (topGen‘ran (,)))
141	115, 134, 135, 136, 138, 109, 50, 140	dvmptres 26025	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ 𝑡)) = (𝑡 ∈ (0(,)1) ↦ 1))
142	115, 130, 132, 141, 14	dvmptcmul 26026	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑌 · 𝑡))) = (𝑡 ∈ (0(,)1) ↦ (𝑌 · 1)))
143	14	mulridd 11199	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 · 1) = 𝑌)
144	143	mpteq2dv 5194	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑌 · 1)) = (𝑡 ∈ (0(,)1) ↦ 𝑌))
145	142, 144	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑌 · 𝑡))) = (𝑡 ∈ (0(,)1) ↦ 𝑌))
146	23	adantr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑍 ∈ ℂ)
147	119, 27	sylan2 602	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℂ)
148	146, 147	mulcld 11202	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑍 · (1 − 𝑡)) ∈ ℂ)
149		negex 11428	. . . . . . . . . . 11 ⊢ -𝑍 ∈ V
150	149	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → -𝑍 ∈ V)
151		negex 11428	. . . . . . . . . . . . 13 ⊢ -1 ∈ V
152	151	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → -1 ∈ V)
153		1cnd 11175	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 1 ∈ ℂ)
154		0red 11184	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 0 ∈ ℝ)
155		1cnd 11175	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 1 ∈ ℂ)
156		0red 11184	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 0 ∈ ℝ)
157		1cnd 11175	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 1 ∈ ℂ)
158	115, 157	dvmptc 26020	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ ℝ ↦ 1)) = (𝑡 ∈ ℝ ↦ 0))
159	115, 155, 156, 158, 138, 109, 50, 140	dvmptres 26025	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ 1)) = (𝑡 ∈ (0(,)1) ↦ 0))
160	115, 153, 154, 159, 130, 132, 141	dvmptsub 26029	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (1 − 𝑡))) = (𝑡 ∈ (0(,)1) ↦ (0 − 1)))
161		df-neg 11417	. . . . . . . . . . . . . 14 ⊢ -1 = (0 − 1)
162	161	mpteq2i 5196	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (0(,)1) ↦ -1) = (𝑡 ∈ (0(,)1) ↦ (0 − 1))
163	160, 162	eqtr4di 2815	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (1 − 𝑡))) = (𝑡 ∈ (0(,)1) ↦ -1))
164	115, 147, 152, 163, 23	dvmptcmul 26026	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0(,)1) ↦ (𝑍 · -1)))
165		neg1cn 12180	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℂ
166		mulcom 11159	. . . . . . . . . . . . . 14 ⊢ ((𝑍 ∈ ℂ ∧ -1 ∈ ℂ) → (𝑍 · -1) = (-1 · 𝑍))
167	23, 165, 166	sylancl 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · -1) = (-1 · 𝑍))
168	23	mulm1d 11639	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (-1 · 𝑍) = -𝑍)
169	167, 168	eqtrd 2797	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · -1) = -𝑍)
170	169	mpteq2dv 5194	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑍 · -1)) = (𝑡 ∈ (0(,)1) ↦ -𝑍))
171	164, 170	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0(,)1) ↦ -𝑍))
172	115, 131, 129, 145, 148, 150, 171	dvmptadd 26022	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0(,)1) ↦ (𝑌 + -𝑍)))
173	14, 23	negsubd 11548	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 + -𝑍) = (𝑌 − 𝑍))
174	173	mpteq2dv 5194	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑌 + -𝑍)) = (𝑡 ∈ (0(,)1) ↦ (𝑌 − 𝑍)))
175	172, 174	eqtrd 2797	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0(,)1) ↦ (𝑌 − 𝑍)))
176	8	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ⊆ ℂ)
177	76, 125, 176, 12, 80	syl22anc 849	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)))
178	89	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((int‘(TopOpen‘ℂ_fld))‘𝐵) = 𝐵)
179	178	reseq2d 5965	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
180	177, 179	eqtrd 2797	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
181	46	oveq2d 7412	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)) = (ℂ D (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧))))
182		dvfcn 25970	. . . . . . . . . . . . 13 ⊢ (ℂ D (𝐹 ↾ 𝐵)):dom (ℂ D (𝐹 ↾ 𝐵))⟶ℂ
183	98	feq2d 6675	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D (𝐹 ↾ 𝐵)):dom (ℂ D (𝐹 ↾ 𝐵))⟶ℂ ↔ (ℂ D (𝐹 ↾ 𝐵)):𝐵⟶ℂ))
184	182, 183	mpbii 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)):𝐵⟶ℂ)
185	180	feq1d 6673	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D (𝐹 ↾ 𝐵)):𝐵⟶ℂ ↔ ((ℂ D 𝐹) ↾ 𝐵):𝐵⟶ℂ))
186	184, 185	mpbid 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ 𝐵):𝐵⟶ℂ)
187	186	feqmptd 6935	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ (((ℂ D 𝐹) ↾ 𝐵)‘𝑧)))
188		fvres 6886	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐵 → (((ℂ D 𝐹) ↾ 𝐵)‘𝑧) = ((ℂ D 𝐹)‘𝑧))
189	188	mpteq2ia 5195	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐵 ↦ (((ℂ D 𝐹) ↾ 𝐵)‘𝑧)) = (𝑧 ∈ 𝐵 ↦ ((ℂ D 𝐹)‘𝑧))
190	187, 189	eqtrdi 2813	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ ((ℂ D 𝐹)‘𝑧)))
191	180, 181, 190	3eqtr3d 2805	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧))) = (𝑧 ∈ 𝐵 ↦ ((ℂ D 𝐹)‘𝑧)))
192		fveq2 6867	. . . . . . . 8 ⊢ (𝑧 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → ((ℂ D 𝐹)‘𝑧) = ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
193	115, 117, 120, 122, 127, 128, 175, 191, 47, 192	dvmptco 26034	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
194	113, 193	eqtrd 2797	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
195	194	dmeqd 5881	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = dom (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
196		ovex 7429	. . . . . . 7 ⊢ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V
197	196	rgenw 3080	. . . . . 6 ⊢ ∀𝑡 ∈ (0(,)1)(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V
198		dmmptg 6229	. . . . . 6 ⊢ (∀𝑡 ∈ (0(,)1)(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V → dom (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))) = (0(,)1))
199	197, 198	mp1i 13	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))) = (0(,)1))
200	195, 199	eqtrd 2797	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (0(,)1))
201		dvlipcn.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
202	201	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑀 ∈ ℝ)
203	121	abscld 15466	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘(𝑌 − 𝑍)) ∈ ℝ)
204	202, 203	remulcld 11212	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑀 · (abs‘(𝑌 − 𝑍))) ∈ ℝ)
205	194	fveq1d 6869	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡) = ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))‘𝑡))
206		eqid 2762	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
207	206	fvmpt2 6987	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ (0(,)1) ∧ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V) → ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
208	196, 207	mpan2 701	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0(,)1) → ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
209	205, 208	sylan9eq 2817	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
210	209	fveq2d 6871	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = (abs‘(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
211		dvfcn 25970	. . . . . . . . . . 11 ⊢ (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ
212	5	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝐵 ⊆ dom (ℂ D 𝐹))
213	212, 120	sseldd 3937	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ dom (ℂ D 𝐹))
214		ffvelcdm 7062	. . . . . . . . . . 11 ⊢ (((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ ∧ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ dom (ℂ D 𝐹)) → ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
215	211, 213, 214	sylancr 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
216	215, 122	absmuld 15484	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))) = ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌 − 𝑍))))
217	210, 216	eqtrd 2797	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌 − 𝑍))))
218	215	abscld 15466	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ℝ)
219	201	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑀 ∈ ℝ)
220	122	abscld 15466	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘(𝑌 − 𝑍)) ∈ ℝ)
221	122	absge0d 15474	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 0 ≤ (abs‘(𝑌 − 𝑍)))
222		2fveq3 6872	. . . . . . . . . . 11 ⊢ (𝑦 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → (abs‘((ℂ D 𝐹)‘𝑦)) = (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
223	222	breq1d 5110	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → ((abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀 ↔ (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ≤ 𝑀))
224		dvlipcn.l	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)
225	224	ralrimiva 3154	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)
226		2fveq3 6872	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (abs‘((ℂ D 𝐹)‘𝑥)) = (abs‘((ℂ D 𝐹)‘𝑦)))
227	226	breq1d 5110	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀 ↔ (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀))
228	227	cbvralvw 3240	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀 ↔ ∀𝑦 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
229	225, 228	sylib 220	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
230	229	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ∀𝑦 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
231	223, 230, 120	rspcdva 3582	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ≤ 𝑀)
232	218, 219, 220, 221, 231	lemul1ad 12131	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌 − 𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
233	217, 232	eqbrtrd 5122	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
234	233	ralrimiva 3154	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ∀𝑡 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
235		nfv 1934	. . . . . . 7 ⊢ Ⅎ𝑧(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))
236		nfcv 2924	. . . . . . . . 9 ⊢ Ⅎ𝑡abs
237		nfcv 2924	. . . . . . . . . . 11 ⊢ Ⅎ𝑡ℝ
238		nfcv 2924	. . . . . . . . . . 11 ⊢ Ⅎ𝑡 D
239		nfmpt1 5199	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
240	237, 238, 239	nfov 7426	. . . . . . . . . 10 ⊢ Ⅎ𝑡(ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
241		nfcv 2924	. . . . . . . . . 10 ⊢ Ⅎ𝑡𝑧
242	240, 241	nffv 6877	. . . . . . . . 9 ⊢ Ⅎ𝑡((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)
243	236, 242	nffv 6877	. . . . . . . 8 ⊢ Ⅎ𝑡(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧))
244		nfcv 2924	. . . . . . . 8 ⊢ Ⅎ𝑡 ≤
245		nfcv 2924	. . . . . . . 8 ⊢ Ⅎ𝑡(𝑀 · (abs‘(𝑌 − 𝑍)))
246	243, 244, 245	nfbr 5147	. . . . . . 7 ⊢ Ⅎ𝑡(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))
247		2fveq3 6872	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)))
248	247	breq1d 5110	. . . . . . 7 ⊢ (𝑡 = 𝑧 → ((abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))) ↔ (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))))
249	235, 246, 248	cbvralw 3304	. . . . . 6 ⊢ (∀𝑡 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))) ↔ ∀𝑧 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
250	234, 249	sylib 220	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ∀𝑧 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
251	250	r19.21bi 3254	. . . 4 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
252	3, 4, 102, 200, 204, 251	dvlip 26055	. . 3 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (1 ∈ (0[,]1) ∧ 0 ∈ (0[,]1))) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0))) ≤ ((𝑀 · (abs‘(𝑌 − 𝑍))) · (abs‘(1 − 0))))
253	1, 2, 252	mpanr12 715	. 2 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0))) ≤ ((𝑀 · (abs‘(𝑌 − 𝑍))) · (abs‘(1 − 0))))
254		oveq2 7404	. . . . . . . . 9 ⊢ (𝑡 = 1 → (𝑌 · 𝑡) = (𝑌 · 1))
255		oveq2 7404	. . . . . . . . . . 11 ⊢ (𝑡 = 1 → (1 − 𝑡) = (1 − 1))
256		1m1e0 12290	. . . . . . . . . . 11 ⊢ (1 − 1) = 0
257	255, 256	eqtrdi 2813	. . . . . . . . . 10 ⊢ (𝑡 = 1 → (1 − 𝑡) = 0)
258	257	oveq2d 7412	. . . . . . . . 9 ⊢ (𝑡 = 1 → (𝑍 · (1 − 𝑡)) = (𝑍 · 0))
259	254, 258	oveq12d 7414	. . . . . . . 8 ⊢ (𝑡 = 1 → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑌 · 1) + (𝑍 · 0)))
260	259	fveq2d 6871	. . . . . . 7 ⊢ (𝑡 = 1 → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝐹‘((𝑌 · 1) + (𝑍 · 0))))
261		eqid 2762	. . . . . . 7 ⊢ (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
262		fvex 6880	. . . . . . 7 ⊢ (𝐹‘((𝑌 · 1) + (𝑍 · 0))) ∈ V
263	260, 261, 262	fvmpt 6975	. . . . . 6 ⊢ (1 ∈ (0[,]1) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) = (𝐹‘((𝑌 · 1) + (𝑍 · 0))))
264	1, 263	ax-mp 5	. . . . 5 ⊢ ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) = (𝐹‘((𝑌 · 1) + (𝑍 · 0)))
265	23	mul01d 11382	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · 0) = 0)
266	143, 265	oveq12d 7414	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 1) + (𝑍 · 0)) = (𝑌 + 0))
267	14	addridd 11383	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 + 0) = 𝑌)
268	266, 267	eqtrd 2797	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 1) + (𝑍 · 0)) = 𝑌)
269	268	fveq2d 6871	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹‘((𝑌 · 1) + (𝑍 · 0))) = (𝐹‘𝑌))
270	264, 269	eqtrid 2809	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) = (𝐹‘𝑌))
271		oveq2 7404	. . . . . . . . 9 ⊢ (𝑡 = 0 → (𝑌 · 𝑡) = (𝑌 · 0))
272		oveq2 7404	. . . . . . . . . . 11 ⊢ (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
273		1m0e1 12337	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
274	272, 273	eqtrdi 2813	. . . . . . . . . 10 ⊢ (𝑡 = 0 → (1 − 𝑡) = 1)
275	274	oveq2d 7412	. . . . . . . . 9 ⊢ (𝑡 = 0 → (𝑍 · (1 − 𝑡)) = (𝑍 · 1))
276	271, 275	oveq12d 7414	. . . . . . . 8 ⊢ (𝑡 = 0 → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑌 · 0) + (𝑍 · 1)))
277	276	fveq2d 6871	. . . . . . 7 ⊢ (𝑡 = 0 → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝐹‘((𝑌 · 0) + (𝑍 · 1))))
278		fvex 6880	. . . . . . 7 ⊢ (𝐹‘((𝑌 · 0) + (𝑍 · 1))) ∈ V
279	277, 261, 278	fvmpt 6975	. . . . . 6 ⊢ (0 ∈ (0[,]1) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0) = (𝐹‘((𝑌 · 0) + (𝑍 · 1))))
280	2, 279	ax-mp 5	. . . . 5 ⊢ ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0) = (𝐹‘((𝑌 · 0) + (𝑍 · 1)))
281	14	mul01d 11382	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 · 0) = 0)
282	23	mulridd 11199	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · 1) = 𝑍)
283	281, 282	oveq12d 7414	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 0) + (𝑍 · 1)) = (0 + 𝑍))
284	23	addlidd 11384	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0 + 𝑍) = 𝑍)
285	283, 284	eqtrd 2797	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 0) + (𝑍 · 1)) = 𝑍)
286	285	fveq2d 6871	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹‘((𝑌 · 0) + (𝑍 · 1))) = (𝐹‘𝑍))
287	280, 286	eqtrid 2809	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0) = (𝐹‘𝑍))
288	270, 287	oveq12d 7414	. . 3 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0)) = ((𝐹‘𝑌) − (𝐹‘𝑍)))
289	288	fveq2d 6871	. 2 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0))) = (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))))
290	273	fveq2i 6870	. . . . 5 ⊢ (abs‘(1 − 0)) = (abs‘1)
291		abs1 15324	. . . . 5 ⊢ (abs‘1) = 1
292	290, 291	eqtri 2785	. . . 4 ⊢ (abs‘(1 − 0)) = 1
293	292	oveq2i 7407	. . 3 ⊢ ((𝑀 · (abs‘(𝑌 − 𝑍))) · (abs‘(1 − 0))) = ((𝑀 · (abs‘(𝑌 − 𝑍))) · 1)
294	204	recnd 11210	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑀 · (abs‘(𝑌 − 𝑍))) ∈ ℂ)
295	294	mulridd 11199	. . 3 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑀 · (abs‘(𝑌 − 𝑍))) · 1) = (𝑀 · (abs‘(𝑌 − 𝑍))))
296	293, 295	eqtrid 2809	. 2 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑀 · (abs‘(𝑌 − 𝑍))) · (abs‘(1 − 0))) = (𝑀 · (abs‘(𝑌 − 𝑍))))
297	253, 289, 296	3brtr3d 5131	1 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1560 ∈ wcel 2142 ∀wral 3076 Vcvv 3454 ∩ cin 3903 ⊆ wss 3904 {cpr 4584 class class class wbr 5100 ↦ cmpt 5181 dom cdm 5647 ran crn 5648 ↾ cres 5649 ∘ ccom 5651 ⟶wf 6517 ‘cfv 6521 (class class class)co 7396 ℂcc 11071 ℝcr 11072 0cc0 11073 1c1 11074 + caddc 11076 · cmul 11078 ℝ^*cxr 11215 ≤ cle 11217 − cmin 11414 -cneg 11415 (,)cioo 13349 [,]cicc 13352 abscabs 15261 TopOpenctopn 17450 topGenctg 17466 ∞Metcxmet 21409 ballcbl 21411 ℂ_fldccnfld 21424 Topctop 22953 intcnt 23077 Cn ccn 23284 ×_t ctx 23620 –cn→ccncf 24938 D cdv 25925

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 ax-pre-sup 11151 ax-addf 11152

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-iin 4952 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-isom 6530 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-of 7660 df-om 7847 df-1st 7970 df-2nd 7971 df-supp 8141 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-2o 8438 df-er 8678 df-map 8810 df-pm 8811 df-ixp 8880 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-fsupp 9308 df-fi 9357 df-sup 9388 df-inf 9389 df-oi 9458 df-card 9897 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-div 11845 df-nn 12211 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12482 df-z 12569 df-dec 12689 df-uz 12840 df-q 12950 df-rp 12994 df-xneg 13114 df-xadd 13115 df-xmul 13116 df-ioo 13353 df-ico 13355 df-icc 13356 df-fz 13513 df-fzo 13660 df-seq 14015 df-exp 14075 df-hash 14344 df-cj 15126 df-re 15127 df-im 15128 df-sqrt 15262 df-abs 15263 df-struct 17183 df-sets 17200 df-slot 17218 df-ndx 17230 df-base 17246 df-ress 17267 df-plusg 17299 df-mulr 17300 df-starv 17301 df-sca 17302 df-vsca 17303 df-ip 17304 df-tset 17305 df-ple 17306 df-ds 17308 df-unif 17309 df-hom 17310 df-cco 17311 df-rest 17451 df-topn 17452 df-0g 17470 df-gsum 17471 df-topgen 17472 df-pt 17473 df-prds 17476 df-xrs 17532 df-qtop 17537 df-imas 17538 df-xps 17540 df-mre 17614 df-mrc 17615 df-acs 17617 df-mgm 18674 df-sgrp 18753 df-mnd 18769 df-submnd 18818 df-mulg 19110 df-cntz 19357 df-cmn 19822 df-psmet 21416 df-xmet 21417 df-met 21418 df-bl 21419 df-mopn 21420 df-fbas 21421 df-fg 21422 df-cnfld 21425 df-top 22954 df-topon 22971 df-topsp 22993 df-bases 23006 df-cld 23079 df-ntr 23080 df-cls 23081 df-nei 23158 df-lp 23196 df-perf 23197 df-cn 23287 df-cnp 23288 df-haus 23375 df-cmp 23447 df-tx 23622 df-hmeo 23815 df-fil 23906 df-fm 23998 df-flim 23999 df-flf 24000 df-xms 24380 df-ms 24381 df-tms 24382 df-cncf 24940 df-limc 25928 df-dv 25929

This theorem is referenced by: dvlip2 26057 dv11cn 26063

W3C validator