Step | Hyp | Ref
| Expression |
1 | | c1lip2.a |
. 2
β’ (π β π΄ β β) |
2 | | c1lip2.b |
. 2
β’ (π β π΅ β β) |
3 | | c1lip2.f |
. . 3
β’ (π β πΉ β
((πCπββ)β1)) |
4 | | ax-resscn 11113 |
. . . . 5
β’ β
β β |
5 | | 1nn0 12434 |
. . . . 5
β’ 1 β
β0 |
6 | | elcpn 25314 |
. . . . 5
β’ ((β
β β β§ 1 β β0) β (πΉ β
((πCπββ)β1) β (πΉ β (β
βpm β) β§ ((β Dπ πΉ)β1) β (dom πΉβcnββ)))) |
7 | 4, 5, 6 | mp2an 691 |
. . . 4
β’ (πΉ β
((πCπββ)β1) β (πΉ β (β
βpm β) β§ ((β Dπ πΉ)β1) β (dom πΉβcnββ))) |
8 | 7 | simplbi 499 |
. . 3
β’ (πΉ β
((πCπββ)β1) β πΉ β (β
βpm β)) |
9 | 3, 8 | syl 17 |
. 2
β’ (π β πΉ β (β βpm
β)) |
10 | | c1lip2.dm |
. . 3
β’ (π β (π΄[,]π΅) β dom πΉ) |
11 | | pmfun 8788 |
. . . . . . . . 9
β’ (πΉ β (β
βpm β) β Fun πΉ) |
12 | 9, 11 | syl 17 |
. . . . . . . 8
β’ (π β Fun πΉ) |
13 | 12 | funfnd 6533 |
. . . . . . 7
β’ (π β πΉ Fn dom πΉ) |
14 | | c1lip2.rn |
. . . . . . 7
β’ (π β ran πΉ β β) |
15 | | df-f 6501 |
. . . . . . 7
β’ (πΉ:dom πΉβΆβ β (πΉ Fn dom πΉ β§ ran πΉ β β)) |
16 | 13, 14, 15 | sylanbrc 584 |
. . . . . 6
β’ (π β πΉ:dom πΉβΆβ) |
17 | | cnex 11137 |
. . . . . . . . 9
β’ β
β V |
18 | | reex 11147 |
. . . . . . . . 9
β’ β
β V |
19 | 17, 18 | elpm2 8815 |
. . . . . . . 8
β’ (πΉ β (β
βpm β) β (πΉ:dom πΉβΆβ β§ dom πΉ β β)) |
20 | 19 | simprbi 498 |
. . . . . . 7
β’ (πΉ β (β
βpm β) β dom πΉ β β) |
21 | 9, 20 | syl 17 |
. . . . . 6
β’ (π β dom πΉ β β) |
22 | | dvfre 25331 |
. . . . . 6
β’ ((πΉ:dom πΉβΆβ β§ dom πΉ β β) β (β D πΉ):dom (β D πΉ)βΆβ) |
23 | 16, 21, 22 | syl2anc 585 |
. . . . 5
β’ (π β (β D πΉ):dom (β D πΉ)βΆβ) |
24 | | 0p1e1 12280 |
. . . . . . . . . . 11
β’ (0 + 1) =
1 |
25 | 24 | fveq2i 6846 |
. . . . . . . . . 10
β’ ((β
Dπ πΉ)β(0 + 1)) = ((β
Dπ πΉ)β1) |
26 | | 0nn0 12433 |
. . . . . . . . . . . 12
β’ 0 β
β0 |
27 | | dvnp1 25305 |
. . . . . . . . . . . 12
β’ ((β
β β β§ πΉ
β (β βpm β) β§ 0 β
β0) β ((β Dπ πΉ)β(0 + 1)) = (β D ((β
Dπ πΉ)β0))) |
28 | 4, 26, 27 | mp3an13 1453 |
. . . . . . . . . . 11
β’ (πΉ β (β
βpm β) β ((β Dπ πΉ)β(0 + 1)) = (β D
((β Dπ πΉ)β0))) |
29 | 9, 28 | syl 17 |
. . . . . . . . . 10
β’ (π β ((β
Dπ πΉ)β(0 + 1)) = (β D ((β
Dπ πΉ)β0))) |
30 | 25, 29 | eqtr3id 2787 |
. . . . . . . . 9
β’ (π β ((β
Dπ πΉ)β1) = (β D ((β
Dπ πΉ)β0))) |
31 | | dvn0 25304 |
. . . . . . . . . . 11
β’ ((β
β β β§ πΉ
β (β βpm β)) β ((β
Dπ πΉ)β0) = πΉ) |
32 | 4, 9, 31 | sylancr 588 |
. . . . . . . . . 10
β’ (π β ((β
Dπ πΉ)β0) = πΉ) |
33 | 32 | oveq2d 7374 |
. . . . . . . . 9
β’ (π β (β D ((β
Dπ πΉ)β0)) = (β D πΉ)) |
34 | 30, 33 | eqtrd 2773 |
. . . . . . . 8
β’ (π β ((β
Dπ πΉ)β1) = (β D πΉ)) |
35 | 7 | simprbi 498 |
. . . . . . . . 9
β’ (πΉ β
((πCπββ)β1) β ((β
Dπ πΉ)β1) β (dom πΉβcnββ)) |
36 | 3, 35 | syl 17 |
. . . . . . . 8
β’ (π β ((β
Dπ πΉ)β1) β (dom πΉβcnββ)) |
37 | 34, 36 | eqeltrrd 2835 |
. . . . . . 7
β’ (π β (β D πΉ) β (dom πΉβcnββ)) |
38 | | cncff 24272 |
. . . . . . 7
β’ ((β
D πΉ) β (dom πΉβcnββ) β (β D πΉ):dom πΉβΆβ) |
39 | | fdm 6678 |
. . . . . . 7
β’ ((β
D πΉ):dom πΉβΆβ β dom (β D πΉ) = dom πΉ) |
40 | 37, 38, 39 | 3syl 18 |
. . . . . 6
β’ (π β dom (β D πΉ) = dom πΉ) |
41 | 40 | feq2d 6655 |
. . . . 5
β’ (π β ((β D πΉ):dom (β D πΉ)βΆβ β (β
D πΉ):dom πΉβΆβ)) |
42 | 23, 41 | mpbid 231 |
. . . 4
β’ (π β (β D πΉ):dom πΉβΆβ) |
43 | | cncfcdm 24277 |
. . . . 5
β’ ((β
β β β§ (β D πΉ) β (dom πΉβcnββ)) β ((β D πΉ) β (dom πΉβcnββ) β (β D πΉ):dom πΉβΆβ)) |
44 | 4, 37, 43 | sylancr 588 |
. . . 4
β’ (π β ((β D πΉ) β (dom πΉβcnββ) β (β D πΉ):dom πΉβΆβ)) |
45 | 42, 44 | mpbird 257 |
. . 3
β’ (π β (β D πΉ) β (dom πΉβcnββ)) |
46 | | rescncf 24276 |
. . 3
β’ ((π΄[,]π΅) β dom πΉ β ((β D πΉ) β (dom πΉβcnββ) β ((β D πΉ) βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ))) |
47 | 10, 45, 46 | sylc 65 |
. 2
β’ (π β ((β D πΉ) βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) |
48 | 18 | prid1 4724 |
. . . . . . . . 9
β’ β
β {β, β} |
49 | | 1eluzge0 12822 |
. . . . . . . . 9
β’ 1 β
(β€β₯β0) |
50 | | cpnord 25315 |
. . . . . . . . 9
β’ ((β
β {β, β} β§ 0 β β0 β§ 1 β
(β€β₯β0)) β
((πCπββ)β1) β
((πCπββ)β0)) |
51 | 48, 26, 49, 50 | mp3an 1462 |
. . . . . . . 8
β’
((πCπββ)β1) β
((πCπββ)β0) |
52 | 51, 3 | sselid 3943 |
. . . . . . 7
β’ (π β πΉ β
((πCπββ)β0)) |
53 | | elcpn 25314 |
. . . . . . . . 9
β’ ((β
β β β§ 0 β β0) β (πΉ β
((πCπββ)β0) β (πΉ β (β
βpm β) β§ ((β Dπ πΉ)β0) β (dom πΉβcnββ)))) |
54 | 4, 26, 53 | mp2an 691 |
. . . . . . . 8
β’ (πΉ β
((πCπββ)β0) β (πΉ β (β
βpm β) β§ ((β Dπ πΉ)β0) β (dom πΉβcnββ))) |
55 | 54 | simprbi 498 |
. . . . . . 7
β’ (πΉ β
((πCπββ)β0) β ((β
Dπ πΉ)β0) β (dom πΉβcnββ)) |
56 | 52, 55 | syl 17 |
. . . . . 6
β’ (π β ((β
Dπ πΉ)β0) β (dom πΉβcnββ)) |
57 | 32, 56 | eqeltrrd 2835 |
. . . . 5
β’ (π β πΉ β (dom πΉβcnββ)) |
58 | | cncfcdm 24277 |
. . . . 5
β’ ((β
β β β§ πΉ
β (dom πΉβcnββ)) β (πΉ β (dom πΉβcnββ) β πΉ:dom πΉβΆβ)) |
59 | 4, 57, 58 | sylancr 588 |
. . . 4
β’ (π β (πΉ β (dom πΉβcnββ) β πΉ:dom πΉβΆβ)) |
60 | 16, 59 | mpbird 257 |
. . 3
β’ (π β πΉ β (dom πΉβcnββ)) |
61 | | rescncf 24276 |
. . 3
β’ ((π΄[,]π΅) β dom πΉ β (πΉ β (dom πΉβcnββ) β (πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ))) |
62 | 10, 60, 61 | sylc 65 |
. 2
β’ (π β (πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) |
63 | 1, 2, 9, 47, 62 | c1lip1 25377 |
1
β’ (π β βπ β β βπ₯ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(absβ((πΉβπ¦) β (πΉβπ₯))) β€ (π Β· (absβ(π¦ β π₯)))) |