Step | Hyp | Ref
| Expression |
1 | | simpll2 1214 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β π
β
β*) |
2 | | simpr1 1195 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β π β π) |
3 | 2 | adantr 482 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β π β π) |
4 | | simpr 486 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β π§ β π) |
5 | | stdbdmet.1 |
. . . . . . 7
β’ π· = (π₯ β π, π¦ β π β¦ if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
)) |
6 | 5 | stdbdmetval 23886 |
. . . . . 6
β’ ((π
β β*
β§ π β π β§ π§ β π) β (ππ·π§) = if((ππΆπ§) β€ π
, (ππΆπ§), π
)) |
7 | 1, 3, 4, 6 | syl3anc 1372 |
. . . . 5
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β (ππ·π§) = if((ππΆπ§) β€ π
, (ππΆπ§), π
)) |
8 | 7 | breq1d 5116 |
. . . 4
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β ((ππ·π§) < π β if((ππΆπ§) β€ π
, (ππΆπ§), π
) < π)) |
9 | | simplr3 1218 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β π β€ π
) |
10 | 9 | biantrud 533 |
. . . . . . 7
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β (π β€ (ππΆπ§) β (π β€ (ππΆπ§) β§ π β€ π
))) |
11 | | simpr2 1196 |
. . . . . . . . 9
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β π β
β*) |
12 | 11 | adantr 482 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β π β
β*) |
13 | | simpl1 1192 |
. . . . . . . . . 10
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β πΆ β (βMetβπ)) |
14 | 13 | adantr 482 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β πΆ β (βMetβπ)) |
15 | | xmetcl 23700 |
. . . . . . . . 9
β’ ((πΆ β (βMetβπ) β§ π β π β§ π§ β π) β (ππΆπ§) β
β*) |
16 | 14, 3, 4, 15 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β (ππΆπ§) β
β*) |
17 | | xrlemin 13109 |
. . . . . . . 8
β’ ((π β β*
β§ (ππΆπ§) β β* β§ π
β β*)
β (π β€ if((ππΆπ§) β€ π
, (ππΆπ§), π
) β (π β€ (ππΆπ§) β§ π β€ π
))) |
18 | 12, 16, 1, 17 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β (π β€ if((ππΆπ§) β€ π
, (ππΆπ§), π
) β (π β€ (ππΆπ§) β§ π β€ π
))) |
19 | 10, 18 | bitr4d 282 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β (π β€ (ππΆπ§) β π β€ if((ππΆπ§) β€ π
, (ππΆπ§), π
))) |
20 | 19 | notbid 318 |
. . . . 5
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β (Β¬ π β€ (ππΆπ§) β Β¬ π β€ if((ππΆπ§) β€ π
, (ππΆπ§), π
))) |
21 | | xrltnle 11227 |
. . . . . 6
β’ (((ππΆπ§) β β* β§ π β β*)
β ((ππΆπ§) < π β Β¬ π β€ (ππΆπ§))) |
22 | 16, 12, 21 | syl2anc 585 |
. . . . 5
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β ((ππΆπ§) < π β Β¬ π β€ (ππΆπ§))) |
23 | 16, 1 | ifcld 4533 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β if((ππΆπ§) β€ π
, (ππΆπ§), π
) β
β*) |
24 | | xrltnle 11227 |
. . . . . 6
β’
((if((ππΆπ§) β€ π
, (ππΆπ§), π
) β β* β§ π β β*)
β (if((ππΆπ§) β€ π
, (ππΆπ§), π
) < π β Β¬ π β€ if((ππΆπ§) β€ π
, (ππΆπ§), π
))) |
25 | 23, 12, 24 | syl2anc 585 |
. . . . 5
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β (if((ππΆπ§) β€ π
, (ππΆπ§), π
) < π β Β¬ π β€ if((ππΆπ§) β€ π
, (ππΆπ§), π
))) |
26 | 20, 22, 25 | 3bitr4d 311 |
. . . 4
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β ((ππΆπ§) < π β if((ππΆπ§) β€ π
, (ππΆπ§), π
) < π)) |
27 | 8, 26 | bitr4d 282 |
. . 3
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β ((ππ·π§) < π β (ππΆπ§) < π)) |
28 | 27 | rabbidva 3413 |
. 2
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β {π§ β π β£ (ππ·π§) < π} = {π§ β π β£ (ππΆπ§) < π}) |
29 | 5 | stdbdxmet 23887 |
. . . 4
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β π· β (βMetβπ)) |
30 | 29 | adantr 482 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β π· β (βMetβπ)) |
31 | | blval 23755 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (π(ballβπ·)π) = {π§ β π β£ (ππ·π§) < π}) |
32 | 30, 2, 11, 31 | syl3anc 1372 |
. 2
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β (π(ballβπ·)π) = {π§ β π β£ (ππ·π§) < π}) |
33 | | blval 23755 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π β π β§ π β β*) β (π(ballβπΆ)π) = {π§ β π β£ (ππΆπ§) < π}) |
34 | 13, 2, 11, 33 | syl3anc 1372 |
. 2
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β (π(ballβπΆ)π) = {π§ β π β£ (ππΆπ§) < π}) |
35 | 28, 32, 34 | 3eqtr4d 2783 |
1
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β (π(ballβπ·)π) = (π(ballβπΆ)π)) |