Step | Hyp | Ref
| Expression |
1 | | df-dv 24764 |
. . . . . . . . . . . . . . . . . . . 20
⊢ D =
(𝑠 ∈ 𝒫
ℂ, 𝑓 ∈ (ℂ
↑pm 𝑠)
↦ ∪ 𝑥 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))) |
2 | 1 | dmmpossx 7836 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom D
⊆ ∪ 𝑠 ∈ 𝒫 ℂ({𝑠} × (ℂ ↑pm 𝑠)) |
3 | | simpl 486 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
〈𝑆, 𝐹〉 ∈ dom D ) |
4 | 2, 3 | sseldi 3899 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
〈𝑆, 𝐹〉 ∈ ∪ 𝑠 ∈ 𝒫 ℂ({𝑠} × (ℂ ↑pm 𝑠))) |
5 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 𝑆 → (ℂ ↑pm 𝑠) = (ℂ ↑pm
𝑆)) |
6 | 5 | opeliunxp2 5707 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑆, 𝐹〉 ∈ ∪ 𝑠 ∈ 𝒫 ℂ({𝑠} × (ℂ ↑pm 𝑠)) ↔ (𝑆 ∈ 𝒫 ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))) |
7 | 4, 6 | sylib 221 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝑆 ∈ 𝒫 ℂ ∧
𝐹 ∈ (ℂ
↑pm 𝑆))) |
8 | 7 | simprd 499 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → 𝐹 ∈ (ℂ
↑pm 𝑆)) |
9 | | cnex 10810 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ
∈ V |
10 | 7 | simpld 498 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → 𝑆 ∈ 𝒫
ℂ) |
11 | | elpm2g 8525 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℂ
∈ V ∧ 𝑆 ∈
𝒫 ℂ) → (𝐹 ∈ (ℂ ↑pm 𝑆) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆))) |
12 | 9, 10, 11 | sylancr 590 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝐹 ∈ (ℂ
↑pm 𝑆)
↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆))) |
13 | 8, 12 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆)) |
14 | 13 | simpld 498 |
. . . . . . . . . . . . . 14
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → 𝐹:dom 𝐹⟶ℂ) |
15 | 14 | adantr 484 |
. . . . . . . . . . . . 13
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → 𝐹:dom 𝐹⟶ℂ) |
16 | 2 | sseli 3896 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑆, 𝐹〉 ∈ dom D →
〈𝑆, 𝐹〉 ∈ ∪ 𝑠 ∈ 𝒫 ℂ({𝑠} × (ℂ ↑pm 𝑠))) |
17 | 16, 6 | sylib 221 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑆, 𝐹〉 ∈ dom D →
(𝑆 ∈ 𝒫 ℂ
∧ 𝐹 ∈ (ℂ
↑pm 𝑆))) |
18 | 17 | simprd 499 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑆, 𝐹〉 ∈ dom D → 𝐹 ∈ (ℂ
↑pm 𝑆)) |
19 | 17 | simpld 498 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑆, 𝐹〉 ∈ dom D → 𝑆 ∈ 𝒫
ℂ) |
20 | 9, 19, 11 | sylancr 590 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑆, 𝐹〉 ∈ dom D →
(𝐹 ∈ (ℂ
↑pm 𝑆)
↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆))) |
21 | 18, 20 | mpbid 235 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑆, 𝐹〉 ∈ dom D →
(𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆)) |
22 | 21 | simprd 499 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑆, 𝐹〉 ∈ dom D → dom
𝐹 ⊆ 𝑆) |
23 | 22 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → dom 𝐹 ⊆ 𝑆) |
24 | 10 | elpwid 4524 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → 𝑆 ⊆
ℂ) |
25 | 23, 24 | sstrd 3911 |
. . . . . . . . . . . . . 14
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → dom 𝐹 ⊆
ℂ) |
26 | 25 | adantr 484 |
. . . . . . . . . . . . 13
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → dom 𝐹 ⊆ ℂ) |
27 | | perfdvf.1 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐾 =
(TopOpen‘ℂfld) |
28 | 27 | cnfldtopon 23680 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐾 ∈
(TopOn‘ℂ) |
29 | | resttopon 22058 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ (𝐾
↾t 𝑆)
∈ (TopOn‘𝑆)) |
30 | 28, 24, 29 | sylancr 590 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝐾 ↾t 𝑆) ∈ (TopOn‘𝑆)) |
31 | | topontop 21810 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ↾t 𝑆) ∈ (TopOn‘𝑆) → (𝐾 ↾t 𝑆) ∈ Top) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝐾 ↾t 𝑆) ∈ Top) |
33 | | toponuni 21811 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ (𝐾 ↾t 𝑆)) |
34 | 30, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → 𝑆 = ∪
(𝐾 ↾t
𝑆)) |
35 | 23, 34 | sseqtrd 3941 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → dom 𝐹 ⊆ ∪ (𝐾
↾t 𝑆)) |
36 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ ∪ (𝐾
↾t 𝑆) =
∪ (𝐾 ↾t 𝑆) |
37 | 36 | ntrss2 21954 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ↾t 𝑆) ∈ Top ∧ dom 𝐹 ⊆ ∪ (𝐾
↾t 𝑆))
→ ((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ dom 𝐹) |
38 | 32, 35, 37 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ dom 𝐹) |
39 | 38 | sselda 3901 |
. . . . . . . . . . . . 13
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → 𝑥 ∈ dom 𝐹) |
40 | 15, 26, 39 | dvlem 24793 |
. . . . . . . . . . . 12
⊢
((((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) ∧ 𝑧 ∈ (dom 𝐹 ∖ {𝑥})) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) ∈ ℂ) |
41 | 40 | fmpttd 6932 |
. . . . . . . . . . 11
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → (𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))):(dom 𝐹 ∖ {𝑥})⟶ℂ) |
42 | 26 | ssdifssd 4057 |
. . . . . . . . . . 11
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → (dom 𝐹 ∖ {𝑥}) ⊆ ℂ) |
43 | 36 | ntrss3 21957 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 ↾t 𝑆) ∈ Top ∧ dom 𝐹 ⊆ ∪ (𝐾
↾t 𝑆))
→ ((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ ∪
(𝐾 ↾t
𝑆)) |
44 | 32, 35, 43 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ ∪
(𝐾 ↾t
𝑆)) |
45 | 44, 34 | sseqtrrd 3942 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ 𝑆) |
46 | | restabs 22062 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ ((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ 𝑆 ∧ 𝑆 ∈ 𝒫 ℂ) → ((𝐾 ↾t 𝑆) ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) = (𝐾 ↾t ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹))) |
47 | 28, 45, 10, 46 | mp3an2i 1468 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → ((𝐾 ↾t 𝑆) ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) = (𝐾 ↾t ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹))) |
48 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝐾 ↾t 𝑆) ∈ Perf) |
49 | 36 | ntropn 21946 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ↾t 𝑆) ∈ Top ∧ dom 𝐹 ⊆ ∪ (𝐾
↾t 𝑆))
→ ((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ∈ (𝐾 ↾t 𝑆)) |
50 | 32, 35, 49 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ∈ (𝐾 ↾t 𝑆)) |
51 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ↾t 𝑆) ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) = ((𝐾 ↾t 𝑆) ↾t ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) |
52 | 36, 51 | perfopn 22082 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ↾t 𝑆) ∈ Perf ∧
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ∈ (𝐾 ↾t 𝑆)) → ((𝐾 ↾t 𝑆) ↾t ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) ∈ Perf) |
53 | 48, 50, 52 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → ((𝐾 ↾t 𝑆) ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) ∈ Perf) |
54 | 47, 53 | eqeltrrd 2839 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝐾 ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) ∈ Perf) |
55 | 27 | cnfldtop 23681 |
. . . . . . . . . . . . . . . 16
⊢ 𝐾 ∈ Top |
56 | 45, 24 | sstrd 3911 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ ℂ) |
57 | 28 | toponunii 21813 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ =
∪ 𝐾 |
58 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) = (𝐾 ↾t ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) |
59 | 57, 58 | restperf 22081 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ Top ∧
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ ℂ) → ((𝐾 ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) ∈ Perf ↔ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) ⊆ ((limPt‘𝐾)‘((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)))) |
60 | 55, 56, 59 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → ((𝐾 ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) ∈ Perf ↔ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) ⊆ ((limPt‘𝐾)‘((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)))) |
61 | 54, 60 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ ((limPt‘𝐾)‘((int‘(𝐾 ↾t 𝑆))‘dom 𝐹))) |
62 | 57 | lpss3 22041 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ Top ∧ dom 𝐹 ⊆ ℂ ∧
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ dom 𝐹) → ((limPt‘𝐾)‘((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) ⊆ ((limPt‘𝐾)‘dom 𝐹)) |
63 | 55, 25, 38, 62 | mp3an2i 1468 |
. . . . . . . . . . . . . 14
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((limPt‘𝐾)‘((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) ⊆ ((limPt‘𝐾)‘dom 𝐹)) |
64 | 61, 63 | sstrd 3911 |
. . . . . . . . . . . . 13
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ ((limPt‘𝐾)‘dom 𝐹)) |
65 | 64 | sselda 3901 |
. . . . . . . . . . . 12
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → 𝑥 ∈ ((limPt‘𝐾)‘dom 𝐹)) |
66 | 57 | lpdifsn 22040 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Top ∧ dom 𝐹 ⊆ ℂ) → (𝑥 ∈ ((limPt‘𝐾)‘dom 𝐹) ↔ 𝑥 ∈ ((limPt‘𝐾)‘(dom 𝐹 ∖ {𝑥})))) |
67 | 55, 26, 66 | sylancr 590 |
. . . . . . . . . . . 12
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → (𝑥 ∈ ((limPt‘𝐾)‘dom 𝐹) ↔ 𝑥 ∈ ((limPt‘𝐾)‘(dom 𝐹 ∖ {𝑥})))) |
68 | 65, 67 | mpbid 235 |
. . . . . . . . . . 11
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → 𝑥 ∈ ((limPt‘𝐾)‘(dom 𝐹 ∖ {𝑥}))) |
69 | 41, 42, 68, 27 | limcmo 24779 |
. . . . . . . . . 10
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → ∃*𝑦 𝑦 ∈ ((𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)) |
70 | 69 | ex 416 |
. . . . . . . . 9
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) → ∃*𝑦 𝑦 ∈ ((𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))) |
71 | | moanimv 2620 |
. . . . . . . . 9
⊢
(∃*𝑦(𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) ∧ 𝑦 ∈ ((𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)) ↔ (𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) → ∃*𝑦 𝑦 ∈ ((𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))) |
72 | 70, 71 | sylibr 237 |
. . . . . . . 8
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
∃*𝑦(𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) ∧ 𝑦 ∈ ((𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))) |
73 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝐾 ↾t 𝑆) = (𝐾 ↾t 𝑆) |
74 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) = (𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) |
75 | 73, 27, 74, 24, 14, 23 | eldv 24795 |
. . . . . . . . 9
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝑥(𝑆 D 𝐹)𝑦 ↔ (𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) ∧ 𝑦 ∈ ((𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))) |
76 | 75 | mobidv 2548 |
. . . . . . . 8
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
(∃*𝑦 𝑥(𝑆 D 𝐹)𝑦 ↔ ∃*𝑦(𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) ∧ 𝑦 ∈ ((𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))) |
77 | 72, 76 | mpbird 260 |
. . . . . . 7
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
∃*𝑦 𝑥(𝑆 D 𝐹)𝑦) |
78 | 77 | alrimiv 1935 |
. . . . . 6
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
∀𝑥∃*𝑦 𝑥(𝑆 D 𝐹)𝑦) |
79 | | reldv 24767 |
. . . . . . 7
⊢ Rel
(𝑆 D 𝐹) |
80 | | dffun6 6395 |
. . . . . . 7
⊢ (Fun
(𝑆 D 𝐹) ↔ (Rel (𝑆 D 𝐹) ∧ ∀𝑥∃*𝑦 𝑥(𝑆 D 𝐹)𝑦)) |
81 | 79, 80 | mpbiran 709 |
. . . . . 6
⊢ (Fun
(𝑆 D 𝐹) ↔ ∀𝑥∃*𝑦 𝑥(𝑆 D 𝐹)𝑦) |
82 | 78, 81 | sylibr 237 |
. . . . 5
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → Fun (𝑆 D 𝐹)) |
83 | 82 | funfnd 6411 |
. . . 4
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝑆 D 𝐹) Fn dom (𝑆 D 𝐹)) |
84 | | vex 3412 |
. . . . . . 7
⊢ 𝑦 ∈ V |
85 | 84 | elrn 5762 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝑆 D 𝐹) ↔ ∃𝑥 𝑥(𝑆 D 𝐹)𝑦) |
86 | 24, 14, 23 | dvcl 24796 |
. . . . . . . 8
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥(𝑆 D 𝐹)𝑦) → 𝑦 ∈ ℂ) |
87 | 86 | ex 416 |
. . . . . . 7
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝑥(𝑆 D 𝐹)𝑦 → 𝑦 ∈ ℂ)) |
88 | 87 | exlimdv 1941 |
. . . . . 6
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
(∃𝑥 𝑥(𝑆 D 𝐹)𝑦 → 𝑦 ∈ ℂ)) |
89 | 85, 88 | syl5bi 245 |
. . . . 5
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝑦 ∈ ran (𝑆 D 𝐹) → 𝑦 ∈ ℂ)) |
90 | 89 | ssrdv 3907 |
. . . 4
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → ran (𝑆 D 𝐹) ⊆ ℂ) |
91 | | df-f 6384 |
. . . 4
⊢ ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ ↔ ((𝑆 D 𝐹) Fn dom (𝑆 D 𝐹) ∧ ran (𝑆 D 𝐹) ⊆ ℂ)) |
92 | 83, 90, 91 | sylanbrc 586 |
. . 3
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
93 | 92 | ex 416 |
. 2
⊢
(〈𝑆, 𝐹〉 ∈ dom D →
((𝐾 ↾t
𝑆) ∈ Perf →
(𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)) |
94 | | f0 6600 |
. . . 4
⊢
∅:∅⟶ℂ |
95 | | df-ov 7216 |
. . . . . 6
⊢ (𝑆 D 𝐹) = ( D ‘〈𝑆, 𝐹〉) |
96 | | ndmfv 6747 |
. . . . . 6
⊢ (¬
〈𝑆, 𝐹〉 ∈ dom D → ( D
‘〈𝑆, 𝐹〉) =
∅) |
97 | 95, 96 | syl5eq 2790 |
. . . . 5
⊢ (¬
〈𝑆, 𝐹〉 ∈ dom D → (𝑆 D 𝐹) = ∅) |
98 | 97 | dmeqd 5774 |
. . . . . 6
⊢ (¬
〈𝑆, 𝐹〉 ∈ dom D → dom (𝑆 D 𝐹) = dom ∅) |
99 | | dm0 5789 |
. . . . . 6
⊢ dom
∅ = ∅ |
100 | 98, 99 | eqtrdi 2794 |
. . . . 5
⊢ (¬
〈𝑆, 𝐹〉 ∈ dom D → dom (𝑆 D 𝐹) = ∅) |
101 | 97, 100 | feq12d 6533 |
. . . 4
⊢ (¬
〈𝑆, 𝐹〉 ∈ dom D → ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ ↔
∅:∅⟶ℂ)) |
102 | 94, 101 | mpbiri 261 |
. . 3
⊢ (¬
〈𝑆, 𝐹〉 ∈ dom D → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
103 | 102 | a1d 25 |
. 2
⊢ (¬
〈𝑆, 𝐹〉 ∈ dom D → ((𝐾 ↾t 𝑆) ∈ Perf → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)) |
104 | 93, 103 | pm2.61i 185 |
1
⊢ ((𝐾 ↾t 𝑆) ∈ Perf → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |