Step | Hyp | Ref
| Expression |
1 | | iscau 24663 |
. 2
β’ (π· β (βMetβπ) β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πΉβπ)(ballβπ·)π₯)))) |
2 | | elfvdm 6883 |
. . . . . . . . . 10
β’ (π· β (βMetβπ) β π β dom βMet) |
3 | | cnex 11140 |
. . . . . . . . . 10
β’ β
β V |
4 | | elpmg 8787 |
. . . . . . . . . 10
β’ ((π β dom βMet β§
β β V) β (πΉ
β (π
βpm β) β (Fun πΉ β§ πΉ β (β Γ π)))) |
5 | 2, 3, 4 | sylancl 587 |
. . . . . . . . 9
β’ (π· β (βMetβπ) β (πΉ β (π βpm β) β (Fun
πΉ β§ πΉ β (β Γ π)))) |
6 | 5 | simprbda 500 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ πΉ β (π βpm β)) β Fun
πΉ) |
7 | | ffvresb 7076 |
. . . . . . . 8
β’ (Fun
πΉ β ((πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πΉβπ)(ballβπ·)π₯) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)))) |
8 | 6, 7 | syl 17 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ πΉ β (π βpm β)) β
((πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πΉβπ)(ballβπ·)π₯) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)))) |
9 | 8 | rexbidv 3172 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ πΉ β (π βpm β)) β
(βπ β β€
(πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πΉβπ)(ballβπ·)π₯) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)))) |
10 | 9 | adantr 482 |
. . . . 5
β’ (((π· β (βMetβπ) β§ πΉ β (π βpm β)) β§ π₯ β β+)
β (βπ β
β€ (πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πΉβπ)(ballβπ·)π₯) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)))) |
11 | | uzid 12786 |
. . . . . . . . . . 11
β’ (π β β€ β π β
(β€β₯βπ)) |
12 | 11 | adantl 483 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ π₯ β β+) β§ π β β€) β π β
(β€β₯βπ)) |
13 | | eleq1w 2817 |
. . . . . . . . . . . 12
β’ (π = π β (π β dom πΉ β π β dom πΉ)) |
14 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉβπ) = (πΉβπ)) |
15 | 14 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π = π β ((πΉβπ) β ((πΉβπ)(ballβπ·)π₯) β (πΉβπ) β ((πΉβπ)(ballβπ·)π₯))) |
16 | 13, 15 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π = π β ((π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)) β (π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)))) |
17 | 16 | rspcv 3579 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)) β (π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)))) |
18 | 12, 17 | syl 17 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π₯ β β+) β§ π β β€) β
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)) β (π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)))) |
19 | | n0i 4297 |
. . . . . . . . . . . 12
β’ ((πΉβπ) β ((πΉβπ)(ballβπ·)π₯) β Β¬ ((πΉβπ)(ballβπ·)π₯) = β
) |
20 | | blf 23783 |
. . . . . . . . . . . . . . 15
β’ (π· β (βMetβπ) β (ballβπ·):(π Γ
β*)βΆπ« π) |
21 | 20 | fdmd 6683 |
. . . . . . . . . . . . . 14
β’ (π· β (βMetβπ) β dom (ballβπ·) = (π Γ
β*)) |
22 | | ndmovg 7541 |
. . . . . . . . . . . . . . 15
β’ ((dom
(ballβπ·) = (π Γ β*)
β§ Β¬ ((πΉβπ) β π β§ π₯ β β*)) β ((πΉβπ)(ballβπ·)π₯) = β
) |
23 | 22 | ex 414 |
. . . . . . . . . . . . . 14
β’ (dom
(ballβπ·) = (π Γ β*)
β (Β¬ ((πΉβπ) β π β§ π₯ β β*) β ((πΉβπ)(ballβπ·)π₯) = β
)) |
24 | 21, 23 | syl 17 |
. . . . . . . . . . . . 13
β’ (π· β (βMetβπ) β (Β¬ ((πΉβπ) β π β§ π₯ β β*) β ((πΉβπ)(ballβπ·)π₯) = β
)) |
25 | 24 | con1d 145 |
. . . . . . . . . . . 12
β’ (π· β (βMetβπ) β (Β¬ ((πΉβπ)(ballβπ·)π₯) = β
β ((πΉβπ) β π β§ π₯ β
β*))) |
26 | | simpl 484 |
. . . . . . . . . . . 12
β’ (((πΉβπ) β π β§ π₯ β β*) β (πΉβπ) β π) |
27 | 19, 25, 26 | syl56 36 |
. . . . . . . . . . 11
β’ (π· β (βMetβπ) β ((πΉβπ) β ((πΉβπ)(ballβπ·)π₯) β (πΉβπ) β π)) |
28 | 27 | adantld 492 |
. . . . . . . . . 10
β’ (π· β (βMetβπ) β ((π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)) β (πΉβπ) β π)) |
29 | 28 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π₯ β β+) β§ π β β€) β ((π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)) β (πΉβπ) β π)) |
30 | 18, 29 | syld 47 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π₯ β β+) β§ π β β€) β
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)) β (πΉβπ) β π)) |
31 | 14 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π = π β ((πΉβπ) β π β (πΉβπ) β π)) |
32 | 14 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉβπ)π·(πΉβπ)) = ((πΉβπ)π·(πΉβπ))) |
33 | 32 | breq1d 5119 |
. . . . . . . . . . . 12
β’ (π = π β (((πΉβπ)π·(πΉβπ)) < π₯ β ((πΉβπ)π·(πΉβπ)) < π₯)) |
34 | 13, 31, 33 | 3anbi123d 1437 |
. . . . . . . . . . 11
β’ (π = π β ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
35 | 34 | rspcv 3579 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
36 | 12, 35 | syl 17 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π₯ β β+) β§ π β β€) β
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
37 | | simp2 1138 |
. . . . . . . . 9
β’ ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β (πΉβπ) β π) |
38 | 36, 37 | syl6 35 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π₯ β β+) β§ π β β€) β
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β (πΉβπ) β π)) |
39 | | rpxr 12932 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β+
β π₯ β
β*) |
40 | | elbl 23764 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ π₯ β β*) β ((πΉβπ) β ((πΉβπ)(ballβπ·)π₯) β ((πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
41 | 39, 40 | syl3an3 1166 |
. . . . . . . . . . . . . . 15
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ π₯ β β+) β ((πΉβπ) β ((πΉβπ)(ballβπ·)π₯) β ((πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
42 | | xmetsym 23723 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ (πΉβπ) β π) β ((πΉβπ)π·(πΉβπ)) = ((πΉβπ)π·(πΉβπ))) |
43 | 42 | 3expa 1119 |
. . . . . . . . . . . . . . . . . 18
β’ (((π· β (βMetβπ) β§ (πΉβπ) β π) β§ (πΉβπ) β π) β ((πΉβπ)π·(πΉβπ)) = ((πΉβπ)π·(πΉβπ))) |
44 | 43 | 3adantl3 1169 |
. . . . . . . . . . . . . . . . 17
β’ (((π· β (βMetβπ) β§ (πΉβπ) β π β§ π₯ β β+) β§ (πΉβπ) β π) β ((πΉβπ)π·(πΉβπ)) = ((πΉβπ)π·(πΉβπ))) |
45 | 44 | breq1d 5119 |
. . . . . . . . . . . . . . . 16
β’ (((π· β (βMetβπ) β§ (πΉβπ) β π β§ π₯ β β+) β§ (πΉβπ) β π) β (((πΉβπ)π·(πΉβπ)) < π₯ β ((πΉβπ)π·(πΉβπ)) < π₯)) |
46 | 45 | pm5.32da 580 |
. . . . . . . . . . . . . . 15
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ π₯ β β+) β (((πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β ((πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
47 | 41, 46 | bitrd 279 |
. . . . . . . . . . . . . 14
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ π₯ β β+) β ((πΉβπ) β ((πΉβπ)(ballβπ·)π₯) β ((πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
48 | 47 | 3com23 1127 |
. . . . . . . . . . . . 13
β’ ((π· β (βMetβπ) β§ π₯ β β+ β§ (πΉβπ) β π) β ((πΉβπ) β ((πΉβπ)(ballβπ·)π₯) β ((πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
49 | 48 | anbi2d 630 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π₯ β β+ β§ (πΉβπ) β π) β ((π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)) β (π β dom πΉ β§ ((πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
50 | | 3anass 1096 |
. . . . . . . . . . . 12
β’ ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β (π β dom πΉ β§ ((πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
51 | 49, 50 | bitr4di 289 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π₯ β β+ β§ (πΉβπ) β π) β ((π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)) β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
52 | 51 | ralbidv 3171 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π₯ β β+ β§ (πΉβπ) β π) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
53 | 52 | 3expia 1122 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π₯ β β+) β ((πΉβπ) β π β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
54 | 53 | adantr 482 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π₯ β β+) β§ π β β€) β ((πΉβπ) β π β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
55 | 30, 38, 54 | pm5.21ndd 381 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π₯ β β+) β§ π β β€) β
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
56 | 55 | rexbidva 3170 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π₯ β β+) β
(βπ β β€
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
57 | 56 | adantlr 714 |
. . . . 5
β’ (((π· β (βMetβπ) β§ πΉ β (π βpm β)) β§ π₯ β β+)
β (βπ β
β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((πΉβπ)(ballβπ·)π₯)) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
58 | 10, 57 | bitrd 279 |
. . . 4
β’ (((π· β (βMetβπ) β§ πΉ β (π βpm β)) β§ π₯ β β+)
β (βπ β
β€ (πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πΉβπ)(ballβπ·)π₯) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
59 | 58 | ralbidva 3169 |
. . 3
β’ ((π· β (βMetβπ) β§ πΉ β (π βpm β)) β
(βπ₯ β
β+ βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πΉβπ)(ballβπ·)π₯) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
60 | 59 | pm5.32da 580 |
. 2
β’ (π· β (βMetβπ) β ((πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πΉβπ)(ballβπ·)π₯)) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
61 | 1, 60 | bitrd 279 |
1
β’ (π· β (βMetβπ) β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |