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 25264

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 13308	. . 3 ⊢ 1 ∈ (0[,]1)
2		0elunit 13307	. . 3 ⊢ 0 ∈ (0[,]1)
3		0red 11084	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 0 ∈ ℝ)
4		1red 11082	. . . 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 25171	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (ℂ D 𝐹) ⊆ 𝑋)
10	5, 9	sstrd 3946	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ⊆ 𝑋)
11	10, 8	sstrd 3946	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ⊆ ℂ)
12	11	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐵 ⊆ ℂ)
13		simprl 769	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
14	12, 13	sseldd 3937	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ ℂ)
15	14	adantr 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑌 ∈ ℂ)
16		unitssre 13337	. . . . . . . . . . 11 ⊢ (0[,]1) ⊆ ℝ
17		ax-resscn 11034	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℂ
18	16, 17	sstri 3945	. . . . . . . . . 10 ⊢ (0[,]1) ⊆ ℂ
19		simpr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ (0[,]1))
20	18, 19	sselid 3934	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℂ)
21	15, 20	mulcomd 11102	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝑌 · 𝑡) = (𝑡 · 𝑌))
22		simprr 771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
23	12, 22	sseldd 3937	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ ℂ)
24	23	adantr 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑍 ∈ ℂ)
25		iirev 24198	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0[,]1) → (1 − 𝑡) ∈ (0[,]1))
26	25	adantl 483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (1 − 𝑡) ∈ (0[,]1))
27	18, 26	sselid 3934	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (1 − 𝑡) ∈ ℂ)
28	24, 27	mulcomd 11102	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝑍 · (1 − 𝑡)) = ((1 − 𝑡) · 𝑍))
29	21, 28	oveq12d 7360	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)))
30		dvlipcn.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℂ)
31	30	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐴 ∈ ℂ)
32		dvlipcn.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ ℝ^*)
33	32	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑅 ∈ ℝ^*)
34	13	adantr 482	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑌 ∈ 𝐵)
35	22	adantr 482	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑍 ∈ 𝐵)
36		dvlipcn.b	. . . . . . . . 9 ⊢ 𝐵 = (𝐴(ball‘(abs ∘ − ))𝑅)
37	36	blcvx 24067	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)) ∈ 𝐵)
38	31, 33, 34, 35, 19, 37	syl23anc 1377	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)) ∈ 𝐵)
39	29, 38	eqeltrd 2838	. . . . . 6 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝐵)
40		eqidd 2738	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
41	7, 10	fssresd 6697	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶ℂ)
42	41	feqmptd 6898	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ ((𝐹 ↾ 𝐵)‘𝑧)))
43		fvres 6849	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑧) = (𝐹‘𝑧))
44	43	mpteq2ia 5200	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐵 ↦ ((𝐹 ↾ 𝐵)‘𝑧)) = (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧))
45	42, 44	eqtrdi 2793	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧)))
46	45	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹 ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧)))
47		fveq2 6830	. . . . . 6 ⊢ (𝑧 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → (𝐹‘𝑧) = (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
48	39, 40, 46, 47	fmptco 7062	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝐹 ↾ 𝐵) ∘ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
49	39	fmpttd 7050	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵)
50		eqid 2737	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
51	50	addcn 24134	. . . . . . . . . 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 24181	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
55	18, 53, 54	mp3an23 1453	. . . . . . . . . . 11 ⊢ (𝑌 ∈ ℂ → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
56	14, 55	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
57		cncfmptid 24182	. . . . . . . . . . . 12 ⊢ (((0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
58	18, 53, 57	mp2an 690	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ)
59	58	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
60	56, 59	mulcncf 24716	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝑌 · 𝑡)) ∈ ((0[,]1)–cn→ℂ))
61		cncfmptc 24181	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
62	18, 53, 61	mp3an23 1453	. . . . . . . . . . 11 ⊢ (𝑍 ∈ ℂ → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
63	23, 62	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
64	50	subcn 24135	. . . . . . . . . . . 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 11035	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
67		cncfmptc 24181	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
68	66, 18, 53, 67	mp3an 1461	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ)
69	68	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
70	50, 65, 69, 59	cncfmpt2f 24184	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (1 − 𝑡)) ∈ ((0[,]1)–cn→ℂ))
71	63, 70	mulcncf 24716	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝑍 · (1 − 𝑡))) ∈ ((0[,]1)–cn→ℂ))
72	50, 52, 60, 71	cncfmpt2f 24184	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→ℂ))
73		cncfcdm 24167	. . . . . . . 8 ⊢ ((𝐵 ⊆ ℂ ∧ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→ℂ)) → ((𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→𝐵) ↔ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵))
74	12, 72, 73	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→𝐵) ↔ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵))
75	49, 74	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→𝐵))
76		ssidd 3959	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℂ ⊆ ℂ)
77	41	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹 ↾ 𝐵):𝐵⟶ℂ)
78	50	cnfldtopon 24052	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
79	78	toponrestid 22176	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
80	50, 79	dvres 25181	. . . . . . . . . . . 12 ⊢ (((ℂ ⊆ ℂ ∧ 𝐹:𝑋⟶ℂ) ∧ (𝑋 ⊆ ℂ ∧ 𝐵 ⊆ ℂ)) → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)))
81	6, 7, 8, 11, 80	syl22anc 837	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)))
82	50	cnfldtop 24053	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) ∈ Top
83		cnxmet 24042	. . . . . . . . . . . . . . 15 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
84	50	cnfldtopn 24051	. . . . . . . . . . . . . . . 16 ⊢ (TopOpen‘ℂ_fld) = (MetOpen‘(abs ∘ − ))
85	84	blopn 23762	. . . . . . . . . . . . . . 15 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (𝐴(ball‘(abs ∘ − ))𝑅) ∈ (TopOpen‘ℂ_fld))
86	83, 30, 32, 85	mp3an2i 1466	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(ball‘(abs ∘ − ))𝑅) ∈ (TopOpen‘ℂ_fld))
87	36, 86	eqeltrid 2842	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ (TopOpen‘ℂ_fld))
88		isopn3i 22339	. . . . . . . . . . . . 13 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ 𝐵 ∈ (TopOpen‘ℂ_fld)) → ((int‘(TopOpen‘ℂ_fld))‘𝐵) = 𝐵)
89	82, 87, 88	sylancr 588	. . . . . . . . . . . 12 ⊢ (𝜑 → ((int‘(TopOpen‘ℂ_fld))‘𝐵) = 𝐵)
90	89	reseq2d 5928	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
91	81, 90	eqtrd 2777	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
92	91	dmeqd 5852	. . . . . . . . 9 ⊢ (𝜑 → dom (ℂ D (𝐹 ↾ 𝐵)) = dom ((ℂ D 𝐹) ↾ 𝐵))
93		dmres 5950	. . . . . . . . . 10 ⊢ dom ((ℂ D 𝐹) ↾ 𝐵) = (𝐵 ∩ dom (ℂ D 𝐹))
94		df-ss 3919	. . . . . . . . . . 11 ⊢ (𝐵 ⊆ dom (ℂ D 𝐹) ↔ (𝐵 ∩ dom (ℂ D 𝐹)) = 𝐵)
95	5, 94	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 ∩ dom (ℂ D 𝐹)) = 𝐵)
96	93, 95	eqtrid 2789	. . . . . . . . 9 ⊢ (𝜑 → dom ((ℂ D 𝐹) ↾ 𝐵) = 𝐵)
97	92, 96	eqtrd 2777	. . . . . . . 8 ⊢ (𝜑 → dom (ℂ D (𝐹 ↾ 𝐵)) = 𝐵)
98	97	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (ℂ D (𝐹 ↾ 𝐵)) = 𝐵)
99		dvcn 25191	. . . . . . 7 ⊢ (((ℂ ⊆ ℂ ∧ (𝐹 ↾ 𝐵):𝐵⟶ℂ ∧ 𝐵 ⊆ ℂ) ∧ dom (ℂ D (𝐹 ↾ 𝐵)) = 𝐵) → (𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ))
100	76, 77, 12, 98, 99	syl31anc 1373	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ))
101	75, 100	cncfco 24176	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝐹 ↾ 𝐵) ∘ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ((0[,]1)–cn→ℂ))
102	48, 101	eqeltrrd 2839	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ((0[,]1)–cn→ℂ))
103	17	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℝ ⊆ ℂ)
104	16	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0[,]1) ⊆ ℝ)
105	7	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐹:𝑋⟶ℂ)
106	10	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐵 ⊆ 𝑋)
107	106, 39	sseldd 3937	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝑋)
108	105, 107	ffvelcdmd 7023	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
109	50	tgioo2 24072	. . . . . . . 8 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
110		1re 11081	. . . . . . . . 9 ⊢ 1 ∈ ℝ
111		iccntr 24090	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
112	3, 110, 111	sylancl 587	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
113	103, 104, 108, 109, 50, 112	dvmptntr 25241	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))))
114		reelprrecn 11069	. . . . . . . . 9 ⊢ ℝ ∈ {ℝ, ℂ}
115	114	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℝ ∈ {ℝ, ℂ})
116		cnelprrecn 11070	. . . . . . . . 9 ⊢ ℂ ∈ {ℝ, ℂ}
117	116	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℂ ∈ {ℝ, ℂ})
118		ioossicc 13271	. . . . . . . . . 10 ⊢ (0(,)1) ⊆ (0[,]1)
119	118	sseli 3932	. . . . . . . . 9 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ (0[,]1))
120	119, 39	sylan2 594	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝐵)
121	14, 23	subcld 11438	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 − 𝑍) ∈ ℂ)
122	121	adantr 482	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑌 − 𝑍) ∈ ℂ)
123	10	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐵 ⊆ 𝑋)
124	123	sselda 3936	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝑋)
125	7	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐹:𝑋⟶ℂ)
126	125	ffvelcdmda 7022	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℂ)
127	124, 126	syldan 592	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) ∈ ℂ)
128		fvexd 6845	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → ((ℂ D 𝐹)‘𝑧) ∈ V)
129	14	adantr 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑌 ∈ ℂ)
130	119, 20	sylan2 594	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
131	129, 130	mulcld 11101	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑌 · 𝑡) ∈ ℂ)
132		1red 11082	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 1 ∈ ℝ)
133		simpr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
134	133	recnd 11109	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
135		1red 11082	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 1 ∈ ℝ)
136	115	dvmptid 25227	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1))
137		ioossre 13246	. . . . . . . . . . . . . 14 ⊢ (0(,)1) ⊆ ℝ
138	137	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0(,)1) ⊆ ℝ)
139		iooretop 24035	. . . . . . . . . . . . . 14 ⊢ (0(,)1) ∈ (topGen‘ran (,))
140	139	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0(,)1) ∈ (topGen‘ran (,)))
141	115, 134, 135, 136, 138, 109, 50, 140	dvmptres 25233	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ 𝑡)) = (𝑡 ∈ (0(,)1) ↦ 1))
142	115, 130, 132, 141, 14	dvmptcmul 25234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑌 · 𝑡))) = (𝑡 ∈ (0(,)1) ↦ (𝑌 · 1)))
143	14	mulid1d 11098	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 · 1) = 𝑌)
144	143	mpteq2dv 5199	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑌 · 1)) = (𝑡 ∈ (0(,)1) ↦ 𝑌))
145	142, 144	eqtrd 2777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑌 · 𝑡))) = (𝑡 ∈ (0(,)1) ↦ 𝑌))
146	23	adantr 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑍 ∈ ℂ)
147	119, 27	sylan2 594	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℂ)
148	146, 147	mulcld 11101	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑍 · (1 − 𝑡)) ∈ ℂ)
149		negex 11325	. . . . . . . . . . 11 ⊢ -𝑍 ∈ V
150	149	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → -𝑍 ∈ V)
151		negex 11325	. . . . . . . . . . . . 13 ⊢ -1 ∈ V
152	151	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → -1 ∈ V)
153		1cnd 11076	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 1 ∈ ℂ)
154		0red 11084	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 0 ∈ ℝ)
155		1cnd 11076	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 1 ∈ ℂ)
156		0red 11084	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 0 ∈ ℝ)
157		1cnd 11076	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 1 ∈ ℂ)
158	115, 157	dvmptc 25228	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ ℝ ↦ 1)) = (𝑡 ∈ ℝ ↦ 0))
159	115, 155, 156, 158, 138, 109, 50, 140	dvmptres 25233	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ 1)) = (𝑡 ∈ (0(,)1) ↦ 0))
160	115, 153, 154, 159, 130, 132, 141	dvmptsub 25237	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (1 − 𝑡))) = (𝑡 ∈ (0(,)1) ↦ (0 − 1)))
161		df-neg 11314	. . . . . . . . . . . . . 14 ⊢ -1 = (0 − 1)
162	161	mpteq2i 5202	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (0(,)1) ↦ -1) = (𝑡 ∈ (0(,)1) ↦ (0 − 1))
163	160, 162	eqtr4di 2795	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (1 − 𝑡))) = (𝑡 ∈ (0(,)1) ↦ -1))
164	115, 147, 152, 163, 23	dvmptcmul 25234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0(,)1) ↦ (𝑍 · -1)))
165		neg1cn 12193	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℂ
166		mulcom 11063	. . . . . . . . . . . . . 14 ⊢ ((𝑍 ∈ ℂ ∧ -1 ∈ ℂ) → (𝑍 · -1) = (-1 · 𝑍))
167	23, 165, 166	sylancl 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · -1) = (-1 · 𝑍))
168	23	mulm1d 11533	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (-1 · 𝑍) = -𝑍)
169	167, 168	eqtrd 2777	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · -1) = -𝑍)
170	169	mpteq2dv 5199	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑍 · -1)) = (𝑡 ∈ (0(,)1) ↦ -𝑍))
171	164, 170	eqtrd 2777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0(,)1) ↦ -𝑍))
172	115, 131, 129, 145, 148, 150, 171	dvmptadd 25230	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0(,)1) ↦ (𝑌 + -𝑍)))
173	14, 23	negsubd 11444	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 + -𝑍) = (𝑌 − 𝑍))
174	173	mpteq2dv 5199	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑌 + -𝑍)) = (𝑡 ∈ (0(,)1) ↦ (𝑌 − 𝑍)))
175	172, 174	eqtrd 2777	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0(,)1) ↦ (𝑌 − 𝑍)))
176	8	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ⊆ ℂ)
177	76, 125, 176, 12, 80	syl22anc 837	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)))
178	89	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((int‘(TopOpen‘ℂ_fld))‘𝐵) = 𝐵)
179	178	reseq2d 5928	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
180	177, 179	eqtrd 2777	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
181	46	oveq2d 7358	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)) = (ℂ D (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧))))
182		dvfcn 25178	. . . . . . . . . . . . 13 ⊢ (ℂ D (𝐹 ↾ 𝐵)):dom (ℂ D (𝐹 ↾ 𝐵))⟶ℂ
183	98	feq2d 6642	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D (𝐹 ↾ 𝐵)):dom (ℂ D (𝐹 ↾ 𝐵))⟶ℂ ↔ (ℂ D (𝐹 ↾ 𝐵)):𝐵⟶ℂ))
184	182, 183	mpbii 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)):𝐵⟶ℂ)
185	180	feq1d 6641	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D (𝐹 ↾ 𝐵)):𝐵⟶ℂ ↔ ((ℂ D 𝐹) ↾ 𝐵):𝐵⟶ℂ))
186	184, 185	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ 𝐵):𝐵⟶ℂ)
187	186	feqmptd 6898	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ (((ℂ D 𝐹) ↾ 𝐵)‘𝑧)))
188		fvres 6849	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐵 → (((ℂ D 𝐹) ↾ 𝐵)‘𝑧) = ((ℂ D 𝐹)‘𝑧))
189	188	mpteq2ia 5200	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐵 ↦ (((ℂ D 𝐹) ↾ 𝐵)‘𝑧)) = (𝑧 ∈ 𝐵 ↦ ((ℂ D 𝐹)‘𝑧))
190	187, 189	eqtrdi 2793	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ ((ℂ D 𝐹)‘𝑧)))
191	180, 181, 190	3eqtr3d 2785	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧))) = (𝑧 ∈ 𝐵 ↦ ((ℂ D 𝐹)‘𝑧)))
192		fveq2 6830	. . . . . . . 8 ⊢ (𝑧 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → ((ℂ D 𝐹)‘𝑧) = ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
193	115, 117, 120, 122, 127, 128, 175, 191, 47, 192	dvmptco 25242	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
194	113, 193	eqtrd 2777	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
195	194	dmeqd 5852	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = dom (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
196		ovex 7375	. . . . . . 7 ⊢ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V
197	196	rgenw 3066	. . . . . 6 ⊢ ∀𝑡 ∈ (0(,)1)(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V
198		dmmptg 6185	. . . . . 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 2777	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (0(,)1))
201		dvlipcn.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
202	201	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑀 ∈ ℝ)
203	121	abscld 15248	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘(𝑌 − 𝑍)) ∈ ℝ)
204	202, 203	remulcld 11111	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑀 · (abs‘(𝑌 − 𝑍))) ∈ ℝ)
205	194	fveq1d 6832	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡) = ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))‘𝑡))
206		eqid 2737	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
207	206	fvmpt2 6947	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ (0(,)1) ∧ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V) → ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
208	196, 207	mpan2 689	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0(,)1) → ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
209	205, 208	sylan9eq 2797	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
210	209	fveq2d 6834	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = (abs‘(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
211		dvfcn 25178	. . . . . . . . . . 11 ⊢ (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ
212	5	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝐵 ⊆ dom (ℂ D 𝐹))
213	212, 120	sseldd 3937	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ dom (ℂ D 𝐹))
214		ffvelcdm 7020	. . . . . . . . . . 11 ⊢ (((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ ∧ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ dom (ℂ D 𝐹)) → ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
215	211, 213, 214	sylancr 588	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
216	215, 122	absmuld 15266	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))) = ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌 − 𝑍))))
217	210, 216	eqtrd 2777	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌 − 𝑍))))
218	215	abscld 15248	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ℝ)
219	201	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑀 ∈ ℝ)
220	122	abscld 15248	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘(𝑌 − 𝑍)) ∈ ℝ)
221	122	absge0d 15256	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 0 ≤ (abs‘(𝑌 − 𝑍)))
222		2fveq3 6835	. . . . . . . . . . 11 ⊢ (𝑦 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → (abs‘((ℂ D 𝐹)‘𝑦)) = (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
223	222	breq1d 5107	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → ((abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀 ↔ (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ≤ 𝑀))
224		dvlipcn.l	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)
225	224	ralrimiva 3140	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)
226		2fveq3 6835	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (abs‘((ℂ D 𝐹)‘𝑥)) = (abs‘((ℂ D 𝐹)‘𝑦)))
227	226	breq1d 5107	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀 ↔ (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀))
228	227	cbvralvw 3222	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀 ↔ ∀𝑦 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
229	225, 228	sylib 217	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
230	229	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ∀𝑦 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
231	223, 230, 120	rspcdva 3575	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ≤ 𝑀)
232	218, 219, 220, 221, 231	lemul1ad 12020	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌 − 𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
233	217, 232	eqbrtrd 5119	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
234	233	ralrimiva 3140	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ∀𝑡 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
235		nfv 1917	. . . . . . 7 ⊢ Ⅎ𝑧(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))
236		nfcv 2905	. . . . . . . . 9 ⊢ Ⅎ𝑡abs
237		nfcv 2905	. . . . . . . . . . 11 ⊢ Ⅎ𝑡ℝ
238		nfcv 2905	. . . . . . . . . . 11 ⊢ Ⅎ𝑡 D
239		nfmpt1 5205	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
240	237, 238, 239	nfov 7372	. . . . . . . . . 10 ⊢ Ⅎ𝑡(ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
241		nfcv 2905	. . . . . . . . . 10 ⊢ Ⅎ𝑡𝑧
242	240, 241	nffv 6840	. . . . . . . . 9 ⊢ Ⅎ𝑡((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)
243	236, 242	nffv 6840	. . . . . . . 8 ⊢ Ⅎ𝑡(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧))
244		nfcv 2905	. . . . . . . 8 ⊢ Ⅎ𝑡 ≤
245		nfcv 2905	. . . . . . . 8 ⊢ Ⅎ𝑡(𝑀 · (abs‘(𝑌 − 𝑍)))
246	243, 244, 245	nfbr 5144	. . . . . . 7 ⊢ Ⅎ𝑡(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))
247		2fveq3 6835	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)))
248	247	breq1d 5107	. . . . . . 7 ⊢ (𝑡 = 𝑧 → ((abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))) ↔ (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))))
249	235, 246, 248	cbvralw 3286	. . . . . 6 ⊢ (∀𝑡 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))) ↔ ∀𝑧 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
250	234, 249	sylib 217	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ∀𝑧 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
251	250	r19.21bi 3231	. . . 4 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
252	3, 4, 102, 200, 204, 251	dvlip 25263	. . 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 703	. 2 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0))) ≤ ((𝑀 · (abs‘(𝑌 − 𝑍))) · (abs‘(1 − 0))))
254		oveq2 7350	. . . . . . . . 9 ⊢ (𝑡 = 1 → (𝑌 · 𝑡) = (𝑌 · 1))
255		oveq2 7350	. . . . . . . . . . 11 ⊢ (𝑡 = 1 → (1 − 𝑡) = (1 − 1))
256		1m1e0 12151	. . . . . . . . . . 11 ⊢ (1 − 1) = 0
257	255, 256	eqtrdi 2793	. . . . . . . . . 10 ⊢ (𝑡 = 1 → (1 − 𝑡) = 0)
258	257	oveq2d 7358	. . . . . . . . 9 ⊢ (𝑡 = 1 → (𝑍 · (1 − 𝑡)) = (𝑍 · 0))
259	254, 258	oveq12d 7360	. . . . . . . 8 ⊢ (𝑡 = 1 → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑌 · 1) + (𝑍 · 0)))
260	259	fveq2d 6834	. . . . . . 7 ⊢ (𝑡 = 1 → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝐹‘((𝑌 · 1) + (𝑍 · 0))))
261		eqid 2737	. . . . . . 7 ⊢ (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
262		fvex 6843	. . . . . . 7 ⊢ (𝐹‘((𝑌 · 1) + (𝑍 · 0))) ∈ V
263	260, 261, 262	fvmpt 6936	. . . . . 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 11280	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · 0) = 0)
266	143, 265	oveq12d 7360	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 1) + (𝑍 · 0)) = (𝑌 + 0))
267	14	addid1d 11281	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 + 0) = 𝑌)
268	266, 267	eqtrd 2777	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 1) + (𝑍 · 0)) = 𝑌)
269	268	fveq2d 6834	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹‘((𝑌 · 1) + (𝑍 · 0))) = (𝐹‘𝑌))
270	264, 269	eqtrid 2789	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) = (𝐹‘𝑌))
271		oveq2 7350	. . . . . . . . 9 ⊢ (𝑡 = 0 → (𝑌 · 𝑡) = (𝑌 · 0))
272		oveq2 7350	. . . . . . . . . . 11 ⊢ (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
273		1m0e1 12200	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
274	272, 273	eqtrdi 2793	. . . . . . . . . 10 ⊢ (𝑡 = 0 → (1 − 𝑡) = 1)
275	274	oveq2d 7358	. . . . . . . . 9 ⊢ (𝑡 = 0 → (𝑍 · (1 − 𝑡)) = (𝑍 · 1))
276	271, 275	oveq12d 7360	. . . . . . . 8 ⊢ (𝑡 = 0 → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑌 · 0) + (𝑍 · 1)))
277	276	fveq2d 6834	. . . . . . 7 ⊢ (𝑡 = 0 → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝐹‘((𝑌 · 0) + (𝑍 · 1))))
278		fvex 6843	. . . . . . 7 ⊢ (𝐹‘((𝑌 · 0) + (𝑍 · 1))) ∈ V
279	277, 261, 278	fvmpt 6936	. . . . . 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 11280	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 · 0) = 0)
282	23	mulid1d 11098	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · 1) = 𝑍)
283	281, 282	oveq12d 7360	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 0) + (𝑍 · 1)) = (0 + 𝑍))
284	23	addid2d 11282	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0 + 𝑍) = 𝑍)
285	283, 284	eqtrd 2777	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 0) + (𝑍 · 1)) = 𝑍)
286	285	fveq2d 6834	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹‘((𝑌 · 0) + (𝑍 · 1))) = (𝐹‘𝑍))
287	280, 286	eqtrid 2789	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0) = (𝐹‘𝑍))
288	270, 287	oveq12d 7360	. . 3 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0)) = ((𝐹‘𝑌) − (𝐹‘𝑍)))
289	288	fveq2d 6834	. 2 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0))) = (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))))
290	273	fveq2i 6833	. . . . 5 ⊢ (abs‘(1 − 0)) = (abs‘1)
291		abs1 15109	. . . . 5 ⊢ (abs‘1) = 1
292	290, 291	eqtri 2765	. . . 4 ⊢ (abs‘(1 − 0)) = 1
293	292	oveq2i 7353	. . 3 ⊢ ((𝑀 · (abs‘(𝑌 − 𝑍))) · (abs‘(1 − 0))) = ((𝑀 · (abs‘(𝑌 − 𝑍))) · 1)
294	204	recnd 11109	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑀 · (abs‘(𝑌 − 𝑍))) ∈ ℂ)
295	294	mulid1d 11098	. . 3 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑀 · (abs‘(𝑌 − 𝑍))) · 1) = (𝑀 · (abs‘(𝑌 − 𝑍))))
296	293, 295	eqtrid 2789	. 2 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑀 · (abs‘(𝑌 − 𝑍))) · (abs‘(1 − 0))) = (𝑀 · (abs‘(𝑌 − 𝑍))))
297	253, 289, 296	3brtr3d 5128	1 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1541 ∈ wcel 2106 ∀wral 3062 Vcvv 3442 ∩ cin 3901 ⊆ wss 3902 {cpr 4580 class class class wbr 5097 ↦ cmpt 5180 dom cdm 5625 ran crn 5626 ↾ cres 5627 ∘ ccom 5629 ⟶wf 6480 ‘cfv 6484 (class class class)co 7342 ℂcc 10975 ℝcr 10976 0cc0 10977 1c1 10978 + caddc 10980 · cmul 10982 ℝ^*cxr 11114 ≤ cle 11116 − cmin 11311 -cneg 11312 (,)cioo 13185 [,]cicc 13188 abscabs 15045 TopOpenctopn 17230 topGenctg 17246 ∞Metcxmet 20688 ballcbl 20690 ℂ_fldccnfld 20703 Topctop 22148 intcnt 22274 Cn ccn 22481 ×_t ctx 22817 –cn→ccncf 24145 D cdv 25133

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-rep 5234 ax-sep 5248 ax-nul 5255 ax-pow 5313 ax-pr 5377 ax-un 7655 ax-cnex 11033 ax-resscn 11034 ax-1cn 11035 ax-icn 11036 ax-addcl 11037 ax-addrcl 11038 ax-mulcl 11039 ax-mulrcl 11040 ax-mulcom 11041 ax-addass 11042 ax-mulass 11043 ax-distr 11044 ax-i2m1 11045 ax-1ne0 11046 ax-1rid 11047 ax-rnegex 11048 ax-rrecex 11049 ax-cnre 11050 ax-pre-lttri 11051 ax-pre-lttrn 11052 ax-pre-ltadd 11053 ax-pre-mulgt0 11054 ax-pre-sup 11055 ax-addf 11056 ax-mulf 11057

This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3444 df-sbc 3732 df-csb 3848 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3921 df-nul 4275 df-if 4479 df-pw 4554 df-sn 4579 df-pr 4581 df-tp 4583 df-op 4585 df-uni 4858 df-int 4900 df-iun 4948 df-iin 4949 df-br 5098 df-opab 5160 df-mpt 5181 df-tr 5215 df-id 5523 df-eprel 5529 df-po 5537 df-so 5538 df-fr 5580 df-se 5581 df-we 5582 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6243 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6436 df-fun 6486 df-fn 6487 df-f 6488 df-f1 6489 df-fo 6490 df-f1o 6491 df-fv 6492 df-isom 6493 df-riota 7298 df-ov 7345 df-oprab 7346 df-mpo 7347 df-of 7600 df-om 7786 df-1st 7904 df-2nd 7905 df-supp 8053 df-frecs 8172 df-wrecs 8203 df-recs 8277 df-rdg 8316 df-1o 8372 df-2o 8373 df-er 8574 df-map 8693 df-pm 8694 df-ixp 8762 df-en 8810 df-dom 8811 df-sdom 8812 df-fin 8813 df-fsupp 9232 df-fi 9273 df-sup 9304 df-inf 9305 df-oi 9372 df-card 9801 df-pnf 11117 df-mnf 11118 df-xr 11119 df-ltxr 11120 df-le 11121 df-sub 11313 df-neg 11314 df-div 11739 df-nn 12080 df-2 12142 df-3 12143 df-4 12144 df-5 12145 df-6 12146 df-7 12147 df-8 12148 df-9 12149 df-n0 12340 df-z 12426 df-dec 12544 df-uz 12689 df-q 12795 df-rp 12837 df-xneg 12954 df-xadd 12955 df-xmul 12956 df-ioo 13189 df-ico 13191 df-icc 13192 df-fz 13346 df-fzo 13489 df-seq 13828 df-exp 13889 df-hash 14151 df-cj 14910 df-re 14911 df-im 14912 df-sqrt 15046 df-abs 15047 df-struct 16946 df-sets 16963 df-slot 16981 df-ndx 16993 df-base 17011 df-ress 17040 df-plusg 17073 df-mulr 17074 df-starv 17075 df-sca 17076 df-vsca 17077 df-ip 17078 df-tset 17079 df-ple 17080 df-ds 17082 df-unif 17083 df-hom 17084 df-cco 17085 df-rest 17231 df-topn 17232 df-0g 17250 df-gsum 17251 df-topgen 17252 df-pt 17253 df-prds 17256 df-xrs 17311 df-qtop 17316 df-imas 17317 df-xps 17319 df-mre 17393 df-mrc 17394 df-acs 17396 df-mgm 18424 df-sgrp 18473 df-mnd 18484 df-submnd 18529 df-mulg 18798 df-cntz 19020 df-cmn 19484 df-psmet 20695 df-xmet 20696 df-met 20697 df-bl 20698 df-mopn 20699 df-fbas 20700 df-fg 20701 df-cnfld 20704 df-top 22149 df-topon 22166 df-topsp 22188 df-bases 22202 df-cld 22276 df-ntr 22277 df-cls 22278 df-nei 22355 df-lp 22393 df-perf 22394 df-cn 22484 df-cnp 22485 df-haus 22572 df-cmp 22644 df-tx 22819 df-hmeo 23012 df-fil 23103 df-fm 23195 df-flim 23196 df-flf 23197 df-xms 23579 df-ms 23580 df-tms 23581 df-cncf 24147 df-limc 25136 df-dv 25137

This theorem is referenced by: dvlip2 25265 dv11cn 25271

W3C validator