Step | Hyp | Ref
| Expression |
1 | | simpr2 1004 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β π β
β*) |
2 | 1 | adantr 276 |
. . . . 5
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β π β
β*) |
3 | | simpl1 1000 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β πΆ β (βMetβπ)) |
4 | 3 | adantr 276 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β πΆ β (βMetβπ)) |
5 | | simpr1 1003 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β π β π) |
6 | 5 | adantr 276 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β π β π) |
7 | | simpr 110 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β π§ β π) |
8 | | xmetcl 13788 |
. . . . . 6
β’ ((πΆ β (βMetβπ) β§ π β π β§ π§ β π) β (ππΆπ§) β
β*) |
9 | 4, 6, 7, 8 | syl3anc 1238 |
. . . . 5
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β (ππΆπ§) β
β*) |
10 | | simpll2 1037 |
. . . . 5
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β π
β
β*) |
11 | | xrminltinf 11279 |
. . . . 5
β’ ((π β β*
β§ (ππΆπ§) β β* β§ π
β β*)
β (inf({(ππΆπ§), π
}, β*, < ) < π β ((ππΆπ§) < π β¨ π
< π))) |
12 | 2, 9, 10, 11 | syl3anc 1238 |
. . . 4
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β (inf({(ππΆπ§), π
}, β*, < ) < π β ((ππΆπ§) < π β¨ π
< π))) |
13 | | xmetf 13786 |
. . . . . . . . 9
β’ (πΆ β (βMetβπ) β πΆ:(π Γ π)βΆβ*) |
14 | 13 | 3ad2ant1 1018 |
. . . . . . . 8
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β πΆ:(π Γ π)βΆβ*) |
15 | 14 | adantr 276 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β πΆ:(π Γ π)βΆβ*) |
16 | 15 | adantr 276 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β πΆ:(π Γ π)βΆβ*) |
17 | | stdbdmet.1 |
. . . . . . 7
β’ π· = (π₯ β π, π¦ β π β¦ inf({(π₯πΆπ¦), π
}, β*, <
)) |
18 | 17 | bdmetval 13936 |
. . . . . 6
β’ (((πΆ:(π Γ π)βΆβ* β§ π
β β*)
β§ (π β π β§ π§ β π)) β (ππ·π§) = inf({(ππΆπ§), π
}, β*, <
)) |
19 | 16, 10, 6, 7, 18 | syl22anc 1239 |
. . . . 5
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β (ππ·π§) = inf({(ππΆπ§), π
}, β*, <
)) |
20 | 19 | breq1d 4013 |
. . . 4
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β ((ππ·π§) < π β inf({(ππΆπ§), π
}, β*, < ) < π)) |
21 | | simpr3 1005 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β π β€ π
) |
22 | | simpl2 1001 |
. . . . . . . . 9
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β π
β
β*) |
23 | | xrlenlt 8021 |
. . . . . . . . 9
β’ ((π β β*
β§ π
β
β*) β (π β€ π
β Β¬ π
< π)) |
24 | 1, 22, 23 | syl2anc 411 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β (π β€ π
β Β¬ π
< π)) |
25 | 21, 24 | mpbid 147 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β Β¬ π
< π) |
26 | | biorf 744 |
. . . . . . 7
β’ (Β¬
π
< π β ((ππΆπ§) < π β (π
< π β¨ (ππΆπ§) < π))) |
27 | 25, 26 | syl 14 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β ((ππΆπ§) < π β (π
< π β¨ (ππΆπ§) < π))) |
28 | | orcom 728 |
. . . . . 6
β’ ((π
< π β¨ (ππΆπ§) < π) β ((ππΆπ§) < π β¨ π
< π)) |
29 | 27, 28 | bitrdi 196 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β ((ππΆπ§) < π β ((ππΆπ§) < π β¨ π
< π))) |
30 | 29 | adantr 276 |
. . . 4
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β ((ππΆπ§) < π β ((ππΆπ§) < π β¨ π
< π))) |
31 | 12, 20, 30 | 3bitr4d 220 |
. . 3
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β§ π§ β π) β ((ππ·π§) < π β (ππΆπ§) < π)) |
32 | 31 | rabbidva 2725 |
. 2
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β {π§ β π β£ (ππ·π§) < π} = {π§ β π β£ (ππΆπ§) < π}) |
33 | 17 | bdxmet 13937 |
. . . 4
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β π· β (βMetβπ)) |
34 | 33 | adantr 276 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β π· β (βMetβπ)) |
35 | | blval 13825 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (π(ballβπ·)π) = {π§ β π β£ (ππ·π§) < π}) |
36 | 34, 5, 1, 35 | syl3anc 1238 |
. 2
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β (π(ballβπ·)π) = {π§ β π β£ (ππ·π§) < π}) |
37 | | blval 13825 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π β π β§ π β β*) β (π(ballβπΆ)π) = {π§ β π β£ (ππΆπ§) < π}) |
38 | 3, 5, 1, 37 | syl3anc 1238 |
. 2
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β (π(ballβπΆ)π) = {π§ β π β£ (ππΆπ§) < π}) |
39 | 32, 36, 38 | 3eqtr4d 2220 |
1
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β (π(ballβπ·)π) = (π(ballβπΆ)π)) |