Proof of Theorem dvres2lem
Step | Hyp | Ref
| Expression |
1 | | dvres.t |
. . . . . . 7
⊢ 𝑇 = (𝐾 ↾t 𝑆) |
2 | | dvres.k |
. . . . . . . . 9
⊢ 𝐾 =
(TopOpen‘ℂfld) |
3 | 2 | cnfldtop 22587 |
. . . . . . . 8
⊢ 𝐾 ∈ Top |
4 | | dvres.s |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
5 | | cnex 10017 |
. . . . . . . . 9
⊢ ℂ
∈ V |
6 | | ssexg 4804 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ ℂ ∧ ℂ
∈ V) → 𝑆 ∈
V) |
7 | 4, 5, 6 | sylancl 694 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ V) |
8 | | resttop 20964 |
. . . . . . . 8
⊢ ((𝐾 ∈ Top ∧ 𝑆 ∈ V) → (𝐾 ↾t 𝑆) ∈ Top) |
9 | 3, 7, 8 | sylancr 695 |
. . . . . . 7
⊢ (𝜑 → (𝐾 ↾t 𝑆) ∈ Top) |
10 | 1, 9 | syl5eqel 2705 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ Top) |
11 | | inss1 3833 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
12 | | dvres.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
13 | 11, 12 | syl5ss 3614 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝑆) |
14 | 2 | cnfldtopon 22586 |
. . . . . . . . . . 11
⊢ 𝐾 ∈
(TopOn‘ℂ) |
15 | | resttopon 20965 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ (𝐾
↾t 𝑆)
∈ (TopOn‘𝑆)) |
16 | 14, 4, 15 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾 ↾t 𝑆) ∈ (TopOn‘𝑆)) |
17 | 1, 16 | syl5eqel 2705 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ (TopOn‘𝑆)) |
18 | | toponuni 20719 |
. . . . . . . . 9
⊢ (𝑇 ∈ (TopOn‘𝑆) → 𝑆 = ∪ 𝑇) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 = ∪ 𝑇) |
20 | 13, 19 | sseqtrd 3641 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ ∪ 𝑇) |
21 | | difssd 3738 |
. . . . . . 7
⊢ (𝜑 → (∪ 𝑇
∖ 𝐵) ⊆ ∪ 𝑇) |
22 | 20, 21 | unssd 3789 |
. . . . . 6
⊢ (𝜑 → ((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵)) ⊆ ∪
𝑇) |
23 | | inundif 4046 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
24 | 12, 19 | sseqtrd 3641 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑇) |
25 | | ssdif 3745 |
. . . . . . . 8
⊢ (𝐴 ⊆ ∪ 𝑇
→ (𝐴 ∖ 𝐵) ⊆ (∪ 𝑇
∖ 𝐵)) |
26 | | unss2 3784 |
. . . . . . . 8
⊢ ((𝐴 ∖ 𝐵) ⊆ (∪
𝑇 ∖ 𝐵) → ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) ⊆ ((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) |
27 | 24, 25, 26 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) ⊆ ((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) |
28 | 23, 27 | syl5eqssr 3650 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) |
29 | | eqid 2622 |
. . . . . . 7
⊢ ∪ 𝑇 =
∪ 𝑇 |
30 | 29 | ntrss 20859 |
. . . . . 6
⊢ ((𝑇 ∈ Top ∧ ((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵)) ⊆ ∪
𝑇 ∧ 𝐴 ⊆ ((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) → ((int‘𝑇)‘𝐴) ⊆ ((int‘𝑇)‘((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵)))) |
31 | 10, 22, 28, 30 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → ((int‘𝑇)‘𝐴) ⊆ ((int‘𝑇)‘((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵)))) |
32 | | dvres2lem.d |
. . . . . . 7
⊢ (𝜑 → 𝑥(𝑆 D 𝐹)𝑦) |
33 | | dvres.g |
. . . . . . . 8
⊢ 𝐺 = (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) |
34 | | dvres.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
35 | 1, 2, 33, 4, 34, 12 | eldv 23662 |
. . . . . . 7
⊢ (𝜑 → (𝑥(𝑆 D 𝐹)𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐴) ∧ 𝑦 ∈ (𝐺 limℂ 𝑥)))) |
36 | 32, 35 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ((int‘𝑇)‘𝐴) ∧ 𝑦 ∈ (𝐺 limℂ 𝑥))) |
37 | 36 | simpld 475 |
. . . . 5
⊢ (𝜑 → 𝑥 ∈ ((int‘𝑇)‘𝐴)) |
38 | 31, 37 | sseldd 3604 |
. . . 4
⊢ (𝜑 → 𝑥 ∈ ((int‘𝑇)‘((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵)))) |
39 | | dvres2lem.x |
. . . 4
⊢ (𝜑 → 𝑥 ∈ 𝐵) |
40 | 38, 39 | elind 3798 |
. . 3
⊢ (𝜑 → 𝑥 ∈ (((int‘𝑇)‘((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) ∩ 𝐵)) |
41 | | dvres.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ 𝑆) |
42 | 41, 19 | sseqtrd 3641 |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ ∪ 𝑇) |
43 | | inss2 3834 |
. . . . . 6
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 |
44 | 43 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐵) |
45 | | eqid 2622 |
. . . . . 6
⊢ (𝑇 ↾t 𝐵) = (𝑇 ↾t 𝐵) |
46 | 29, 45 | restntr 20986 |
. . . . 5
⊢ ((𝑇 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑇
∧ (𝐴 ∩ 𝐵) ⊆ 𝐵) → ((int‘(𝑇 ↾t 𝐵))‘(𝐴 ∩ 𝐵)) = (((int‘𝑇)‘((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) ∩ 𝐵)) |
47 | 10, 42, 44, 46 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → ((int‘(𝑇 ↾t 𝐵))‘(𝐴 ∩ 𝐵)) = (((int‘𝑇)‘((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) ∩ 𝐵)) |
48 | 1 | oveq1i 6660 |
. . . . . . 7
⊢ (𝑇 ↾t 𝐵) = ((𝐾 ↾t 𝑆) ↾t 𝐵) |
49 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ Top) |
50 | | restabs 20969 |
. . . . . . . 8
⊢ ((𝐾 ∈ Top ∧ 𝐵 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐾 ↾t 𝑆) ↾t 𝐵) = (𝐾 ↾t 𝐵)) |
51 | 49, 41, 7, 50 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → ((𝐾 ↾t 𝑆) ↾t 𝐵) = (𝐾 ↾t 𝐵)) |
52 | 48, 51 | syl5eq 2668 |
. . . . . 6
⊢ (𝜑 → (𝑇 ↾t 𝐵) = (𝐾 ↾t 𝐵)) |
53 | 52 | fveq2d 6195 |
. . . . 5
⊢ (𝜑 → (int‘(𝑇 ↾t 𝐵)) = (int‘(𝐾 ↾t 𝐵))) |
54 | 53 | fveq1d 6193 |
. . . 4
⊢ (𝜑 → ((int‘(𝑇 ↾t 𝐵))‘(𝐴 ∩ 𝐵)) = ((int‘(𝐾 ↾t 𝐵))‘(𝐴 ∩ 𝐵))) |
55 | 47, 54 | eqtr3d 2658 |
. . 3
⊢ (𝜑 → (((int‘𝑇)‘((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) ∩ 𝐵) = ((int‘(𝐾 ↾t 𝐵))‘(𝐴 ∩ 𝐵))) |
56 | 40, 55 | eleqtrd 2703 |
. 2
⊢ (𝜑 → 𝑥 ∈ ((int‘(𝐾 ↾t 𝐵))‘(𝐴 ∩ 𝐵))) |
57 | | limcresi 23649 |
. . . 4
⊢ (𝐺 limℂ 𝑥) ⊆ ((𝐺 ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) limℂ 𝑥) |
58 | 36 | simprd 479 |
. . . 4
⊢ (𝜑 → 𝑦 ∈ (𝐺 limℂ 𝑥)) |
59 | 57, 58 | sseldi 3601 |
. . 3
⊢ (𝜑 → 𝑦 ∈ ((𝐺 ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) limℂ 𝑥)) |
60 | | difss 3737 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ⊆ (𝐴 ∩ 𝐵) |
61 | 60, 43 | sstri 3612 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ⊆ 𝐵 |
62 | 61 | sseli 3599 |
. . . . . . 7
⊢ (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) → 𝑧 ∈ 𝐵) |
63 | | fvres 6207 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑧) = (𝐹‘𝑧)) |
64 | | fvres 6207 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑥) = (𝐹‘𝑥)) |
65 | 39, 64 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹 ↾ 𝐵)‘𝑥) = (𝐹‘𝑥)) |
66 | 63, 65 | oveqan12rd 6670 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) = ((𝐹‘𝑧) − (𝐹‘𝑥))) |
67 | 66 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥)) = (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) |
68 | 62, 67 | sylan2 491 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥})) → ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥)) = (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) |
69 | 68 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥))) = (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)))) |
70 | 33 | reseq1i 5392 |
. . . . . 6
⊢ (𝐺 ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) = ((𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) |
71 | | ssdif 3745 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 → ((𝐴 ∩ 𝐵) ∖ {𝑥}) ⊆ (𝐴 ∖ {𝑥})) |
72 | | resmpt 5449 |
. . . . . . 7
⊢ (((𝐴 ∩ 𝐵) ∖ {𝑥}) ⊆ (𝐴 ∖ {𝑥}) → ((𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) = (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)))) |
73 | 11, 71, 72 | mp2b 10 |
. . . . . 6
⊢ ((𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) = (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) |
74 | 70, 73 | eqtri 2644 |
. . . . 5
⊢ (𝐺 ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) = (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) |
75 | 69, 74 | syl6eqr 2674 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥))) = (𝐺 ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥}))) |
76 | 75 | oveq1d 6665 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥) = ((𝐺 ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) limℂ 𝑥)) |
77 | 59, 76 | eleqtrrd 2704 |
. 2
⊢ (𝜑 → 𝑦 ∈ ((𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)) |
78 | | eqid 2622 |
. . 3
⊢ (𝐾 ↾t 𝐵) = (𝐾 ↾t 𝐵) |
79 | | eqid 2622 |
. . 3
⊢ (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥))) = (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥))) |
80 | 41, 4 | sstrd 3613 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ ℂ) |
81 | | fresin 6073 |
. . . 4
⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ 𝐵):(𝐴 ∩ 𝐵)⟶ℂ) |
82 | 34, 81 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹 ↾ 𝐵):(𝐴 ∩ 𝐵)⟶ℂ) |
83 | 78, 2, 79, 80, 82, 44 | eldv 23662 |
. 2
⊢ (𝜑 → (𝑥(𝐵 D (𝐹 ↾ 𝐵))𝑦 ↔ (𝑥 ∈ ((int‘(𝐾 ↾t 𝐵))‘(𝐴 ∩ 𝐵)) ∧ 𝑦 ∈ ((𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))) |
84 | 56, 77, 83 | mpbir2and 957 |
1
⊢ (𝜑 → 𝑥(𝐵 D (𝐹 ↾ 𝐵))𝑦) |