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 26369

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 13641	. . 3 ⊢ 1 ∈ (0[,]1)
2		0elunit 13640	. . 3 ⊢ 0 ∈ (0[,]1)
3		0red 11350	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 0 ∈ ℝ)
4		1red 11348	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 1 ∈ ℝ)
5		dvlipcn.d	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ⊆ dom (ℂ D 𝐹))
6		ssidd 3936	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ℂ ⊆ ℂ)
7		dvlipcn.f	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
8		dvlipcn.x	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
9	6, 7, 8	dvbss 26276	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (ℂ D 𝐹) ⊆ 𝑋)
10	5, 9	sstrd 3923	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ⊆ 𝑋)
11	10, 8	sstrd 3923	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ⊆ ℂ)
12	11	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐵 ⊆ ℂ)
13		simprl 783	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
14	12, 13	sseldd 3914	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ ℂ)
15	14	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑌 ∈ ℂ)
16		unitssre 13670	. . . . . . . . . . 11 ⊢ (0[,]1) ⊆ ℝ
17		ax-resscn 11296	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℂ
18	16, 17	sstri 3922	. . . . . . . . . 10 ⊢ (0[,]1) ⊆ ℂ
19		simpr 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ (0[,]1))
20	18, 19	sselid 3911	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℂ)
21	15, 20	mulcomd 11369	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝑌 · 𝑡) = (𝑡 · 𝑌))
22		simprr 785	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
23	12, 22	sseldd 3914	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ ℂ)
24	23	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑍 ∈ ℂ)
25		iirev 25305	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0[,]1) → (1 − 𝑡) ∈ (0[,]1))
26	25	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (1 − 𝑡) ∈ (0[,]1))
27	18, 26	sselid 3911	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (1 − 𝑡) ∈ ℂ)
28	24, 27	mulcomd 11369	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝑍 · (1 − 𝑡)) = ((1 − 𝑡) · 𝑍))
29	21, 28	oveq12d 7469	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)))
30		dvlipcn.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℂ)
31	30	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐴 ∈ ℂ)
32		dvlipcn.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ ℝ^*)
33	32	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑅 ∈ ℝ^*)
34	13	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑌 ∈ 𝐵)
35	22	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑍 ∈ 𝐵)
36		dvlipcn.b	. . . . . . . . 9 ⊢ 𝐵 = (𝐴(ball‘(abs ∘ − ))𝑅)
37	36	blcvx 25172	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)) ∈ 𝐵)
38	31, 33, 34, 35, 19, 37	syl23anc 1405	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)) ∈ 𝐵)
39	29, 38	eqeltrd 2864	. . . . . 6 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝐵)
40		eqidd 2764	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
41	7, 10	fssresd 6779	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶ℂ)
42	41	feqmptd 6984	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ ((𝐹 ↾ 𝐵)‘𝑧)))
43		fvres 6935	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑧) = (𝐹‘𝑧))
44	43	mpteq2ia 5206	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐵 ↦ ((𝐹 ↾ 𝐵)‘𝑧)) = (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧))
45	42, 44	eqtrdi 2814	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧)))
46	45	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹 ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧)))
47		fveq2 6916	. . . . . 6 ⊢ (𝑧 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → (𝐹‘𝑧) = (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
48	39, 40, 46, 47	fmptco 7162	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝐹 ↾ 𝐵) ∘ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
49	39	fmpttd 7147	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵)
50		eqid 2763	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
51	50	addcn 25240	. . . . . . . . . 10 ⊢ + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
52	51	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
53		ssid 3935	. . . . . . . . . . . 12 ⊢ ℂ ⊆ ℂ
54		cncfmptc 25288	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
55	18, 53, 54	mp3an23 1483	. . . . . . . . . . 11 ⊢ (𝑌 ∈ ℂ → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
56	14, 55	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
57		cncfmptid 25289	. . . . . . . . . . . 12 ⊢ (((0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
58	18, 53, 57	mp2an 705	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ)
59	58	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
60	56, 59	mulcncf 25822	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝑌 · 𝑡)) ∈ ((0[,]1)–cn→ℂ))
61		cncfmptc 25288	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
62	18, 53, 61	mp3an23 1483	. . . . . . . . . . 11 ⊢ (𝑍 ∈ ℂ → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
63	23, 62	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
64	50	subcn 25241	. . . . . . . . . . . 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 11297	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
67		cncfmptc 25288	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
68	66, 18, 53, 67	mp3an 1491	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ)
69	68	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
70	50, 65, 69, 59	cncfmpt2f 25291	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (1 − 𝑡)) ∈ ((0[,]1)–cn→ℂ))
71	63, 70	mulcncf 25822	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝑍 · (1 − 𝑡))) ∈ ((0[,]1)–cn→ℂ))
72	50, 52, 60, 71	cncfmpt2f 25291	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→ℂ))
73		cncfcdm 25274	. . . . . . . 8 ⊢ ((𝐵 ⊆ ℂ ∧ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→ℂ)) → ((𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→𝐵) ↔ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵))
74	12, 72, 73	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→𝐵) ↔ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵))
75	49, 74	mpbird 260	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→𝐵))
76		ssidd 3936	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℂ ⊆ ℂ)
77	41	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹 ↾ 𝐵):𝐵⟶ℂ)
78	50	cnfldtopon 25156	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
79	78	toponrestid 23294	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
80	50, 79	dvres 26286	. . . . . . . . . . . 12 ⊢ (((ℂ ⊆ ℂ ∧ 𝐹:𝑋⟶ℂ) ∧ (𝑋 ⊆ ℂ ∧ 𝐵 ⊆ ℂ)) → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)))
81	6, 7, 8, 11, 80	syl22anc 852	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)))
82	50	cnfldtop 25157	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) ∈ Top
83		cnxmet 25146	. . . . . . . . . . . . . . 15 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
84	50	cnfldtopn 25155	. . . . . . . . . . . . . . . 16 ⊢ (TopOpen‘ℂ_fld) = (MetOpen‘(abs ∘ − ))
85	84	blopn 24874	. . . . . . . . . . . . . . 15 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (𝐴(ball‘(abs ∘ − ))𝑅) ∈ (TopOpen‘ℂ_fld))
86	83, 30, 32, 85	mp3an2i 1496	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(ball‘(abs ∘ − ))𝑅) ∈ (TopOpen‘ℂ_fld))
87	36, 86	eqeltrid 2868	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ (TopOpen‘ℂ_fld))
88		isopn3i 23455	. . . . . . . . . . . . 13 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ 𝐵 ∈ (TopOpen‘ℂ_fld)) → ((int‘(TopOpen‘ℂ_fld))‘𝐵) = 𝐵)
89	82, 87, 88	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝜑 → ((int‘(TopOpen‘ℂ_fld))‘𝐵) = 𝐵)
90	89	reseq2d 5986	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
91	81, 90	eqtrd 2798	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
92	91	dmeqd 5899	. . . . . . . . 9 ⊢ (𝜑 → dom (ℂ D (𝐹 ↾ 𝐵)) = dom ((ℂ D 𝐹) ↾ 𝐵))
93		dmres 6020	. . . . . . . . . 10 ⊢ dom ((ℂ D 𝐹) ↾ 𝐵) = (𝐵 ∩ dom (ℂ D 𝐹))
94		dfss2 4097	. . . . . . . . . . 11 ⊢ (𝐵 ⊆ dom (ℂ D 𝐹) ↔ (𝐵 ∩ dom (ℂ D 𝐹)) = 𝐵)
95	5, 94	sylib 221	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 ∩ dom (ℂ D 𝐹)) = 𝐵)
96	93, 95	eqtrid 2810	. . . . . . . . 9 ⊢ (𝜑 → dom ((ℂ D 𝐹) ↾ 𝐵) = 𝐵)
97	92, 96	eqtrd 2798	. . . . . . . 8 ⊢ (𝜑 → dom (ℂ D (𝐹 ↾ 𝐵)) = 𝐵)
98	97	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (ℂ D (𝐹 ↾ 𝐵)) = 𝐵)
99		dvcn 26296	. . . . . . 7 ⊢ (((ℂ ⊆ ℂ ∧ (𝐹 ↾ 𝐵):𝐵⟶ℂ ∧ 𝐵 ⊆ ℂ) ∧ dom (ℂ D (𝐹 ↾ 𝐵)) = 𝐵) → (𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ))
100	76, 77, 12, 98, 99	syl31anc 1401	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ))
101	75, 100	cncfco 25283	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝐹 ↾ 𝐵) ∘ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ((0[,]1)–cn→ℂ))
102	48, 101	eqeltrrd 2865	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ((0[,]1)–cn→ℂ))
103	17	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℝ ⊆ ℂ)
104	16	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0[,]1) ⊆ ℝ)
105	7	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐹:𝑋⟶ℂ)
106	10	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐵 ⊆ 𝑋)
107	106, 39	sseldd 3914	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝑋)
108	105, 107	ffvelcdmd 7117	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
109		tgioo4 25179	. . . . . . . 8 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
110		1re 11347	. . . . . . . . 9 ⊢ 1 ∈ ℝ
111		iccntr 25196	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
112	3, 110, 111	sylancl 598	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
113	103, 104, 108, 109, 50, 112	dvmptntr 26346	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))))
114		reelprrecn 11331	. . . . . . . . 9 ⊢ ℝ ∈ {ℝ, ℂ}
115	114	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℝ ∈ {ℝ, ℂ})
116		cnelprrecn 11332	. . . . . . . . 9 ⊢ ℂ ∈ {ℝ, ℂ}
117	116	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℂ ∈ {ℝ, ℂ})
118		ioossicc 13604	. . . . . . . . . 10 ⊢ (0(,)1) ⊆ (0[,]1)
119	118	sseli 3909	. . . . . . . . 9 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ (0[,]1))
120	119, 39	sylan2 605	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝐵)
121	14, 23	subcld 11708	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 − 𝑍) ∈ ℂ)
122	121	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑌 − 𝑍) ∈ ℂ)
123	10	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐵 ⊆ 𝑋)
124	123	sselda 3913	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝑋)
125	7	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐹:𝑋⟶ℂ)
126	125	ffvelcdmda 7116	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℂ)
127	124, 126	syldan 603	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) ∈ ℂ)
128		fvexd 6931	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → ((ℂ D 𝐹)‘𝑧) ∈ V)
129	14	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑌 ∈ ℂ)
130	119, 20	sylan2 605	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
131	129, 130	mulcld 11368	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑌 · 𝑡) ∈ ℂ)
132		1red 11348	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 1 ∈ ℝ)
133		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
134	133	recnd 11376	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
135		1red 11348	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 1 ∈ ℝ)
136	115	dvmptid 26332	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1))
137		ioossre 13578	. . . . . . . . . . . . . 14 ⊢ (0(,)1) ⊆ ℝ
138	137	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0(,)1) ⊆ ℝ)
139		iooretop 25139	. . . . . . . . . . . . . 14 ⊢ (0(,)1) ∈ (topGen‘ran (,))
140	139	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0(,)1) ∈ (topGen‘ran (,)))
141	115, 134, 135, 136, 138, 109, 50, 140	dvmptres 26338	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ 𝑡)) = (𝑡 ∈ (0(,)1) ↦ 1))
142	115, 130, 132, 141, 14	dvmptcmul 26339	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑌 · 𝑡))) = (𝑡 ∈ (0(,)1) ↦ (𝑌 · 1)))
143	14	mulridd 11365	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 · 1) = 𝑌)
144	143	mpteq2dv 5205	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑌 · 1)) = (𝑡 ∈ (0(,)1) ↦ 𝑌))
145	142, 144	eqtrd 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑌 · 𝑡))) = (𝑡 ∈ (0(,)1) ↦ 𝑌))
146	23	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑍 ∈ ℂ)
147	119, 27	sylan2 605	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℂ)
148	146, 147	mulcld 11368	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑍 · (1 − 𝑡)) ∈ ℂ)
149		negex 11594	. . . . . . . . . . 11 ⊢ -𝑍 ∈ V
150	149	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → -𝑍 ∈ V)
151		negex 11594	. . . . . . . . . . . . 13 ⊢ -1 ∈ V
152	151	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → -1 ∈ V)
153		1cnd 11341	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 1 ∈ ℂ)
154		0red 11350	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 0 ∈ ℝ)
155		1cnd 11341	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 1 ∈ ℂ)
156		0red 11350	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 0 ∈ ℝ)
157		1cnd 11341	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 1 ∈ ℂ)
158	115, 157	dvmptc 26333	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ ℝ ↦ 1)) = (𝑡 ∈ ℝ ↦ 0))
159	115, 155, 156, 158, 138, 109, 50, 140	dvmptres 26338	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ 1)) = (𝑡 ∈ (0(,)1) ↦ 0))
160	115, 153, 154, 159, 130, 132, 141	dvmptsub 26342	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (1 − 𝑡))) = (𝑡 ∈ (0(,)1) ↦ (0 − 1)))
161		df-neg 11583	. . . . . . . . . . . . . 14 ⊢ -1 = (0 − 1)
162	161	mpteq2i 5207	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (0(,)1) ↦ -1) = (𝑡 ∈ (0(,)1) ↦ (0 − 1))
163	160, 162	eqtr4di 2816	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (1 − 𝑡))) = (𝑡 ∈ (0(,)1) ↦ -1))
164	115, 147, 152, 163, 23	dvmptcmul 26339	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0(,)1) ↦ (𝑍 · -1)))
165		neg1cn 12345	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℂ
166		mulcom 11325	. . . . . . . . . . . . . 14 ⊢ ((𝑍 ∈ ℂ ∧ -1 ∈ ℂ) → (𝑍 · -1) = ( -1 · 𝑍))
167	23, 165, 166	sylancl 598	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · -1) = ( -1 · 𝑍))
168	23	mulm1d 11807	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ( -1 · 𝑍) = -𝑍)
169	167, 168	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · -1) = -𝑍)
170	169	mpteq2dv 5205	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑍 · -1)) = (𝑡 ∈ (0(,)1) ↦ -𝑍))
171	164, 170	eqtrd 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0(,)1) ↦ -𝑍))
172	115, 131, 129, 145, 148, 150, 171	dvmptadd 26335	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0(,)1) ↦ (𝑌 + -𝑍)))
173	14, 23	negsubd 11714	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 + -𝑍) = (𝑌 − 𝑍))
174	173	mpteq2dv 5205	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑌 + -𝑍)) = (𝑡 ∈ (0(,)1) ↦ (𝑌 − 𝑍)))
175	172, 174	eqtrd 2798	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0(,)1) ↦ (𝑌 − 𝑍)))
176	8	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ⊆ ℂ)
177	76, 125, 176, 12, 80	syl22anc 852	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)))
178	89	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((int‘(TopOpen‘ℂ_fld))‘𝐵) = 𝐵)
179	178	reseq2d 5986	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
180	177, 179	eqtrd 2798	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
181	46	oveq2d 7467	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)) = (ℂ D (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧))))
182		dvfcn 26283	. . . . . . . . . . . . 13 ⊢ (ℂ D (𝐹 ↾ 𝐵)):dom (ℂ D (𝐹 ↾ 𝐵))⟶ℂ
183	98	feq2d 6723	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D (𝐹 ↾ 𝐵)):dom (ℂ D (𝐹 ↾ 𝐵))⟶ℂ ↔ (ℂ D (𝐹 ↾ 𝐵)):𝐵⟶ℂ))
184	182, 183	mpbii 236	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)):𝐵⟶ℂ)
185	180	feq1d 6721	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D (𝐹 ↾ 𝐵)):𝐵⟶ℂ ↔ ((ℂ D 𝐹) ↾ 𝐵):𝐵⟶ℂ))
186	184, 185	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ 𝐵):𝐵⟶ℂ)
187	186	feqmptd 6984	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ (((ℂ D 𝐹) ↾ 𝐵)‘𝑧)))
188		fvres 6935	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐵 → (((ℂ D 𝐹) ↾ 𝐵)‘𝑧) = ((ℂ D 𝐹)‘𝑧))
189	188	mpteq2ia 5206	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐵 ↦ (((ℂ D 𝐹) ↾ 𝐵)‘𝑧)) = (𝑧 ∈ 𝐵 ↦ ((ℂ D 𝐹)‘𝑧))
190	187, 189	eqtrdi 2814	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ ((ℂ D 𝐹)‘𝑧)))
191	180, 181, 190	3eqtr3d 2806	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧))) = (𝑧 ∈ 𝐵 ↦ ((ℂ D 𝐹)‘𝑧)))
192		fveq2 6916	. . . . . . . 8 ⊢ (𝑧 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → ((ℂ D 𝐹)‘𝑧) = ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
193	115, 117, 120, 122, 127, 128, 175, 191, 47, 192	dvmptco 26347	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
194	113, 193	eqtrd 2798	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
195	194	dmeqd 5899	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = dom (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
196		ovex 7484	. . . . . . 7 ⊢ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V
197	196	rgenw 3084	. . . . . 6 ⊢ ∀𝑡 ∈ (0(,)1)(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V
198		dmmptg 6262	. . . . . 6 ⊢ (∀𝑡 ∈ (0(,)1)(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V → dom (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))) = (0(,)1))
199	197, 198	mp1i 14	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))) = (0(,)1))
200	195, 199	eqtrd 2798	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (0(,)1))
201		dvlipcn.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
202	201	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑀 ∈ ℝ)
203	121	abscld 15650	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘(𝑌 − 𝑍)) ∈ ℝ)
204	202, 203	remulcld 11378	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑀 · (abs‘(𝑌 − 𝑍))) ∈ ℝ)
205	194	fveq1d 6918	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡) = ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))‘𝑡))
206		eqid 2763	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
207	206	fvmpt2 7036	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ (0(,)1) ∧ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V) → ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
208	196, 207	mpan2 704	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0(,)1) → ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
209	205, 208	sylan9eq 2818	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
210	209	fveq2d 6920	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = (abs‘(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
211		dvfcn 26283	. . . . . . . . . . 11 ⊢ (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ
212	5	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝐵 ⊆ dom (ℂ D 𝐹))
213	212, 120	sseldd 3914	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ dom (ℂ D 𝐹))
214		ffvelcdm 7113	. . . . . . . . . . 11 ⊢ (((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ ∧ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ dom (ℂ D 𝐹)) → ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
215	211, 213, 214	sylancr 599	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
216	215, 122	absmuld 15668	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))) = ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌 − 𝑍))))
217	210, 216	eqtrd 2798	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌 − 𝑍))))
218	215	abscld 15650	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ℝ)
219	201	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑀 ∈ ℝ)
220	122	abscld 15650	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘(𝑌 − 𝑍)) ∈ ℝ)
221	122	absge0d 15658	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 0 ≤ (abs‘(𝑌 − 𝑍)))
222		2fveq3 6921	. . . . . . . . . . 11 ⊢ (𝑦 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → (abs‘((ℂ D 𝐹)‘𝑦)) = (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
223	222	breq1d 5118	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → ((abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀 ↔ (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ≤ 𝑀))
224		dvlipcn.l	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)
225	224	ralrimiva 3158	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)
226		2fveq3 6921	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (abs‘((ℂ D 𝐹)‘𝑥)) = (abs‘((ℂ D 𝐹)‘𝑦)))
227	226	breq1d 5118	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀 ↔ (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀))
228	227	cbvralvw 3244	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀 ↔ ∀𝑦 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
229	225, 228	sylib 221	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
230	229	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ∀𝑦 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
231	223, 230, 120	rspcdva 3581	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ≤ 𝑀)
232	218, 219, 220, 221, 231	lemul1ad 12296	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌 − 𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
233	217, 232	eqbrtrd 5133	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
234	233	ralrimiva 3158	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ∀𝑡 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
235		nfv 1949	. . . . . . 7 ⊢ Ⅎ𝑧(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))
236		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑡abs
237		nfcv 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑡ℝ
238		nfcv 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑡 D
239		nfmpt1 5210	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
240	237, 238, 239	nfov 7481	. . . . . . . . . 10 ⊢ Ⅎ𝑡(ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
241		nfcv 2926	. . . . . . . . . 10 ⊢ Ⅎ𝑡𝑧
242	240, 241	nffv 6926	. . . . . . . . 9 ⊢ Ⅎ𝑡((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)
243	236, 242	nffv 6926	. . . . . . . 8 ⊢ Ⅎ𝑡(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧))
244		nfcv 2926	. . . . . . . 8 ⊢ Ⅎ𝑡 ≤
245		nfcv 2926	. . . . . . . 8 ⊢ Ⅎ𝑡(𝑀 · (abs‘(𝑌 − 𝑍)))
246	243, 244, 245	nfbr 5158	. . . . . . 7 ⊢ Ⅎ𝑡(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))
247		2fveq3 6921	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)))
248	247	breq1d 5118	. . . . . . 7 ⊢ (𝑡 = 𝑧 → ((abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))) ↔ (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))))
249	235, 246, 248	cbvralw 3308	. . . . . 6 ⊢ (∀𝑡 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))) ↔ ∀𝑧 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
250	234, 249	sylib 221	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ∀𝑧 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
251	250	r19.21bi 3258	. . . 4 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
252	3, 4, 102, 200, 204, 251	dvlip 26368	. . 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 718	. 2 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0))) ≤ ((𝑀 · (abs‘(𝑌 − 𝑍))) · (abs‘(1 − 0))))
254		oveq2 7459	. . . . . . . . 9 ⊢ (𝑡 = 1 → (𝑌 · 𝑡) = (𝑌 · 1))
255		oveq2 7459	. . . . . . . . . . 11 ⊢ (𝑡 = 1 → (1 − 𝑡) = (1 − 1))
256		1m1e0 12455	. . . . . . . . . . 11 ⊢ (1 − 1) = 0
257	255, 256	eqtrdi 2814	. . . . . . . . . 10 ⊢ (𝑡 = 1 → (1 − 𝑡) = 0)
258	257	oveq2d 7467	. . . . . . . . 9 ⊢ (𝑡 = 1 → (𝑍 · (1 − 𝑡)) = (𝑍 · 0))
259	254, 258	oveq12d 7469	. . . . . . . 8 ⊢ (𝑡 = 1 → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑌 · 1) + (𝑍 · 0)))
260	259	fveq2d 6920	. . . . . . 7 ⊢ (𝑡 = 1 → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝐹‘((𝑌 · 1) + (𝑍 · 0))))
261		eqid 2763	. . . . . . 7 ⊢ (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
262		fvex 6929	. . . . . . 7 ⊢ (𝐹‘((𝑌 · 1) + (𝑍 · 0))) ∈ V
263	260, 261, 262	fvmpt 7024	. . . . . 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 11548	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · 0) = 0)
266	143, 265	oveq12d 7469	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 1) + (𝑍 · 0)) = (𝑌 + 0))
267	14	addridd 11549	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 + 0) = 𝑌)
268	266, 267	eqtrd 2798	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 1) + (𝑍 · 0)) = 𝑌)
269	268	fveq2d 6920	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹‘((𝑌 · 1) + (𝑍 · 0))) = (𝐹‘𝑌))
270	264, 269	eqtrid 2810	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) = (𝐹‘𝑌))
271		oveq2 7459	. . . . . . . . 9 ⊢ (𝑡 = 0 → (𝑌 · 𝑡) = (𝑌 · 0))
272		oveq2 7459	. . . . . . . . . . 11 ⊢ (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
273		1m0e1 12502	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
274	272, 273	eqtrdi 2814	. . . . . . . . . 10 ⊢ (𝑡 = 0 → (1 − 𝑡) = 1)
275	274	oveq2d 7467	. . . . . . . . 9 ⊢ (𝑡 = 0 → (𝑍 · (1 − 𝑡)) = (𝑍 · 1))
276	271, 275	oveq12d 7469	. . . . . . . 8 ⊢ (𝑡 = 0 → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑌 · 0) + (𝑍 · 1)))
277	276	fveq2d 6920	. . . . . . 7 ⊢ (𝑡 = 0 → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝐹‘((𝑌 · 0) + (𝑍 · 1))))
278		fvex 6929	. . . . . . 7 ⊢ (𝐹‘((𝑌 · 0) + (𝑍 · 1))) ∈ V
279	277, 261, 278	fvmpt 7024	. . . . . 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 11548	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 · 0) = 0)
282	23	mulridd 11365	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · 1) = 𝑍)
283	281, 282	oveq12d 7469	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 0) + (𝑍 · 1)) = (0 + 𝑍))
284	23	addlidd 11550	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0 + 𝑍) = 𝑍)
285	283, 284	eqtrd 2798	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 0) + (𝑍 · 1)) = 𝑍)
286	285	fveq2d 6920	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹‘((𝑌 · 0) + (𝑍 · 1))) = (𝐹‘𝑍))
287	280, 286	eqtrid 2810	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0) = (𝐹‘𝑍))
288	270, 287	oveq12d 7469	. . 3 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0)) = ((𝐹‘𝑌) − (𝐹‘𝑍)))
289	288	fveq2d 6920	. 2 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0))) = (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))))
290	273	fveq2i 6919	. . . . 5 ⊢ (abs‘(1 − 0)) = (abs‘1)
291		abs1 15507	. . . . 5 ⊢ (abs‘1) = 1
292	290, 291	eqtri 2786	. . . 4 ⊢ (abs‘(1 − 0)) = 1
293	292	oveq2i 7462	. . 3 ⊢ ((𝑀 · (abs‘(𝑌 − 𝑍))) · (abs‘(1 − 0))) = ((𝑀 · (abs‘(𝑌 − 𝑍))) · 1)
294	204	recnd 11376	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑀 · (abs‘(𝑌 − 𝑍))) ∈ ℂ)
295	294	mulridd 11365	. . 3 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑀 · (abs‘(𝑌 − 𝑍))) · 1) = (𝑀 · (abs‘(𝑌 − 𝑍))))
296	293, 295	eqtrid 2810	. 2 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑀 · (abs‘(𝑌 − 𝑍))) · (abs‘(1 − 0))) = (𝑀 · (abs‘(𝑌 − 𝑍))))
297	253, 289, 296	3brtr3d 5142	1 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ∀wral 3080 Vcvv 3454 ⊆ wss 3900 ∩ cin 4092 {cpr 4590 class class class wbr 5108 ↦ cmpt 5192 dom cdm 5658 ran crn 5659 ↾ cres 5660 ∘ ccom 5662 ⟶wf 6562 ‘cfv 6566 (class class class)co 7451 ℂcc 11237 ℝcr 11238 0cc0 11239 1c1 11240 + caddc 11242 · cmul 11244 ℝ^*cxr 11381 ≤ cle 11383 − cmin 11580 -cneg 11581 (,)cioo 13516 [,]cicc 13519 abscabs 15444 TopOpenctopn 17642 topGenctg 17658 ∞Metcxmet 21714 ballcbl 21716 ℂ_fldccnfld 21729 Topctop 23266 intcnt 23390 Cn ccn 23597 ×_t ctx 23934 –cn→ccncf 25252 D cdv 26238

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-pre-sup 11317 ax-addf 11318

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-isom 6575 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-of 7725 df-om 7912 df-1st 8035 df-2nd 8036 df-supp 8215 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-2o 8515 df-er 8755 df-map 8887 df-pm 8888 df-ixp 8964 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-fsupp 9392 df-fi 9440 df-sup 9471 df-inf 9472 df-oi 9541 df-card 10057 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-2 12445 df-3 12446 df-4 12447 df-5 12448 df-6 12449 df-7 12450 df-8 12451 df-9 12452 df-n0 12647 df-z 12734 df-dec 12855 df-uz 13006 df-q 13116 df-rp 13161 df-xneg 13281 df-xadd 13282 df-xmul 13283 df-ioo 13520 df-ico 13522 df-icc 13523 df-fz 13680 df-fzo 13829 df-seq 14185 df-exp 14245 df-hash 14516 df-cj 15309 df-re 15310 df-im 15311 df-sqrt 15445 df-abs 15446 df-struct 17369 df-sets 17386 df-slot 17404 df-ndx 17416 df-base 17432 df-ress 17453 df-plusg 17486 df-mulr 17487 df-starv 17488 df-sca 17489 df-vsca 17490 df-ip 17491 df-tset 17492 df-ple 17493 df-ds 17495 df-unif 17496 df-hom 17497 df-cco 17498 df-euf 17499 df-rest 17643 df-topn 17644 df-0g 17662 df-gsum 17663 df-topgen 17664 df-pt 17665 df-prds 17668 df-xrs 17724 df-qtop 17729 df-imas 17730 df-xps 17732 df-mre 17806 df-mrc 17807 df-acs 17809 df-mgm 18866 df-sgrp 18958 df-mnd 18974 df-submnd 19029 df-mulg 19328 df-cntz 19582 df-cmn 20047 df-psmet 21721 df-xmet 21722 df-met 21723 df-bl 21724 df-mopn 21725 df-fbas 21726 df-fg 21727 df-cnfld 21730 df-top 23267 df-topon 23284 df-topsp 23306 df-bases 23319 df-cld 23392 df-ntr 23393 df-cls 23394 df-nei 23471 df-lp 23509 df-perf 23510 df-cn 23600 df-cnp 23601 df-haus 23688 df-cmp 23760 df-tx 23936 df-hmeo 24129 df-fil 24220 df-fm 24312 df-flim 24313 df-flf 24314 df-xms 24694 df-ms 24695 df-tms 24696 df-cncf 25254 df-limc 26241 df-dv 26242

This theorem is used by: dvlip2 26370 dv11cn 26376

W3C validator