Proof of Theorem dvres2lem
| Step | Hyp | Ref
| Expression |
| 1 | | dvres.t |
. . . . . . 7
⊢ 𝑇 = (𝐾 ↾t 𝑆) |
| 2 | | dvres.k |
. . . . . . . . 9
⊢ 𝐾 =
(TopOpen‘ℂfld) |
| 3 | 2 | cnfldtop 24804 |
. . . . . . . 8
⊢ 𝐾 ∈ Top |
| 4 | | dvres.s |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
| 5 | | cnex 11236 |
. . . . . . . . 9
⊢ ℂ
∈ V |
| 6 | | ssexg 5323 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ ℂ ∧ ℂ
∈ V) → 𝑆 ∈
V) |
| 7 | 4, 5, 6 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ V) |
| 8 | | resttop 23168 |
. . . . . . . 8
⊢ ((𝐾 ∈ Top ∧ 𝑆 ∈ V) → (𝐾 ↾t 𝑆) ∈ Top) |
| 9 | 3, 7, 8 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (𝐾 ↾t 𝑆) ∈ Top) |
| 10 | 1, 9 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ Top) |
| 11 | | inss1 4237 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
| 12 | | dvres.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
| 13 | 11, 12 | sstrid 3995 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝑆) |
| 14 | 2 | cnfldtopon 24803 |
. . . . . . . . . . 11
⊢ 𝐾 ∈
(TopOn‘ℂ) |
| 15 | | resttopon 23169 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ (𝐾
↾t 𝑆)
∈ (TopOn‘𝑆)) |
| 16 | 14, 4, 15 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾 ↾t 𝑆) ∈ (TopOn‘𝑆)) |
| 17 | 1, 16 | eqeltrid 2845 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ (TopOn‘𝑆)) |
| 18 | | toponuni 22920 |
. . . . . . . . 9
⊢ (𝑇 ∈ (TopOn‘𝑆) → 𝑆 = ∪ 𝑇) |
| 19 | 17, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 = ∪ 𝑇) |
| 20 | 13, 19 | sseqtrd 4020 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ ∪ 𝑇) |
| 21 | | difssd 4137 |
. . . . . . 7
⊢ (𝜑 → (∪ 𝑇
∖ 𝐵) ⊆ ∪ 𝑇) |
| 22 | 20, 21 | unssd 4192 |
. . . . . 6
⊢ (𝜑 → ((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵)) ⊆ ∪
𝑇) |
| 23 | | inundif 4479 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
| 24 | 12, 19 | sseqtrd 4020 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑇) |
| 25 | | ssdif 4144 |
. . . . . . . 8
⊢ (𝐴 ⊆ ∪ 𝑇
→ (𝐴 ∖ 𝐵) ⊆ (∪ 𝑇
∖ 𝐵)) |
| 26 | | unss2 4187 |
. . . . . . . 8
⊢ ((𝐴 ∖ 𝐵) ⊆ (∪
𝑇 ∖ 𝐵) → ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) ⊆ ((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) |
| 27 | 24, 25, 26 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) ⊆ ((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) |
| 28 | 23, 27 | eqsstrrid 4023 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) |
| 29 | | eqid 2737 |
. . . . . . 7
⊢ ∪ 𝑇 =
∪ 𝑇 |
| 30 | 29 | ntrss 23063 |
. . . . . 6
⊢ ((𝑇 ∈ Top ∧ ((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵)) ⊆ ∪
𝑇 ∧ 𝐴 ⊆ ((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) → ((int‘𝑇)‘𝐴) ⊆ ((int‘𝑇)‘((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵)))) |
| 31 | 10, 22, 28, 30 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → ((int‘𝑇)‘𝐴) ⊆ ((int‘𝑇)‘((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵)))) |
| 32 | | dvres2lem.d |
. . . . . . 7
⊢ (𝜑 → 𝑥(𝑆 D 𝐹)𝑦) |
| 33 | | dvres.g |
. . . . . . . 8
⊢ 𝐺 = (𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) |
| 34 | | dvres.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
| 35 | 1, 2, 33, 4, 34, 12 | eldv 25933 |
. . . . . . 7
⊢ (𝜑 → (𝑥(𝑆 D 𝐹)𝑦 ↔ (𝑥 ∈ ((int‘𝑇)‘𝐴) ∧ 𝑦 ∈ (𝐺 limℂ 𝑥)))) |
| 36 | 32, 35 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ((int‘𝑇)‘𝐴) ∧ 𝑦 ∈ (𝐺 limℂ 𝑥))) |
| 37 | 36 | simpld 494 |
. . . . 5
⊢ (𝜑 → 𝑥 ∈ ((int‘𝑇)‘𝐴)) |
| 38 | 31, 37 | sseldd 3984 |
. . . 4
⊢ (𝜑 → 𝑥 ∈ ((int‘𝑇)‘((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵)))) |
| 39 | | dvres2lem.x |
. . . 4
⊢ (𝜑 → 𝑥 ∈ 𝐵) |
| 40 | 38, 39 | elind 4200 |
. . 3
⊢ (𝜑 → 𝑥 ∈ (((int‘𝑇)‘((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) ∩ 𝐵)) |
| 41 | | dvres.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ 𝑆) |
| 42 | 41, 19 | sseqtrd 4020 |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ ∪ 𝑇) |
| 43 | | inss2 4238 |
. . . . . 6
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 |
| 44 | 43 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐵) |
| 45 | | eqid 2737 |
. . . . . 6
⊢ (𝑇 ↾t 𝐵) = (𝑇 ↾t 𝐵) |
| 46 | 29, 45 | restntr 23190 |
. . . . 5
⊢ ((𝑇 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑇
∧ (𝐴 ∩ 𝐵) ⊆ 𝐵) → ((int‘(𝑇 ↾t 𝐵))‘(𝐴 ∩ 𝐵)) = (((int‘𝑇)‘((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) ∩ 𝐵)) |
| 47 | 10, 42, 44, 46 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((int‘(𝑇 ↾t 𝐵))‘(𝐴 ∩ 𝐵)) = (((int‘𝑇)‘((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) ∩ 𝐵)) |
| 48 | 1 | oveq1i 7441 |
. . . . . . 7
⊢ (𝑇 ↾t 𝐵) = ((𝐾 ↾t 𝑆) ↾t 𝐵) |
| 49 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ Top) |
| 50 | | restabs 23173 |
. . . . . . . 8
⊢ ((𝐾 ∈ Top ∧ 𝐵 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐾 ↾t 𝑆) ↾t 𝐵) = (𝐾 ↾t 𝐵)) |
| 51 | 49, 41, 7, 50 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → ((𝐾 ↾t 𝑆) ↾t 𝐵) = (𝐾 ↾t 𝐵)) |
| 52 | 48, 51 | eqtrid 2789 |
. . . . . 6
⊢ (𝜑 → (𝑇 ↾t 𝐵) = (𝐾 ↾t 𝐵)) |
| 53 | 52 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 → (int‘(𝑇 ↾t 𝐵)) = (int‘(𝐾 ↾t 𝐵))) |
| 54 | 53 | fveq1d 6908 |
. . . 4
⊢ (𝜑 → ((int‘(𝑇 ↾t 𝐵))‘(𝐴 ∩ 𝐵)) = ((int‘(𝐾 ↾t 𝐵))‘(𝐴 ∩ 𝐵))) |
| 55 | 47, 54 | eqtr3d 2779 |
. . 3
⊢ (𝜑 → (((int‘𝑇)‘((𝐴 ∩ 𝐵) ∪ (∪ 𝑇 ∖ 𝐵))) ∩ 𝐵) = ((int‘(𝐾 ↾t 𝐵))‘(𝐴 ∩ 𝐵))) |
| 56 | 40, 55 | eleqtrd 2843 |
. 2
⊢ (𝜑 → 𝑥 ∈ ((int‘(𝐾 ↾t 𝐵))‘(𝐴 ∩ 𝐵))) |
| 57 | | limcresi 25920 |
. . . 4
⊢ (𝐺 limℂ 𝑥) ⊆ ((𝐺 ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) limℂ 𝑥) |
| 58 | 36 | simprd 495 |
. . . 4
⊢ (𝜑 → 𝑦 ∈ (𝐺 limℂ 𝑥)) |
| 59 | 57, 58 | sselid 3981 |
. . 3
⊢ (𝜑 → 𝑦 ∈ ((𝐺 ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) limℂ 𝑥)) |
| 60 | | difss 4136 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ⊆ (𝐴 ∩ 𝐵) |
| 61 | 60, 43 | sstri 3993 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ⊆ 𝐵 |
| 62 | 61 | sseli 3979 |
. . . . . . 7
⊢ (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) → 𝑧 ∈ 𝐵) |
| 63 | | fvres 6925 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑧) = (𝐹‘𝑧)) |
| 64 | 39 | fvresd 6926 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹 ↾ 𝐵)‘𝑥) = (𝐹‘𝑥)) |
| 65 | 63, 64 | oveqan12rd 7451 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) = ((𝐹‘𝑧) − (𝐹‘𝑥))) |
| 66 | 65 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥)) = (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) |
| 67 | 62, 66 | sylan2 593 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥})) → ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥)) = (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) |
| 68 | 67 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥))) = (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)))) |
| 69 | 33 | reseq1i 5993 |
. . . . . 6
⊢ (𝐺 ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) = ((𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) |
| 70 | | ssdif 4144 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 → ((𝐴 ∩ 𝐵) ∖ {𝑥}) ⊆ (𝐴 ∖ {𝑥})) |
| 71 | | resmpt 6055 |
. . . . . . 7
⊢ (((𝐴 ∩ 𝐵) ∖ {𝑥}) ⊆ (𝐴 ∖ {𝑥}) → ((𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) = (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)))) |
| 72 | 11, 70, 71 | mp2b 10 |
. . . . . 6
⊢ ((𝑧 ∈ (𝐴 ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) = (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) |
| 73 | 69, 72 | eqtri 2765 |
. . . . 5
⊢ (𝐺 ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) = (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥))) |
| 74 | 68, 73 | eqtr4di 2795 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥))) = (𝐺 ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥}))) |
| 75 | 74 | oveq1d 7446 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥) = ((𝐺 ↾ ((𝐴 ∩ 𝐵) ∖ {𝑥})) limℂ 𝑥)) |
| 76 | 59, 75 | eleqtrrd 2844 |
. 2
⊢ (𝜑 → 𝑦 ∈ ((𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)) |
| 77 | | eqid 2737 |
. . 3
⊢ (𝐾 ↾t 𝐵) = (𝐾 ↾t 𝐵) |
| 78 | | eqid 2737 |
. . 3
⊢ (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥))) = (𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥))) |
| 79 | 41, 4 | sstrd 3994 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ ℂ) |
| 80 | | fresin 6777 |
. . . 4
⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ 𝐵):(𝐴 ∩ 𝐵)⟶ℂ) |
| 81 | 34, 80 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹 ↾ 𝐵):(𝐴 ∩ 𝐵)⟶ℂ) |
| 82 | 77, 2, 78, 79, 81, 44 | eldv 25933 |
. 2
⊢ (𝜑 → (𝑥(𝐵 D (𝐹 ↾ 𝐵))𝑦 ↔ (𝑥 ∈ ((int‘(𝐾 ↾t 𝐵))‘(𝐴 ∩ 𝐵)) ∧ 𝑦 ∈ ((𝑧 ∈ ((𝐴 ∩ 𝐵) ∖ {𝑥}) ↦ ((((𝐹 ↾ 𝐵)‘𝑧) − ((𝐹 ↾ 𝐵)‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))) |
| 83 | 56, 76, 82 | mpbir2and 713 |
1
⊢ (𝜑 → 𝑥(𝐵 D (𝐹 ↾ 𝐵))𝑦) |