Step | Hyp | Ref
| Expression |
1 | | dvco.bg |
. . . 4
β’ (π β πΆ(π D πΊ)πΏ) |
2 | | eqid 2177 |
. . . . 5
β’ (π½ βΎt π) = (π½ βΎt π) |
3 | | dvcoap.j |
. . . . 5
β’ π½ = (MetOpenβ(abs β
β )) |
4 | | eqid 2177 |
. . . . 5
β’ (π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) = (π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) |
5 | | dvcobr.t |
. . . . 5
β’ (π β π β β) |
6 | | dvco.g |
. . . . . 6
β’ (π β πΊ:πβΆπ) |
7 | | dvco.x |
. . . . . . 7
β’ (π β π β π) |
8 | | dvcobr.s |
. . . . . . 7
β’ (π β π β β) |
9 | 7, 8 | sstrd 3165 |
. . . . . 6
β’ (π β π β β) |
10 | 6, 9 | fssd 5378 |
. . . . 5
β’ (π β πΊ:πβΆβ) |
11 | | dvco.y |
. . . . 5
β’ (π β π β π) |
12 | 2, 3, 4, 5, 10, 11 | eldvap 14087 |
. . . 4
β’ (π β (πΆ(π D πΊ)πΏ β (πΆ β ((intβ(π½ βΎt π))βπ) β§ πΏ β ((π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) limβ πΆ)))) |
13 | 1, 12 | mpbid 147 |
. . 3
β’ (π β (πΆ β ((intβ(π½ βΎt π))βπ) β§ πΏ β ((π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) limβ πΆ))) |
14 | 13 | simpld 112 |
. 2
β’ (π β πΆ β ((intβ(π½ βΎt π))βπ)) |
15 | | dvco.f |
. . . . . . . 8
β’ (π β πΉ:πβΆβ) |
16 | 15 | adantr 276 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β πΉ:πβΆβ) |
17 | 6 | adantr 276 |
. . . . . . . 8
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β πΊ:πβΆπ) |
18 | | elrabi 2890 |
. . . . . . . . 9
β’ (π§ β {π€ β π β£ π€ # πΆ} β π§ β π) |
19 | 18 | adantl 277 |
. . . . . . . 8
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β π§ β π) |
20 | 17, 19 | ffvelcdmd 5652 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΊβπ§) β π) |
21 | 16, 20 | ffvelcdmd 5652 |
. . . . . 6
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΉβ(πΊβπ§)) β β) |
22 | 5, 10, 11 | dvbss 14090 |
. . . . . . . . . 10
β’ (π β dom (π D πΊ) β π) |
23 | | cnex 7934 |
. . . . . . . . . . . . . 14
β’ β
β V |
24 | 23 | a1i 9 |
. . . . . . . . . . . . 13
β’ (π β β β
V) |
25 | 24, 5 | ssexd 4143 |
. . . . . . . . . . . . 13
β’ (π β π β V) |
26 | | elpm2r 6665 |
. . . . . . . . . . . . 13
β’
(((β β V β§ π β V) β§ (πΊ:πβΆβ β§ π β π)) β πΊ β (β βpm
π)) |
27 | 24, 25, 10, 11, 26 | syl22anc 1239 |
. . . . . . . . . . . 12
β’ (π β πΊ β (β βpm
π)) |
28 | | reldvg 14084 |
. . . . . . . . . . . 12
β’ ((π β β β§ πΊ β (β
βpm π)) β Rel (π D πΊ)) |
29 | 5, 27, 28 | syl2anc 411 |
. . . . . . . . . . 11
β’ (π β Rel (π D πΊ)) |
30 | | releldm 4862 |
. . . . . . . . . . 11
β’ ((Rel
(π D πΊ) β§ πΆ(π D πΊ)πΏ) β πΆ β dom (π D πΊ)) |
31 | 29, 1, 30 | syl2anc 411 |
. . . . . . . . . 10
β’ (π β πΆ β dom (π D πΊ)) |
32 | 22, 31 | sseldd 3156 |
. . . . . . . . 9
β’ (π β πΆ β π) |
33 | 32 | adantr 276 |
. . . . . . . 8
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β πΆ β π) |
34 | 17, 33 | ffvelcdmd 5652 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΊβπΆ) β π) |
35 | 16, 34 | ffvelcdmd 5652 |
. . . . . 6
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΉβ(πΊβπΆ)) β β) |
36 | 21, 35 | subcld 8267 |
. . . . 5
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((πΉβ(πΊβπ§)) β (πΉβ(πΊβπΆ))) β β) |
37 | 10 | adantr 276 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β πΊ:πβΆβ) |
38 | 37, 19 | ffvelcdmd 5652 |
. . . . . 6
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΊβπ§) β β) |
39 | 37, 33 | ffvelcdmd 5652 |
. . . . . 6
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΊβπΆ) β β) |
40 | 38, 39 | subcld 8267 |
. . . . 5
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((πΊβπ§) β (πΊβπΆ)) β β) |
41 | 9 | adantr 276 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β π β β) |
42 | 41, 20 | sseldd 3156 |
. . . . . 6
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΊβπ§) β β) |
43 | 41, 34 | sseldd 3156 |
. . . . . 6
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΊβπΆ) β β) |
44 | | breq1 4006 |
. . . . . . . . . 10
β’ (π€ = π§ β (π€ # πΆ β π§ # πΆ)) |
45 | 44 | elrab 2893 |
. . . . . . . . 9
β’ (π§ β {π€ β π β£ π€ # πΆ} β (π§ β π β§ π§ # πΆ)) |
46 | 45 | simprbi 275 |
. . . . . . . 8
β’ (π§ β {π€ β π β£ π€ # πΆ} β π§ # πΆ) |
47 | 46 | adantl 277 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β π§ # πΆ) |
48 | | breq1 4006 |
. . . . . . . . 9
β’ (π’ = π§ β (π’ # πΆ β π§ # πΆ)) |
49 | | fveq2 5515 |
. . . . . . . . . 10
β’ (π’ = π§ β (πΊβπ’) = (πΊβπ§)) |
50 | 49 | breq1d 4013 |
. . . . . . . . 9
β’ (π’ = π§ β ((πΊβπ’) # (πΊβπΆ) β (πΊβπ§) # (πΊβπΆ))) |
51 | 48, 50 | imbi12d 234 |
. . . . . . . 8
β’ (π’ = π§ β ((π’ # πΆ β (πΊβπ’) # (πΊβπΆ)) β (π§ # πΆ β (πΊβπ§) # (πΊβπΆ)))) |
52 | | dvcoap.gap |
. . . . . . . . 9
β’ (π β βπ’ β π (π’ # πΆ β (πΊβπ’) # (πΊβπΆ))) |
53 | 52 | adantr 276 |
. . . . . . . 8
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β βπ’ β π (π’ # πΆ β (πΊβπ’) # (πΊβπΆ))) |
54 | 51, 53, 19 | rspcdva 2846 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (π§ # πΆ β (πΊβπ§) # (πΊβπΆ))) |
55 | 47, 54 | mpd 13 |
. . . . . 6
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΊβπ§) # (πΊβπΆ)) |
56 | 42, 43, 55 | subap0d 8600 |
. . . . 5
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((πΊβπ§) β (πΊβπΆ)) # 0) |
57 | 36, 40, 56 | divclapd 8746 |
. . . 4
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (((πΉβ(πΊβπ§)) β (πΉβ(πΊβπΆ))) / ((πΊβπ§) β (πΊβπΆ))) β β) |
58 | 11, 5 | sstrd 3165 |
. . . . 5
β’ (π β π β β) |
59 | 10, 58, 32 | dvlemap 14085 |
. . . 4
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ)) β β) |
60 | | ssidd 3176 |
. . . 4
β’ (π β β β
β) |
61 | 3 | cntoptopon 13968 |
. . . . . 6
β’ π½ β
(TopOnββ) |
62 | | txtopon 13698 |
. . . . . 6
β’ ((π½ β (TopOnββ)
β§ π½ β
(TopOnββ)) β (π½ Γt π½) β (TopOnβ(β Γ
β))) |
63 | 61, 61, 62 | mp2an 426 |
. . . . 5
β’ (π½ Γt π½) β (TopOnβ(β
Γ β)) |
64 | 63 | toponrestid 13457 |
. . . 4
β’ (π½ Γt π½) = ((π½ Γt π½) βΎt (β Γ
β)) |
65 | | breq1 4006 |
. . . . . 6
β’ (π€ = (πΊβπ§) β (π€ # (πΊβπΆ) β (πΊβπ§) # (πΊβπΆ))) |
66 | 65, 20, 55 | elrabd 2895 |
. . . . 5
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (πΊβπ§) β {π€ β π β£ π€ # (πΊβπΆ)}) |
67 | 15 | adantr 276 |
. . . . . . . 8
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β πΉ:πβΆβ) |
68 | | elrabi 2890 |
. . . . . . . . 9
β’ (π¦ β {π€ β π β£ π€ # (πΊβπΆ)} β π¦ β π) |
69 | 68 | adantl 277 |
. . . . . . . 8
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β π¦ β π) |
70 | 67, 69 | ffvelcdmd 5652 |
. . . . . . 7
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β (πΉβπ¦) β β) |
71 | 6 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β πΊ:πβΆπ) |
72 | 32 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β πΆ β π) |
73 | 71, 72 | ffvelcdmd 5652 |
. . . . . . . 8
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β (πΊβπΆ) β π) |
74 | 67, 73 | ffvelcdmd 5652 |
. . . . . . 7
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β (πΉβ(πΊβπΆ)) β β) |
75 | 70, 74 | subcld 8267 |
. . . . . 6
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β ((πΉβπ¦) β (πΉβ(πΊβπΆ))) β β) |
76 | 9 | adantr 276 |
. . . . . . . 8
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β π β β) |
77 | 76, 69 | sseldd 3156 |
. . . . . . 7
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β π¦ β β) |
78 | 76, 73 | sseldd 3156 |
. . . . . . 7
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β (πΊβπΆ) β β) |
79 | 77, 78 | subcld 8267 |
. . . . . 6
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β (π¦ β (πΊβπΆ)) β β) |
80 | | breq1 4006 |
. . . . . . . . . 10
β’ (π€ = π¦ β (π€ # (πΊβπΆ) β π¦ # (πΊβπΆ))) |
81 | 80 | elrab 2893 |
. . . . . . . . 9
β’ (π¦ β {π€ β π β£ π€ # (πΊβπΆ)} β (π¦ β π β§ π¦ # (πΊβπΆ))) |
82 | 81 | simprbi 275 |
. . . . . . . 8
β’ (π¦ β {π€ β π β£ π€ # (πΊβπΆ)} β π¦ # (πΊβπΆ)) |
83 | 82 | adantl 277 |
. . . . . . 7
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β π¦ # (πΊβπΆ)) |
84 | 77, 78, 83 | subap0d 8600 |
. . . . . 6
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β (π¦ β (πΊβπΆ)) # 0) |
85 | 75, 79, 84 | divclapd 8746 |
. . . . 5
β’ ((π β§ π¦ β {π€ β π β£ π€ # (πΊβπΆ)}) β (((πΉβπ¦) β (πΉβ(πΊβπΆ))) / (π¦ β (πΊβπΆ))) β β) |
86 | | limcresi 14071 |
. . . . . . 7
β’ (πΊ limβ πΆ) β ((πΊ βΎ {π€ β π β£ π€ # πΆ}) limβ πΆ) |
87 | 6 | feqmptd 5569 |
. . . . . . . . . 10
β’ (π β πΊ = (π§ β π β¦ (πΊβπ§))) |
88 | 87 | reseq1d 4906 |
. . . . . . . . 9
β’ (π β (πΊ βΎ {π€ β π β£ π€ # πΆ}) = ((π§ β π β¦ (πΊβπ§)) βΎ {π€ β π β£ π€ # πΆ})) |
89 | | ssrab2 3240 |
. . . . . . . . . 10
β’ {π€ β π β£ π€ # πΆ} β π |
90 | | resmpt 4955 |
. . . . . . . . . 10
β’ ({π€ β π β£ π€ # πΆ} β π β ((π§ β π β¦ (πΊβπ§)) βΎ {π€ β π β£ π€ # πΆ}) = (π§ β {π€ β π β£ π€ # πΆ} β¦ (πΊβπ§))) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . 9
β’ ((π§ β π β¦ (πΊβπ§)) βΎ {π€ β π β£ π€ # πΆ}) = (π§ β {π€ β π β£ π€ # πΆ} β¦ (πΊβπ§)) |
92 | 88, 91 | eqtrdi 2226 |
. . . . . . . 8
β’ (π β (πΊ βΎ {π€ β π β£ π€ # πΆ}) = (π§ β {π€ β π β£ π€ # πΆ} β¦ (πΊβπ§))) |
93 | 92 | oveq1d 5889 |
. . . . . . 7
β’ (π β ((πΊ βΎ {π€ β π β£ π€ # πΆ}) limβ πΆ) = ((π§ β {π€ β π β£ π€ # πΆ} β¦ (πΊβπ§)) limβ πΆ)) |
94 | 86, 93 | sseqtrid 3205 |
. . . . . 6
β’ (π β (πΊ limβ πΆ) β ((π§ β {π€ β π β£ π€ # πΆ} β¦ (πΊβπ§)) limβ πΆ)) |
95 | | eqid 2177 |
. . . . . . . . . 10
β’ (π½ βΎt π) = (π½ βΎt π) |
96 | 95, 3 | dvcnp2cntop 14099 |
. . . . . . . . 9
β’ (((π β β β§ πΊ:πβΆβ β§ π β π) β§ πΆ β dom (π D πΊ)) β πΊ β (((π½ βΎt π) CnP π½)βπΆ)) |
97 | 5, 10, 11, 31, 96 | syl31anc 1241 |
. . . . . . . 8
β’ (π β πΊ β (((π½ βΎt π) CnP π½)βπΆ)) |
98 | 3, 95 | cnplimccntop 14075 |
. . . . . . . . 9
β’ ((π β β β§ πΆ β π) β (πΊ β (((π½ βΎt π) CnP π½)βπΆ) β (πΊ:πβΆβ β§ (πΊβπΆ) β (πΊ limβ πΆ)))) |
99 | 58, 32, 98 | syl2anc 411 |
. . . . . . . 8
β’ (π β (πΊ β (((π½ βΎt π) CnP π½)βπΆ) β (πΊ:πβΆβ β§ (πΊβπΆ) β (πΊ limβ πΆ)))) |
100 | 97, 99 | mpbid 147 |
. . . . . . 7
β’ (π β (πΊ:πβΆβ β§ (πΊβπΆ) β (πΊ limβ πΆ))) |
101 | 100 | simprd 114 |
. . . . . 6
β’ (π β (πΊβπΆ) β (πΊ limβ πΆ)) |
102 | 94, 101 | sseldd 3156 |
. . . . 5
β’ (π β (πΊβπΆ) β ((π§ β {π€ β π β£ π€ # πΆ} β¦ (πΊβπ§)) limβ πΆ)) |
103 | | dvco.bf |
. . . . . . 7
β’ (π β (πΊβπΆ)(π D πΉ)πΎ) |
104 | | eqid 2177 |
. . . . . . . 8
β’ (π½ βΎt π) = (π½ βΎt π) |
105 | | eqid 2177 |
. . . . . . . 8
β’ (π¦ β {π€ β π β£ π€ # (πΊβπΆ)} β¦ (((πΉβπ¦) β (πΉβ(πΊβπΆ))) / (π¦ β (πΊβπΆ)))) = (π¦ β {π€ β π β£ π€ # (πΊβπΆ)} β¦ (((πΉβπ¦) β (πΉβ(πΊβπΆ))) / (π¦ β (πΊβπΆ)))) |
106 | 104, 3, 105, 8, 15, 7 | eldvap 14087 |
. . . . . . 7
β’ (π β ((πΊβπΆ)(π D πΉ)πΎ β ((πΊβπΆ) β ((intβ(π½ βΎt π))βπ) β§ πΎ β ((π¦ β {π€ β π β£ π€ # (πΊβπΆ)} β¦ (((πΉβπ¦) β (πΉβ(πΊβπΆ))) / (π¦ β (πΊβπΆ)))) limβ (πΊβπΆ))))) |
107 | 103, 106 | mpbid 147 |
. . . . . 6
β’ (π β ((πΊβπΆ) β ((intβ(π½ βΎt π))βπ) β§ πΎ β ((π¦ β {π€ β π β£ π€ # (πΊβπΆ)} β¦ (((πΉβπ¦) β (πΉβ(πΊβπΆ))) / (π¦ β (πΊβπΆ)))) limβ (πΊβπΆ)))) |
108 | 107 | simprd 114 |
. . . . 5
β’ (π β πΎ β ((π¦ β {π€ β π β£ π€ # (πΊβπΆ)} β¦ (((πΉβπ¦) β (πΉβ(πΊβπΆ))) / (π¦ β (πΊβπΆ)))) limβ (πΊβπΆ))) |
109 | | fveq2 5515 |
. . . . . . 7
β’ (π¦ = (πΊβπ§) β (πΉβπ¦) = (πΉβ(πΊβπ§))) |
110 | 109 | oveq1d 5889 |
. . . . . 6
β’ (π¦ = (πΊβπ§) β ((πΉβπ¦) β (πΉβ(πΊβπΆ))) = ((πΉβ(πΊβπ§)) β (πΉβ(πΊβπΆ)))) |
111 | | oveq1 5881 |
. . . . . 6
β’ (π¦ = (πΊβπ§) β (π¦ β (πΊβπΆ)) = ((πΊβπ§) β (πΊβπΆ))) |
112 | 110, 111 | oveq12d 5892 |
. . . . 5
β’ (π¦ = (πΊβπ§) β (((πΉβπ¦) β (πΉβ(πΊβπΆ))) / (π¦ β (πΊβπΆ))) = (((πΉβ(πΊβπ§)) β (πΉβ(πΊβπΆ))) / ((πΊβπ§) β (πΊβπΆ)))) |
113 | 66, 85, 102, 108, 112 | limccoap 14083 |
. . . 4
β’ (π β πΎ β ((π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβ(πΊβπ§)) β (πΉβ(πΊβπΆ))) / ((πΊβπ§) β (πΊβπΆ)))) limβ πΆ)) |
114 | 13 | simprd 114 |
. . . 4
β’ (π β πΏ β ((π§ β {π€ β π β£ π€ # πΆ} β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) limβ πΆ)) |
115 | 3 | mulcncntop 13990 |
. . . . 5
β’ Β·
β ((π½
Γt π½) Cn
π½) |
116 | 8, 15, 7 | dvcl 14088 |
. . . . . . 7
β’ ((π β§ (πΊβπΆ)(π D πΉ)πΎ) β πΎ β β) |
117 | 103, 116 | mpdan 421 |
. . . . . 6
β’ (π β πΎ β β) |
118 | 5, 10, 11 | dvcl 14088 |
. . . . . . 7
β’ ((π β§ πΆ(π D πΊ)πΏ) β πΏ β β) |
119 | 1, 118 | mpdan 421 |
. . . . . 6
β’ (π β πΏ β β) |
120 | 117, 119 | opelxpd 4659 |
. . . . 5
β’ (π β β¨πΎ, πΏβ© β (β Γ
β)) |
121 | 63 | toponunii 13453 |
. . . . . 6
β’ (β
Γ β) = βͺ (π½ Γt π½) |
122 | 121 | cncnpi 13664 |
. . . . 5
β’ ((
Β· β ((π½
Γt π½) Cn
π½) β§ β¨πΎ, πΏβ© β (β Γ β))
β Β· β (((π½
Γt π½) CnP
π½)ββ¨πΎ, πΏβ©)) |
123 | 115, 120,
122 | sylancr 414 |
. . . 4
β’ (π β Β· β (((π½ Γt π½) CnP π½)ββ¨πΎ, πΏβ©)) |
124 | 57, 59, 60, 60, 3, 64, 113, 114, 123 | limccnp2cntop 14082 |
. . 3
β’ (π β (πΎ Β· πΏ) β ((π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉβ(πΊβπ§)) β (πΉβ(πΊβπΆ))) / ((πΊβπ§) β (πΊβπΆ))) Β· (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ)))) limβ πΆ)) |
125 | 42, 43 | subcld 8267 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((πΊβπ§) β (πΊβπΆ)) β β) |
126 | 58 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β π β β) |
127 | 126, 19 | sseldd 3156 |
. . . . . . . 8
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β π§ β β) |
128 | 126, 33 | sseldd 3156 |
. . . . . . . 8
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β πΆ β β) |
129 | 127, 128 | subcld 8267 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (π§ β πΆ) β β) |
130 | 127, 128,
47 | subap0d 8600 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (π§ β πΆ) # 0) |
131 | 36, 125, 129, 56, 130 | dmdcanap2d 8777 |
. . . . . 6
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((((πΉβ(πΊβπ§)) β (πΉβ(πΊβπΆ))) / ((πΊβπ§) β (πΊβπΆ))) Β· (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) = (((πΉβ(πΊβπ§)) β (πΉβ(πΊβπΆ))) / (π§ β πΆ))) |
132 | | fvco3 5587 |
. . . . . . . . 9
β’ ((πΊ:πβΆπ β§ π§ β π) β ((πΉ β πΊ)βπ§) = (πΉβ(πΊβπ§))) |
133 | 17, 19, 132 | syl2anc 411 |
. . . . . . . 8
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((πΉ β πΊ)βπ§) = (πΉβ(πΊβπ§))) |
134 | | fvco3 5587 |
. . . . . . . . 9
β’ ((πΊ:πβΆπ β§ πΆ β π) β ((πΉ β πΊ)βπΆ) = (πΉβ(πΊβπΆ))) |
135 | 17, 33, 134 | syl2anc 411 |
. . . . . . . 8
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((πΉ β πΊ)βπΆ) = (πΉβ(πΊβπΆ))) |
136 | 133, 135 | oveq12d 5892 |
. . . . . . 7
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β (((πΉ β πΊ)βπ§) β ((πΉ β πΊ)βπΆ)) = ((πΉβ(πΊβπ§)) β (πΉβ(πΊβπΆ)))) |
137 | 136 | oveq1d 5889 |
. . . . . 6
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((((πΉ β πΊ)βπ§) β ((πΉ β πΊ)βπΆ)) / (π§ β πΆ)) = (((πΉβ(πΊβπ§)) β (πΉβ(πΊβπΆ))) / (π§ β πΆ))) |
138 | 131, 137 | eqtr4d 2213 |
. . . . 5
β’ ((π β§ π§ β {π€ β π β£ π€ # πΆ}) β ((((πΉβ(πΊβπ§)) β (πΉβ(πΊβπΆ))) / ((πΊβπ§) β (πΊβπΆ))) Β· (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) = ((((πΉ β πΊ)βπ§) β ((πΉ β πΊ)βπΆ)) / (π§ β πΆ))) |
139 | 138 | mpteq2dva 4093 |
. . . 4
β’ (π β (π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉβ(πΊβπ§)) β (πΉβ(πΊβπΆ))) / ((πΊβπ§) β (πΊβπΆ))) Β· (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ)))) = (π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉ β πΊ)βπ§) β ((πΉ β πΊ)βπΆ)) / (π§ β πΆ)))) |
140 | 139 | oveq1d 5889 |
. . 3
β’ (π β ((π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉβ(πΊβπ§)) β (πΉβ(πΊβπΆ))) / ((πΊβπ§) β (πΊβπΆ))) Β· (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ)))) limβ πΆ) = ((π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉ β πΊ)βπ§) β ((πΉ β πΊ)βπΆ)) / (π§ β πΆ))) limβ πΆ)) |
141 | 124, 140 | eleqtrd 2256 |
. 2
β’ (π β (πΎ Β· πΏ) β ((π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉ β πΊ)βπ§) β ((πΉ β πΊ)βπΆ)) / (π§ β πΆ))) limβ πΆ)) |
142 | | eqid 2177 |
. . 3
β’ (π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉ β πΊ)βπ§) β ((πΉ β πΊ)βπΆ)) / (π§ β πΆ))) = (π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉ β πΊ)βπ§) β ((πΉ β πΊ)βπΆ)) / (π§ β πΆ))) |
143 | | fco 5381 |
. . . 4
β’ ((πΉ:πβΆβ β§ πΊ:πβΆπ) β (πΉ β πΊ):πβΆβ) |
144 | 15, 6, 143 | syl2anc 411 |
. . 3
β’ (π β (πΉ β πΊ):πβΆβ) |
145 | 2, 3, 142, 5, 144, 11 | eldvap 14087 |
. 2
β’ (π β (πΆ(π D (πΉ β πΊ))(πΎ Β· πΏ) β (πΆ β ((intβ(π½ βΎt π))βπ) β§ (πΎ Β· πΏ) β ((π§ β {π€ β π β£ π€ # πΆ} β¦ ((((πΉ β πΊ)βπ§) β ((πΉ β πΊ)βπΆ)) / (π§ β πΆ))) limβ πΆ)))) |
146 | 14, 141, 145 | mpbir2and 944 |
1
β’ (π β πΆ(π D (πΉ β πΊ))(πΎ Β· πΏ)) |