Step | Hyp | Ref
| Expression |
1 | | dvres.t |
. . . . . . 7
β’ π = (πΎ βΎt π) |
2 | | dvres.k |
. . . . . . . . 9
β’ πΎ =
(TopOpenββfld) |
3 | 2 | cnfldtop 24299 |
. . . . . . . 8
β’ πΎ β Top |
4 | | dvres.s |
. . . . . . . . 9
β’ (π β π β β) |
5 | | cnex 11190 |
. . . . . . . . 9
β’ β
β V |
6 | | ssexg 5323 |
. . . . . . . . 9
β’ ((π β β β§ β
β V) β π β
V) |
7 | 4, 5, 6 | sylancl 586 |
. . . . . . . 8
β’ (π β π β V) |
8 | | resttop 22663 |
. . . . . . . 8
β’ ((πΎ β Top β§ π β V) β (πΎ βΎt π) β Top) |
9 | 3, 7, 8 | sylancr 587 |
. . . . . . 7
β’ (π β (πΎ βΎt π) β Top) |
10 | 1, 9 | eqeltrid 2837 |
. . . . . 6
β’ (π β π β Top) |
11 | | inss1 4228 |
. . . . . . . . 9
β’ (π΄ β© π΅) β π΄ |
12 | | dvres.a |
. . . . . . . . 9
β’ (π β π΄ β π) |
13 | 11, 12 | sstrid 3993 |
. . . . . . . 8
β’ (π β (π΄ β© π΅) β π) |
14 | 2 | cnfldtopon 24298 |
. . . . . . . . . . 11
β’ πΎ β
(TopOnββ) |
15 | | resttopon 22664 |
. . . . . . . . . . 11
β’ ((πΎ β (TopOnββ)
β§ π β β)
β (πΎ
βΎt π)
β (TopOnβπ)) |
16 | 14, 4, 15 | sylancr 587 |
. . . . . . . . . 10
β’ (π β (πΎ βΎt π) β (TopOnβπ)) |
17 | 1, 16 | eqeltrid 2837 |
. . . . . . . . 9
β’ (π β π β (TopOnβπ)) |
18 | | toponuni 22415 |
. . . . . . . . 9
β’ (π β (TopOnβπ) β π = βͺ π) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
β’ (π β π = βͺ π) |
20 | 13, 19 | sseqtrd 4022 |
. . . . . . 7
β’ (π β (π΄ β© π΅) β βͺ π) |
21 | | difssd 4132 |
. . . . . . 7
β’ (π β (βͺ π
β π΅) β βͺ π) |
22 | 20, 21 | unssd 4186 |
. . . . . 6
β’ (π β ((π΄ β© π΅) βͺ (βͺ π β π΅)) β βͺ
π) |
23 | | inundif 4478 |
. . . . . . 7
β’ ((π΄ β© π΅) βͺ (π΄ β π΅)) = π΄ |
24 | 12, 19 | sseqtrd 4022 |
. . . . . . . 8
β’ (π β π΄ β βͺ π) |
25 | | ssdif 4139 |
. . . . . . . 8
β’ (π΄ β βͺ π
β (π΄ β π΅) β (βͺ π
β π΅)) |
26 | | unss2 4181 |
. . . . . . . 8
β’ ((π΄ β π΅) β (βͺ
π β π΅) β ((π΄ β© π΅) βͺ (π΄ β π΅)) β ((π΄ β© π΅) βͺ (βͺ π β π΅))) |
27 | 24, 25, 26 | 3syl 18 |
. . . . . . 7
β’ (π β ((π΄ β© π΅) βͺ (π΄ β π΅)) β ((π΄ β© π΅) βͺ (βͺ π β π΅))) |
28 | 23, 27 | eqsstrrid 4031 |
. . . . . 6
β’ (π β π΄ β ((π΄ β© π΅) βͺ (βͺ π β π΅))) |
29 | | eqid 2732 |
. . . . . . 7
β’ βͺ π =
βͺ π |
30 | 29 | ntrss 22558 |
. . . . . 6
β’ ((π β Top β§ ((π΄ β© π΅) βͺ (βͺ π β π΅)) β βͺ
π β§ π΄ β ((π΄ β© π΅) βͺ (βͺ π β π΅))) β ((intβπ)βπ΄) β ((intβπ)β((π΄ β© π΅) βͺ (βͺ π β π΅)))) |
31 | 10, 22, 28, 30 | syl3anc 1371 |
. . . . 5
β’ (π β ((intβπ)βπ΄) β ((intβπ)β((π΄ β© π΅) βͺ (βͺ π β π΅)))) |
32 | | dvres2lem.d |
. . . . . . 7
β’ (π β π₯(π D πΉ)π¦) |
33 | | dvres.g |
. . . . . . . 8
β’ πΊ = (π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) |
34 | | dvres.f |
. . . . . . . 8
β’ (π β πΉ:π΄βΆβ) |
35 | 1, 2, 33, 4, 34, 12 | eldv 25414 |
. . . . . . 7
β’ (π β (π₯(π D πΉ)π¦ β (π₯ β ((intβπ)βπ΄) β§ π¦ β (πΊ limβ π₯)))) |
36 | 32, 35 | mpbid 231 |
. . . . . 6
β’ (π β (π₯ β ((intβπ)βπ΄) β§ π¦ β (πΊ limβ π₯))) |
37 | 36 | simpld 495 |
. . . . 5
β’ (π β π₯ β ((intβπ)βπ΄)) |
38 | 31, 37 | sseldd 3983 |
. . . 4
β’ (π β π₯ β ((intβπ)β((π΄ β© π΅) βͺ (βͺ π β π΅)))) |
39 | | dvres2lem.x |
. . . 4
β’ (π β π₯ β π΅) |
40 | 38, 39 | elind 4194 |
. . 3
β’ (π β π₯ β (((intβπ)β((π΄ β© π΅) βͺ (βͺ π β π΅))) β© π΅)) |
41 | | dvres.b |
. . . . . 6
β’ (π β π΅ β π) |
42 | 41, 19 | sseqtrd 4022 |
. . . . 5
β’ (π β π΅ β βͺ π) |
43 | | inss2 4229 |
. . . . . 6
β’ (π΄ β© π΅) β π΅ |
44 | 43 | a1i 11 |
. . . . 5
β’ (π β (π΄ β© π΅) β π΅) |
45 | | eqid 2732 |
. . . . . 6
β’ (π βΎt π΅) = (π βΎt π΅) |
46 | 29, 45 | restntr 22685 |
. . . . 5
β’ ((π β Top β§ π΅ β βͺ π
β§ (π΄ β© π΅) β π΅) β ((intβ(π βΎt π΅))β(π΄ β© π΅)) = (((intβπ)β((π΄ β© π΅) βͺ (βͺ π β π΅))) β© π΅)) |
47 | 10, 42, 44, 46 | syl3anc 1371 |
. . . 4
β’ (π β ((intβ(π βΎt π΅))β(π΄ β© π΅)) = (((intβπ)β((π΄ β© π΅) βͺ (βͺ π β π΅))) β© π΅)) |
48 | 1 | oveq1i 7418 |
. . . . . . 7
β’ (π βΎt π΅) = ((πΎ βΎt π) βΎt π΅) |
49 | 3 | a1i 11 |
. . . . . . . 8
β’ (π β πΎ β Top) |
50 | | restabs 22668 |
. . . . . . . 8
β’ ((πΎ β Top β§ π΅ β π β§ π β V) β ((πΎ βΎt π) βΎt π΅) = (πΎ βΎt π΅)) |
51 | 49, 41, 7, 50 | syl3anc 1371 |
. . . . . . 7
β’ (π β ((πΎ βΎt π) βΎt π΅) = (πΎ βΎt π΅)) |
52 | 48, 51 | eqtrid 2784 |
. . . . . 6
β’ (π β (π βΎt π΅) = (πΎ βΎt π΅)) |
53 | 52 | fveq2d 6895 |
. . . . 5
β’ (π β (intβ(π βΎt π΅)) = (intβ(πΎ βΎt π΅))) |
54 | 53 | fveq1d 6893 |
. . . 4
β’ (π β ((intβ(π βΎt π΅))β(π΄ β© π΅)) = ((intβ(πΎ βΎt π΅))β(π΄ β© π΅))) |
55 | 47, 54 | eqtr3d 2774 |
. . 3
β’ (π β (((intβπ)β((π΄ β© π΅) βͺ (βͺ π β π΅))) β© π΅) = ((intβ(πΎ βΎt π΅))β(π΄ β© π΅))) |
56 | 40, 55 | eleqtrd 2835 |
. 2
β’ (π β π₯ β ((intβ(πΎ βΎt π΅))β(π΄ β© π΅))) |
57 | | limcresi 25401 |
. . . 4
β’ (πΊ limβ π₯) β ((πΊ βΎ ((π΄ β© π΅) β {π₯})) limβ π₯) |
58 | 36 | simprd 496 |
. . . 4
β’ (π β π¦ β (πΊ limβ π₯)) |
59 | 57, 58 | sselid 3980 |
. . 3
β’ (π β π¦ β ((πΊ βΎ ((π΄ β© π΅) β {π₯})) limβ π₯)) |
60 | | difss 4131 |
. . . . . . . . 9
β’ ((π΄ β© π΅) β {π₯}) β (π΄ β© π΅) |
61 | 60, 43 | sstri 3991 |
. . . . . . . 8
β’ ((π΄ β© π΅) β {π₯}) β π΅ |
62 | 61 | sseli 3978 |
. . . . . . 7
β’ (π§ β ((π΄ β© π΅) β {π₯}) β π§ β π΅) |
63 | | fvres 6910 |
. . . . . . . . 9
β’ (π§ β π΅ β ((πΉ βΎ π΅)βπ§) = (πΉβπ§)) |
64 | 39 | fvresd 6911 |
. . . . . . . . 9
β’ (π β ((πΉ βΎ π΅)βπ₯) = (πΉβπ₯)) |
65 | 63, 64 | oveqan12rd 7428 |
. . . . . . . 8
β’ ((π β§ π§ β π΅) β (((πΉ βΎ π΅)βπ§) β ((πΉ βΎ π΅)βπ₯)) = ((πΉβπ§) β (πΉβπ₯))) |
66 | 65 | oveq1d 7423 |
. . . . . . 7
β’ ((π β§ π§ β π΅) β ((((πΉ βΎ π΅)βπ§) β ((πΉ βΎ π΅)βπ₯)) / (π§ β π₯)) = (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) |
67 | 62, 66 | sylan2 593 |
. . . . . 6
β’ ((π β§ π§ β ((π΄ β© π΅) β {π₯})) β ((((πΉ βΎ π΅)βπ§) β ((πΉ βΎ π΅)βπ₯)) / (π§ β π₯)) = (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) |
68 | 67 | mpteq2dva 5248 |
. . . . 5
β’ (π β (π§ β ((π΄ β© π΅) β {π₯}) β¦ ((((πΉ βΎ π΅)βπ§) β ((πΉ βΎ π΅)βπ₯)) / (π§ β π₯))) = (π§ β ((π΄ β© π΅) β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)))) |
69 | 33 | reseq1i 5977 |
. . . . . 6
β’ (πΊ βΎ ((π΄ β© π΅) β {π₯})) = ((π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) βΎ ((π΄ β© π΅) β {π₯})) |
70 | | ssdif 4139 |
. . . . . . 7
β’ ((π΄ β© π΅) β π΄ β ((π΄ β© π΅) β {π₯}) β (π΄ β {π₯})) |
71 | | resmpt 6037 |
. . . . . . 7
β’ (((π΄ β© π΅) β {π₯}) β (π΄ β {π₯}) β ((π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) βΎ ((π΄ β© π΅) β {π₯})) = (π§ β ((π΄ β© π΅) β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)))) |
72 | 11, 70, 71 | mp2b 10 |
. . . . . 6
β’ ((π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) βΎ ((π΄ β© π΅) β {π₯})) = (π§ β ((π΄ β© π΅) β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) |
73 | 69, 72 | eqtri 2760 |
. . . . 5
β’ (πΊ βΎ ((π΄ β© π΅) β {π₯})) = (π§ β ((π΄ β© π΅) β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) |
74 | 68, 73 | eqtr4di 2790 |
. . . 4
β’ (π β (π§ β ((π΄ β© π΅) β {π₯}) β¦ ((((πΉ βΎ π΅)βπ§) β ((πΉ βΎ π΅)βπ₯)) / (π§ β π₯))) = (πΊ βΎ ((π΄ β© π΅) β {π₯}))) |
75 | 74 | oveq1d 7423 |
. . 3
β’ (π β ((π§ β ((π΄ β© π΅) β {π₯}) β¦ ((((πΉ βΎ π΅)βπ§) β ((πΉ βΎ π΅)βπ₯)) / (π§ β π₯))) limβ π₯) = ((πΊ βΎ ((π΄ β© π΅) β {π₯})) limβ π₯)) |
76 | 59, 75 | eleqtrrd 2836 |
. 2
β’ (π β π¦ β ((π§ β ((π΄ β© π΅) β {π₯}) β¦ ((((πΉ βΎ π΅)βπ§) β ((πΉ βΎ π΅)βπ₯)) / (π§ β π₯))) limβ π₯)) |
77 | | eqid 2732 |
. . 3
β’ (πΎ βΎt π΅) = (πΎ βΎt π΅) |
78 | | eqid 2732 |
. . 3
β’ (π§ β ((π΄ β© π΅) β {π₯}) β¦ ((((πΉ βΎ π΅)βπ§) β ((πΉ βΎ π΅)βπ₯)) / (π§ β π₯))) = (π§ β ((π΄ β© π΅) β {π₯}) β¦ ((((πΉ βΎ π΅)βπ§) β ((πΉ βΎ π΅)βπ₯)) / (π§ β π₯))) |
79 | 41, 4 | sstrd 3992 |
. . 3
β’ (π β π΅ β β) |
80 | | fresin 6760 |
. . . 4
β’ (πΉ:π΄βΆβ β (πΉ βΎ π΅):(π΄ β© π΅)βΆβ) |
81 | 34, 80 | syl 17 |
. . 3
β’ (π β (πΉ βΎ π΅):(π΄ β© π΅)βΆβ) |
82 | 77, 2, 78, 79, 81, 44 | eldv 25414 |
. 2
β’ (π β (π₯(π΅ D (πΉ βΎ π΅))π¦ β (π₯ β ((intβ(πΎ βΎt π΅))β(π΄ β© π΅)) β§ π¦ β ((π§ β ((π΄ β© π΅) β {π₯}) β¦ ((((πΉ βΎ π΅)βπ§) β ((πΉ βΎ π΅)βπ₯)) / (π§ β π₯))) limβ π₯)))) |
83 | 56, 76, 82 | mpbir2and 711 |
1
β’ (π β π₯(π΅ D (πΉ βΎ π΅))π¦) |