Step | Hyp | Ref
| Expression |
1 | | df-dv 23631 |
. . . . . . . . . . . . . . . . . . . 20
⊢ D =
(𝑠 ∈ 𝒫
ℂ, 𝑓 ∈ (ℂ
↑pm 𝑠) ↦ ∪
𝑥 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))) |
2 | 1 | dmmpt2ssx 7235 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom D
⊆ ∪ 𝑠 ∈ 𝒫 ℂ({𝑠} × (ℂ ↑pm
𝑠)) |
3 | | simpl 473 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
〈𝑆, 𝐹〉 ∈ dom D ) |
4 | 2, 3 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
〈𝑆, 𝐹〉 ∈ ∪ 𝑠 ∈ 𝒫 ℂ({𝑠} × (ℂ ↑pm
𝑠))) |
5 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 𝑆 → (ℂ ↑pm
𝑠) = (ℂ
↑pm 𝑆)) |
6 | 5 | opeliunxp2 5260 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑆, 𝐹〉 ∈ ∪ 𝑠 ∈ 𝒫 ℂ({𝑠} × (ℂ ↑pm
𝑠)) ↔ (𝑆 ∈ 𝒫 ℂ ∧
𝐹 ∈ (ℂ
↑pm 𝑆))) |
7 | 4, 6 | sylib 208 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝑆 ∈ 𝒫 ℂ ∧
𝐹 ∈ (ℂ
↑pm 𝑆))) |
8 | 7 | simprd 479 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → 𝐹 ∈ (ℂ
↑pm 𝑆)) |
9 | | cnex 10017 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ
∈ V |
10 | 7 | simpld 475 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → 𝑆 ∈ 𝒫
ℂ) |
11 | | elpm2g 7874 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℂ
∈ V ∧ 𝑆 ∈
𝒫 ℂ) → (𝐹 ∈ (ℂ ↑pm
𝑆) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆))) |
12 | 9, 10, 11 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝐹 ∈ (ℂ
↑pm 𝑆) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆))) |
13 | 8, 12 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆)) |
14 | 13 | simpld 475 |
. . . . . . . . . . . . . 14
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → 𝐹:dom 𝐹⟶ℂ) |
15 | 14 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → 𝐹:dom 𝐹⟶ℂ) |
16 | 2 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑆, 𝐹〉 ∈ dom D →
〈𝑆, 𝐹〉 ∈ ∪ 𝑠 ∈ 𝒫 ℂ({𝑠} × (ℂ ↑pm
𝑠))) |
17 | 16, 6 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑆, 𝐹〉 ∈ dom D →
(𝑆 ∈ 𝒫 ℂ
∧ 𝐹 ∈ (ℂ
↑pm 𝑆))) |
18 | 17 | simprd 479 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑆, 𝐹〉 ∈ dom D → 𝐹 ∈ (ℂ
↑pm 𝑆)) |
19 | 17 | simpld 475 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑆, 𝐹〉 ∈ dom D → 𝑆 ∈ 𝒫
ℂ) |
20 | 9, 19, 11 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑆, 𝐹〉 ∈ dom D →
(𝐹 ∈ (ℂ
↑pm 𝑆) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆))) |
21 | 18, 20 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑆, 𝐹〉 ∈ dom D →
(𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆)) |
22 | 21 | simprd 479 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑆, 𝐹〉 ∈ dom D → dom
𝐹 ⊆ 𝑆) |
23 | 22 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → dom 𝐹 ⊆ 𝑆) |
24 | 10 | elpwid 4170 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → 𝑆 ⊆
ℂ) |
25 | 23, 24 | sstrd 3613 |
. . . . . . . . . . . . . 14
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → dom 𝐹 ⊆
ℂ) |
26 | 25 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → dom 𝐹 ⊆ ℂ) |
27 | | perfdvf.1 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐾 =
(TopOpen‘ℂfld) |
28 | 27 | cnfldtopon 22586 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐾 ∈
(TopOn‘ℂ) |
29 | | resttopon 20965 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ (𝐾
↾t 𝑆)
∈ (TopOn‘𝑆)) |
30 | 28, 24, 29 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝐾 ↾t 𝑆) ∈ (TopOn‘𝑆)) |
31 | | topontop 20718 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ↾t 𝑆) ∈ (TopOn‘𝑆) → (𝐾 ↾t 𝑆) ∈ Top) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝐾 ↾t 𝑆) ∈ Top) |
33 | | toponuni 20719 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ (𝐾 ↾t 𝑆)) |
34 | 30, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → 𝑆 = ∪
(𝐾 ↾t
𝑆)) |
35 | 23, 34 | sseqtrd 3641 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → dom 𝐹 ⊆ ∪ (𝐾
↾t 𝑆)) |
36 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ ∪ (𝐾
↾t 𝑆) =
∪ (𝐾 ↾t 𝑆) |
37 | 36 | ntrss2 20861 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ↾t 𝑆) ∈ Top ∧ dom 𝐹 ⊆ ∪ (𝐾
↾t 𝑆))
→ ((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ dom 𝐹) |
38 | 32, 35, 37 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ dom 𝐹) |
39 | 38 | sselda 3603 |
. . . . . . . . . . . . 13
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → 𝑥 ∈ dom 𝐹) |
40 | 15, 26, 39 | dvlem 23660 |
. . . . . . . . . . . 12
⊢
((((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) ∧ 𝑧 ∈ (dom 𝐹 ∖ {𝑥})) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) ∈ ℂ) |
41 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) = (𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) |
42 | 40, 41 | fmptd 6385 |
. . . . . . . . . . 11
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → (𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))):(dom 𝐹 ∖ {𝑥})⟶ℂ) |
43 | 26 | ssdifssd 3748 |
. . . . . . . . . . 11
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → (dom 𝐹 ∖ {𝑥}) ⊆ ℂ) |
44 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → 𝐾 ∈
(TopOn‘ℂ)) |
45 | 36 | ntrss3 20864 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 ↾t 𝑆) ∈ Top ∧ dom 𝐹 ⊆ ∪ (𝐾
↾t 𝑆))
→ ((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ ∪
(𝐾 ↾t
𝑆)) |
46 | 32, 35, 45 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ ∪
(𝐾 ↾t
𝑆)) |
47 | 46, 34 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ 𝑆) |
48 | | restabs 20969 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ ((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ 𝑆 ∧ 𝑆 ∈ 𝒫 ℂ) → ((𝐾 ↾t 𝑆) ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) = (𝐾 ↾t ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹))) |
49 | 44, 47, 10, 48 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → ((𝐾 ↾t 𝑆) ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) = (𝐾 ↾t ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹))) |
50 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝐾 ↾t 𝑆) ∈ Perf) |
51 | 36 | ntropn 20853 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ↾t 𝑆) ∈ Top ∧ dom 𝐹 ⊆ ∪ (𝐾
↾t 𝑆))
→ ((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ∈ (𝐾 ↾t 𝑆)) |
52 | 32, 35, 51 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ∈ (𝐾 ↾t 𝑆)) |
53 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ↾t 𝑆) ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) = ((𝐾 ↾t 𝑆) ↾t ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) |
54 | 36, 53 | perfopn 20989 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ↾t 𝑆) ∈ Perf ∧
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ∈ (𝐾 ↾t 𝑆)) → ((𝐾 ↾t 𝑆) ↾t ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) ∈ Perf) |
55 | 50, 52, 54 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → ((𝐾 ↾t 𝑆) ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) ∈ Perf) |
56 | 49, 55 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝐾 ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) ∈ Perf) |
57 | 27 | cnfldtop 22587 |
. . . . . . . . . . . . . . . 16
⊢ 𝐾 ∈ Top |
58 | 47, 24 | sstrd 3613 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ ℂ) |
59 | 28 | toponunii 20721 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ =
∪ 𝐾 |
60 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) = (𝐾 ↾t ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) |
61 | 59, 60 | restperf 20988 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ Top ∧
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ ℂ) → ((𝐾 ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) ∈ Perf ↔ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) ⊆ ((limPt‘𝐾)‘((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)))) |
62 | 57, 58, 61 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → ((𝐾 ↾t
((int‘(𝐾
↾t 𝑆))‘dom 𝐹)) ∈ Perf ↔ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) ⊆ ((limPt‘𝐾)‘((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)))) |
63 | 56, 62 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ ((limPt‘𝐾)‘((int‘(𝐾 ↾t 𝑆))‘dom 𝐹))) |
64 | 57 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → 𝐾 ∈ Top) |
65 | 59 | lpss3 20948 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ Top ∧ dom 𝐹 ⊆ ℂ ∧
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ dom 𝐹) → ((limPt‘𝐾)‘((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) ⊆ ((limPt‘𝐾)‘dom 𝐹)) |
66 | 64, 25, 38, 65 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((limPt‘𝐾)‘((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) ⊆ ((limPt‘𝐾)‘dom 𝐹)) |
67 | 63, 66 | sstrd 3613 |
. . . . . . . . . . . . 13
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
((int‘(𝐾
↾t 𝑆))‘dom 𝐹) ⊆ ((limPt‘𝐾)‘dom 𝐹)) |
68 | 67 | sselda 3603 |
. . . . . . . . . . . 12
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → 𝑥 ∈ ((limPt‘𝐾)‘dom 𝐹)) |
69 | 59 | lpdifsn 20947 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Top ∧ dom 𝐹 ⊆ ℂ) → (𝑥 ∈ ((limPt‘𝐾)‘dom 𝐹) ↔ 𝑥 ∈ ((limPt‘𝐾)‘(dom 𝐹 ∖ {𝑥})))) |
70 | 57, 26, 69 | sylancr 695 |
. . . . . . . . . . . 12
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → (𝑥 ∈ ((limPt‘𝐾)‘dom 𝐹) ↔ 𝑥 ∈ ((limPt‘𝐾)‘(dom 𝐹 ∖ {𝑥})))) |
71 | 68, 70 | mpbid 222 |
. . . . . . . . . . 11
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → 𝑥 ∈ ((limPt‘𝐾)‘(dom 𝐹 ∖ {𝑥}))) |
72 | 42, 43, 71, 27 | limcmo 23646 |
. . . . . . . . . 10
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹)) → ∃*𝑦 𝑦 ∈ ((𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)) |
73 | 72 | ex 450 |
. . . . . . . . 9
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) → ∃*𝑦 𝑦 ∈ ((𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))) |
74 | | moanimv 2531 |
. . . . . . . . 9
⊢
(∃*𝑦(𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) ∧ 𝑦 ∈ ((𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)) ↔ (𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) → ∃*𝑦 𝑦 ∈ ((𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))) |
75 | 73, 74 | sylibr 224 |
. . . . . . . 8
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
∃*𝑦(𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) ∧ 𝑦 ∈ ((𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))) |
76 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝐾 ↾t 𝑆) = (𝐾 ↾t 𝑆) |
77 | 76, 27, 41, 24, 14, 23 | eldv 23662 |
. . . . . . . . 9
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝑥(𝑆 D 𝐹)𝑦 ↔ (𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) ∧ 𝑦 ∈ ((𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))) |
78 | 77 | mobidv 2491 |
. . . . . . . 8
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
(∃*𝑦 𝑥(𝑆 D 𝐹)𝑦 ↔ ∃*𝑦(𝑥 ∈ ((int‘(𝐾 ↾t 𝑆))‘dom 𝐹) ∧ 𝑦 ∈ ((𝑧 ∈ (dom 𝐹 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))) |
79 | 75, 78 | mpbird 247 |
. . . . . . 7
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
∃*𝑦 𝑥(𝑆 D 𝐹)𝑦) |
80 | 79 | alrimiv 1855 |
. . . . . 6
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
∀𝑥∃*𝑦 𝑥(𝑆 D 𝐹)𝑦) |
81 | | reldv 23634 |
. . . . . . 7
⊢ Rel
(𝑆 D 𝐹) |
82 | | dffun6 5903 |
. . . . . . 7
⊢ (Fun
(𝑆 D 𝐹) ↔ (Rel (𝑆 D 𝐹) ∧ ∀𝑥∃*𝑦 𝑥(𝑆 D 𝐹)𝑦)) |
83 | 81, 82 | mpbiran 953 |
. . . . . 6
⊢ (Fun
(𝑆 D 𝐹) ↔ ∀𝑥∃*𝑦 𝑥(𝑆 D 𝐹)𝑦) |
84 | 80, 83 | sylibr 224 |
. . . . 5
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → Fun (𝑆 D 𝐹)) |
85 | | funfn 5918 |
. . . . 5
⊢ (Fun
(𝑆 D 𝐹) ↔ (𝑆 D 𝐹) Fn dom (𝑆 D 𝐹)) |
86 | 84, 85 | sylib 208 |
. . . 4
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝑆 D 𝐹) Fn dom (𝑆 D 𝐹)) |
87 | | vex 3203 |
. . . . . . 7
⊢ 𝑦 ∈ V |
88 | 87 | elrn 5366 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝑆 D 𝐹) ↔ ∃𝑥 𝑥(𝑆 D 𝐹)𝑦) |
89 | 24, 14, 23 | dvcl 23663 |
. . . . . . . 8
⊢
(((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) ∧ 𝑥(𝑆 D 𝐹)𝑦) → 𝑦 ∈ ℂ) |
90 | 89 | ex 450 |
. . . . . . 7
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝑥(𝑆 D 𝐹)𝑦 → 𝑦 ∈ ℂ)) |
91 | 90 | exlimdv 1861 |
. . . . . 6
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) →
(∃𝑥 𝑥(𝑆 D 𝐹)𝑦 → 𝑦 ∈ ℂ)) |
92 | 88, 91 | syl5bi 232 |
. . . . 5
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝑦 ∈ ran (𝑆 D 𝐹) → 𝑦 ∈ ℂ)) |
93 | 92 | ssrdv 3609 |
. . . 4
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → ran (𝑆 D 𝐹) ⊆ ℂ) |
94 | | df-f 5892 |
. . . 4
⊢ ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ ↔ ((𝑆 D 𝐹) Fn dom (𝑆 D 𝐹) ∧ ran (𝑆 D 𝐹) ⊆ ℂ)) |
95 | 86, 93, 94 | sylanbrc 698 |
. . 3
⊢
((〈𝑆, 𝐹〉 ∈ dom D ∧ (𝐾 ↾t 𝑆) ∈ Perf) → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
96 | 95 | ex 450 |
. 2
⊢
(〈𝑆, 𝐹〉 ∈ dom D →
((𝐾 ↾t
𝑆) ∈ Perf →
(𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)) |
97 | | f0 6086 |
. . . 4
⊢
∅:∅⟶ℂ |
98 | | df-ov 6653 |
. . . . . 6
⊢ (𝑆 D 𝐹) = ( D ‘〈𝑆, 𝐹〉) |
99 | | ndmfv 6218 |
. . . . . 6
⊢ (¬
〈𝑆, 𝐹〉 ∈ dom D → ( D
‘〈𝑆, 𝐹〉) =
∅) |
100 | 98, 99 | syl5eq 2668 |
. . . . 5
⊢ (¬
〈𝑆, 𝐹〉 ∈ dom D → (𝑆 D 𝐹) = ∅) |
101 | 100 | dmeqd 5326 |
. . . . . 6
⊢ (¬
〈𝑆, 𝐹〉 ∈ dom D → dom (𝑆 D 𝐹) = dom ∅) |
102 | | dm0 5339 |
. . . . . 6
⊢ dom
∅ = ∅ |
103 | 101, 102 | syl6eq 2672 |
. . . . 5
⊢ (¬
〈𝑆, 𝐹〉 ∈ dom D → dom (𝑆 D 𝐹) = ∅) |
104 | 100, 103 | feq12d 6033 |
. . . 4
⊢ (¬
〈𝑆, 𝐹〉 ∈ dom D → ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ ↔
∅:∅⟶ℂ)) |
105 | 97, 104 | mpbiri 248 |
. . 3
⊢ (¬
〈𝑆, 𝐹〉 ∈ dom D → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
106 | 105 | a1d 25 |
. 2
⊢ (¬
〈𝑆, 𝐹〉 ∈ dom D → ((𝐾 ↾t 𝑆) ∈ Perf → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)) |
107 | 96, 106 | pm2.61i 176 |
1
⊢ ((𝐾 ↾t 𝑆) ∈ Perf → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |