Step | Hyp | Ref
| Expression |
1 | | ulmclm.u |
. 2
β’ (π β πΉ(βπ’βπ)πΊ) |
2 | | ulmclm.a |
. . . . . . 7
β’ (π β π΄ β π) |
3 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π§ = π΄ β ((πΉβπ)βπ§) = ((πΉβπ)βπ΄)) |
4 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π§ = π΄ β (πΊβπ§) = (πΊβπ΄)) |
5 | 3, 4 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π§ = π΄ β (((πΉβπ)βπ§) β (πΊβπ§)) = (((πΉβπ)βπ΄) β (πΊβπ΄))) |
6 | 5 | fveq2d 6851 |
. . . . . . . . 9
β’ (π§ = π΄ β (absβ(((πΉβπ)βπ§) β (πΊβπ§))) = (absβ(((πΉβπ)βπ΄) β (πΊβπ΄)))) |
7 | 6 | breq1d 5120 |
. . . . . . . 8
β’ (π§ = π΄ β ((absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β (absβ(((πΉβπ)βπ΄) β (πΊβπ΄))) < π₯)) |
8 | 7 | rspcv 3580 |
. . . . . . 7
β’ (π΄ β π β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β (absβ(((πΉβπ)βπ΄) β (πΊβπ΄))) < π₯)) |
9 | 2, 8 | syl 17 |
. . . . . 6
β’ (π β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β (absβ(((πΉβπ)βπ΄) β (πΊβπ΄))) < π₯)) |
10 | 9 | ralimdv 3167 |
. . . . 5
β’ (π β (βπ β
(β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ΄) β (πΊβπ΄))) < π₯)) |
11 | 10 | reximdv 3168 |
. . . 4
β’ (π β (βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β βπ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ΄) β (πΊβπ΄))) < π₯)) |
12 | 11 | ralimdv 3167 |
. . 3
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ΄) β (πΊβπ΄))) < π₯)) |
13 | | ulmclm.z |
. . . 4
β’ π =
(β€β₯βπ) |
14 | | ulmclm.m |
. . . 4
β’ (π β π β β€) |
15 | | ulmclm.f |
. . . 4
β’ (π β πΉ:πβΆ(β βm π)) |
16 | | eqidd 2738 |
. . . 4
β’ ((π β§ (π β π β§ π§ β π)) β ((πΉβπ)βπ§) = ((πΉβπ)βπ§)) |
17 | | eqidd 2738 |
. . . 4
β’ ((π β§ π§ β π) β (πΊβπ§) = (πΊβπ§)) |
18 | | ulmcl 25756 |
. . . . 5
β’ (πΉ(βπ’βπ)πΊ β πΊ:πβΆβ) |
19 | 1, 18 | syl 17 |
. . . 4
β’ (π β πΊ:πβΆβ) |
20 | | ulmscl 25754 |
. . . . 5
β’ (πΉ(βπ’βπ)πΊ β π β V) |
21 | 1, 20 | syl 17 |
. . . 4
β’ (π β π β V) |
22 | 13, 14, 15, 16, 17, 19, 21 | ulm2 25760 |
. . 3
β’ (π β (πΉ(βπ’βπ)πΊ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯)) |
23 | | ulmclm.h |
. . . 4
β’ (π β π» β π) |
24 | | ulmclm.e |
. . . . 5
β’ ((π β§ π β π) β ((πΉβπ)βπ΄) = (π»βπ)) |
25 | 24 | eqcomd 2743 |
. . . 4
β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ)βπ΄)) |
26 | 19, 2 | ffvelcdmd 7041 |
. . . 4
β’ (π β (πΊβπ΄) β β) |
27 | 15 | ffvelcdmda 7040 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β (β βm π)) |
28 | | elmapi 8794 |
. . . . . 6
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
29 | 27, 28 | syl 17 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ):πβΆβ) |
30 | 2 | adantr 482 |
. . . . 5
β’ ((π β§ π β π) β π΄ β π) |
31 | 29, 30 | ffvelcdmd 7041 |
. . . 4
β’ ((π β§ π β π) β ((πΉβπ)βπ΄) β β) |
32 | 13, 14, 23, 25, 26, 31 | clim2c 15394 |
. . 3
β’ (π β (π» β (πΊβπ΄) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ΄) β (πΊβπ΄))) < π₯)) |
33 | 12, 22, 32 | 3imtr4d 294 |
. 2
β’ (π β (πΉ(βπ’βπ)πΊ β π» β (πΊβπ΄))) |
34 | 1, 33 | mpd 15 |
1
β’ (π β π» β (πΊβπ΄)) |