Step | Hyp | Ref
| Expression |
1 | | ax-resscn 11116 |
. . . . 5
β’ β
β β |
2 | 1 | a1i 11 |
. . . 4
β’ (π β β β
β) |
3 | | dvcj.f |
. . . 4
β’ (π β πΉ:πβΆβ) |
4 | | dvcj.x |
. . . 4
β’ (π β π β β) |
5 | | eqid 2733 |
. . . . 5
β’
(TopOpenββfld) =
(TopOpenββfld) |
6 | 5 | tgioo2 24189 |
. . . 4
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
7 | 2, 3, 4, 6, 5 | dvbssntr 25287 |
. . 3
β’ (π β dom (β D πΉ) β
((intβ(topGenβran (,)))βπ)) |
8 | | dvcj.c |
. . 3
β’ (π β πΆ β dom (β D πΉ)) |
9 | 7, 8 | sseldd 3949 |
. 2
β’ (π β πΆ β ((intβ(topGenβran
(,)))βπ)) |
10 | 4, 1 | sstrdi 3960 |
. . . . . 6
β’ (π β π β β) |
11 | 1 | a1i 11 |
. . . . . . . . 9
β’ ((πΉ:πβΆβ β§ π β β) β β β
β) |
12 | | simpl 484 |
. . . . . . . . 9
β’ ((πΉ:πβΆβ β§ π β β) β πΉ:πβΆβ) |
13 | | simpr 486 |
. . . . . . . . 9
β’ ((πΉ:πβΆβ β§ π β β) β π β β) |
14 | 11, 12, 13 | dvbss 25288 |
. . . . . . . 8
β’ ((πΉ:πβΆβ β§ π β β) β dom (β D
πΉ) β π) |
15 | 3, 4, 14 | syl2anc 585 |
. . . . . . 7
β’ (π β dom (β D πΉ) β π) |
16 | 15, 8 | sseldd 3949 |
. . . . . 6
β’ (π β πΆ β π) |
17 | 3, 10, 16 | dvlem 25283 |
. . . . 5
β’ ((π β§ π₯ β (π β {πΆ})) β (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ)) β β) |
18 | 17 | fmpttd 7067 |
. . . 4
β’ (π β (π₯ β (π β {πΆ}) β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))):(π β {πΆ})βΆβ) |
19 | | ssidd 3971 |
. . . 4
β’ (π β β β
β) |
20 | 5 | cnfldtopon 24169 |
. . . . 5
β’
(TopOpenββfld) β
(TopOnββ) |
21 | 20 | toponrestid 22293 |
. . . 4
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
22 | | dvf 25294 |
. . . . . . . 8
β’ (β
D πΉ):dom (β D πΉ)βΆβ |
23 | | ffun 6675 |
. . . . . . . 8
β’ ((β
D πΉ):dom (β D πΉ)βΆβ β Fun
(β D πΉ)) |
24 | | funfvbrb 7005 |
. . . . . . . 8
β’ (Fun
(β D πΉ) β (πΆ β dom (β D πΉ) β πΆ(β D πΉ)((β D πΉ)βπΆ))) |
25 | 22, 23, 24 | mp2b 10 |
. . . . . . 7
β’ (πΆ β dom (β D πΉ) β πΆ(β D πΉ)((β D πΉ)βπΆ)) |
26 | 8, 25 | sylib 217 |
. . . . . 6
β’ (π β πΆ(β D πΉ)((β D πΉ)βπΆ)) |
27 | | eqid 2733 |
. . . . . . 7
β’ (π₯ β (π β {πΆ}) β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))) = (π₯ β (π β {πΆ}) β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))) |
28 | 6, 5, 27, 2, 3, 4 | eldv 25285 |
. . . . . 6
β’ (π β (πΆ(β D πΉ)((β D πΉ)βπΆ) β (πΆ β ((intβ(topGenβran
(,)))βπ) β§
((β D πΉ)βπΆ) β ((π₯ β (π β {πΆ}) β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))) limβ πΆ)))) |
29 | 26, 28 | mpbid 231 |
. . . . 5
β’ (π β (πΆ β ((intβ(topGenβran
(,)))βπ) β§
((β D πΉ)βπΆ) β ((π₯ β (π β {πΆ}) β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))) limβ πΆ))) |
30 | 29 | simprd 497 |
. . . 4
β’ (π β ((β D πΉ)βπΆ) β ((π₯ β (π β {πΆ}) β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))) limβ πΆ)) |
31 | | cjcncf 24290 |
. . . . . 6
β’ β
β (ββcnββ) |
32 | 5 | cncfcn1 24297 |
. . . . . 6
β’
(ββcnββ) =
((TopOpenββfld) Cn
(TopOpenββfld)) |
33 | 31, 32 | eleqtri 2832 |
. . . . 5
β’ β
β ((TopOpenββfld) Cn
(TopOpenββfld)) |
34 | 22 | ffvelcdmi 7038 |
. . . . . 6
β’ (πΆ β dom (β D πΉ) β ((β D πΉ)βπΆ) β β) |
35 | 8, 34 | syl 17 |
. . . . 5
β’ (π β ((β D πΉ)βπΆ) β β) |
36 | | unicntop 24172 |
. . . . . 6
β’ β =
βͺ
(TopOpenββfld) |
37 | 36 | cncnpi 22652 |
. . . . 5
β’
((β β ((TopOpenββfld) Cn
(TopOpenββfld)) β§ ((β D πΉ)βπΆ) β β) β β β
(((TopOpenββfld) CnP
(TopOpenββfld))β((β D πΉ)βπΆ))) |
38 | 33, 35, 37 | sylancr 588 |
. . . 4
β’ (π β β β
(((TopOpenββfld) CnP
(TopOpenββfld))β((β D πΉ)βπΆ))) |
39 | 18, 19, 5, 21, 30, 38 | limccnp 25278 |
. . 3
β’ (π β (ββ((β
D πΉ)βπΆ)) β ((β β
(π₯ β (π β {πΆ}) β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ)))) limβ πΆ)) |
40 | | cjf 14998 |
. . . . . . 7
β’
β:ββΆβ |
41 | 40 | a1i 11 |
. . . . . 6
β’ (π β
β:ββΆβ) |
42 | 41, 17 | cofmpt 7082 |
. . . . 5
β’ (π β (β β (π₯ β (π β {πΆ}) β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ)))) = (π₯ β (π β {πΆ}) β¦ (ββ(((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))))) |
43 | 3 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π β {πΆ})) β πΉ:πβΆβ) |
44 | | eldifi 4090 |
. . . . . . . . . . 11
β’ (π₯ β (π β {πΆ}) β π₯ β π) |
45 | 44 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π β {πΆ})) β π₯ β π) |
46 | 43, 45 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π β {πΆ})) β (πΉβπ₯) β β) |
47 | 3, 16 | ffvelcdmd 7040 |
. . . . . . . . . 10
β’ (π β (πΉβπΆ) β β) |
48 | 47 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π β {πΆ})) β (πΉβπΆ) β β) |
49 | 46, 48 | subcld 11520 |
. . . . . . . 8
β’ ((π β§ π₯ β (π β {πΆ})) β ((πΉβπ₯) β (πΉβπΆ)) β β) |
50 | 4 | sselda 3948 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β π₯ β β) |
51 | 44, 50 | sylan2 594 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π β {πΆ})) β π₯ β β) |
52 | 4, 16 | sseldd 3949 |
. . . . . . . . . . 11
β’ (π β πΆ β β) |
53 | 52 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π β {πΆ})) β πΆ β β) |
54 | 51, 53 | resubcld 11591 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π β {πΆ})) β (π₯ β πΆ) β β) |
55 | 54 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π₯ β (π β {πΆ})) β (π₯ β πΆ) β β) |
56 | 51 | recnd 11191 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π β {πΆ})) β π₯ β β) |
57 | 53 | recnd 11191 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π β {πΆ})) β πΆ β β) |
58 | | eldifsni 4754 |
. . . . . . . . . 10
β’ (π₯ β (π β {πΆ}) β π₯ β πΆ) |
59 | 58 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π β {πΆ})) β π₯ β πΆ) |
60 | 56, 57, 59 | subne0d 11529 |
. . . . . . . 8
β’ ((π β§ π₯ β (π β {πΆ})) β (π₯ β πΆ) β 0) |
61 | 49, 55, 60 | cjdivd 15117 |
. . . . . . 7
β’ ((π β§ π₯ β (π β {πΆ})) β (ββ(((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))) = ((ββ((πΉβπ₯) β (πΉβπΆ))) / (ββ(π₯ β πΆ)))) |
62 | | cjsub 15043 |
. . . . . . . . . 10
β’ (((πΉβπ₯) β β β§ (πΉβπΆ) β β) β
(ββ((πΉβπ₯) β (πΉβπΆ))) = ((ββ(πΉβπ₯)) β (ββ(πΉβπΆ)))) |
63 | 46, 48, 62 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π β {πΆ})) β (ββ((πΉβπ₯) β (πΉβπΆ))) = ((ββ(πΉβπ₯)) β (ββ(πΉβπΆ)))) |
64 | | fvco3 6944 |
. . . . . . . . . . 11
β’ ((πΉ:πβΆβ β§ π₯ β π) β ((β β πΉ)βπ₯) = (ββ(πΉβπ₯))) |
65 | 3, 44, 64 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π β {πΆ})) β ((β β πΉ)βπ₯) = (ββ(πΉβπ₯))) |
66 | | fvco3 6944 |
. . . . . . . . . . . 12
β’ ((πΉ:πβΆβ β§ πΆ β π) β ((β β πΉ)βπΆ) = (ββ(πΉβπΆ))) |
67 | 3, 16, 66 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β ((β β πΉ)βπΆ) = (ββ(πΉβπΆ))) |
68 | 67 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π β {πΆ})) β ((β β πΉ)βπΆ) = (ββ(πΉβπΆ))) |
69 | 65, 68 | oveq12d 7379 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π β {πΆ})) β (((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) = ((ββ(πΉβπ₯)) β (ββ(πΉβπΆ)))) |
70 | 63, 69 | eqtr4d 2776 |
. . . . . . . 8
β’ ((π β§ π₯ β (π β {πΆ})) β (ββ((πΉβπ₯) β (πΉβπΆ))) = (((β β πΉ)βπ₯) β ((β β πΉ)βπΆ))) |
71 | 54 | cjred 15120 |
. . . . . . . 8
β’ ((π β§ π₯ β (π β {πΆ})) β (ββ(π₯ β πΆ)) = (π₯ β πΆ)) |
72 | 70, 71 | oveq12d 7379 |
. . . . . . 7
β’ ((π β§ π₯ β (π β {πΆ})) β ((ββ((πΉβπ₯) β (πΉβπΆ))) / (ββ(π₯ β πΆ))) = ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ))) |
73 | 61, 72 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π₯ β (π β {πΆ})) β (ββ(((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))) = ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ))) |
74 | 73 | mpteq2dva 5209 |
. . . . 5
β’ (π β (π₯ β (π β {πΆ}) β¦ (ββ(((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ)))) = (π₯ β (π β {πΆ}) β¦ ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ)))) |
75 | 42, 74 | eqtrd 2773 |
. . . 4
β’ (π β (β β (π₯ β (π β {πΆ}) β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ)))) = (π₯ β (π β {πΆ}) β¦ ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ)))) |
76 | 75 | oveq1d 7376 |
. . 3
β’ (π β ((β β (π₯ β (π β {πΆ}) β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ)))) limβ πΆ) = ((π₯ β (π β {πΆ}) β¦ ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ))) limβ πΆ)) |
77 | 39, 76 | eleqtrd 2836 |
. 2
β’ (π β (ββ((β
D πΉ)βπΆ)) β ((π₯ β (π β {πΆ}) β¦ ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ))) limβ πΆ)) |
78 | | eqid 2733 |
. . 3
β’ (π₯ β (π β {πΆ}) β¦ ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ))) = (π₯ β (π β {πΆ}) β¦ ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ))) |
79 | | fco 6696 |
. . . 4
β’
((β:ββΆβ β§ πΉ:πβΆβ) β (β β
πΉ):πβΆβ) |
80 | 40, 3, 79 | sylancr 588 |
. . 3
β’ (π β (β β πΉ):πβΆβ) |
81 | 6, 5, 78, 2, 80, 4 | eldv 25285 |
. 2
β’ (π β (πΆ(β D (β β πΉ))(ββ((β D
πΉ)βπΆ)) β (πΆ β ((intβ(topGenβran
(,)))βπ) β§
(ββ((β D πΉ)βπΆ)) β ((π₯ β (π β {πΆ}) β¦ ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ))) limβ πΆ)))) |
82 | 9, 77, 81 | mpbir2and 712 |
1
β’ (π β πΆ(β D (β β πΉ))(ββ((β D
πΉ)βπΆ))) |