Step | Hyp | Ref
| Expression |
1 | | rpxr 12983 |
. . . . . . . 8
β’ (π β β+
β π β
β*) |
2 | 1 | ad2antll 728 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β π β
β*) |
3 | | simpl2 1193 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β π
β
β*) |
4 | 2, 3 | ifcld 4575 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β if(π β€ π
, π, π
) β
β*) |
5 | | rpre 12982 |
. . . . . . 7
β’ (π β β+
β π β
β) |
6 | 5 | ad2antll 728 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β π β
β) |
7 | | rpgt0 12986 |
. . . . . . . . 9
β’ (π β β+
β 0 < π) |
8 | 7 | ad2antll 728 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β 0 <
π) |
9 | | simpl3 1194 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β 0 <
π
) |
10 | | breq2 5153 |
. . . . . . . . 9
β’ (π = if(π β€ π
, π, π
) β (0 < π β 0 < if(π β€ π
, π, π
))) |
11 | | breq2 5153 |
. . . . . . . . 9
β’ (π
= if(π β€ π
, π, π
) β (0 < π
β 0 < if(π β€ π
, π, π
))) |
12 | 10, 11 | ifboth 4568 |
. . . . . . . 8
β’ ((0 <
π β§ 0 < π
) β 0 < if(π β€ π
, π, π
)) |
13 | 8, 9, 12 | syl2anc 585 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β 0 <
if(π β€ π
, π, π
)) |
14 | | 0xr 11261 |
. . . . . . . 8
β’ 0 β
β* |
15 | | xrltle 13128 |
. . . . . . . 8
β’ ((0
β β* β§ if(π β€ π
, π, π
) β β*) β (0 <
if(π β€ π
, π, π
) β 0 β€ if(π β€ π
, π, π
))) |
16 | 14, 4, 15 | sylancr 588 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β (0 <
if(π β€ π
, π, π
) β 0 β€ if(π β€ π
, π, π
))) |
17 | 13, 16 | mpd 15 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β 0 β€
if(π β€ π
, π, π
)) |
18 | | xrmin1 13156 |
. . . . . . 7
β’ ((π β β*
β§ π
β
β*) β if(π β€ π
, π, π
) β€ π) |
19 | 2, 3, 18 | syl2anc 585 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β if(π β€ π
, π, π
) β€ π) |
20 | | xrrege0 13153 |
. . . . . 6
β’
(((if(π β€ π
, π, π
) β β* β§ π β β) β§ (0 β€
if(π β€ π
, π, π
) β§ if(π β€ π
, π, π
) β€ π)) β if(π β€ π
, π, π
) β β) |
21 | 4, 6, 17, 19, 20 | syl22anc 838 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β if(π β€ π
, π, π
) β β) |
22 | 21, 13 | elrpd 13013 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β if(π β€ π
, π, π
) β
β+) |
23 | | simprl 770 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β π§ β π) |
24 | | xrmin2 13157 |
. . . . . . . 8
β’ ((π β β*
β§ π
β
β*) β if(π β€ π
, π, π
) β€ π
) |
25 | 2, 3, 24 | syl2anc 585 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β if(π β€ π
, π, π
) β€ π
) |
26 | 23, 4, 25 | 3jca 1129 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β (π§ β π β§ if(π β€ π
, π, π
) β β* β§ if(π β€ π
, π, π
) β€ π
)) |
27 | | stdbdmet.1 |
. . . . . . 7
β’ π· = (π₯ β π, π¦ β π β¦ if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
)) |
28 | 27 | stdbdbl 24026 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ if(π β€ π
, π, π
) β β* β§ if(π β€ π
, π, π
) β€ π
)) β (π§(ballβπ·)if(π β€ π
, π, π
)) = (π§(ballβπΆ)if(π β€ π
, π, π
))) |
29 | 26, 28 | syldan 592 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β (π§(ballβπ·)if(π β€ π
, π, π
)) = (π§(ballβπΆ)if(π β€ π
, π, π
))) |
30 | 29 | eqcomd 2739 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β (π§(ballβπΆ)if(π β€ π
, π, π
)) = (π§(ballβπ·)if(π β€ π
, π, π
))) |
31 | | breq1 5152 |
. . . . . 6
β’ (π = if(π β€ π
, π, π
) β (π β€ π β if(π β€ π
, π, π
) β€ π)) |
32 | | oveq2 7417 |
. . . . . . 7
β’ (π = if(π β€ π
, π, π
) β (π§(ballβπΆ)π ) = (π§(ballβπΆ)if(π β€ π
, π, π
))) |
33 | | oveq2 7417 |
. . . . . . 7
β’ (π = if(π β€ π
, π, π
) β (π§(ballβπ·)π ) = (π§(ballβπ·)if(π β€ π
, π, π
))) |
34 | 32, 33 | eqeq12d 2749 |
. . . . . 6
β’ (π = if(π β€ π
, π, π
) β ((π§(ballβπΆ)π ) = (π§(ballβπ·)π ) β (π§(ballβπΆ)if(π β€ π
, π, π
)) = (π§(ballβπ·)if(π β€ π
, π, π
)))) |
35 | 31, 34 | anbi12d 632 |
. . . . 5
β’ (π = if(π β€ π
, π, π
) β ((π β€ π β§ (π§(ballβπΆ)π ) = (π§(ballβπ·)π )) β (if(π β€ π
, π, π
) β€ π β§ (π§(ballβπΆ)if(π β€ π
, π, π
)) = (π§(ballβπ·)if(π β€ π
, π, π
))))) |
36 | 35 | rspcev 3613 |
. . . 4
β’
((if(π β€ π
, π, π
) β β+ β§ (if(π β€ π
, π, π
) β€ π β§ (π§(ballβπΆ)if(π β€ π
, π, π
)) = (π§(ballβπ·)if(π β€ π
, π, π
)))) β βπ β β+ (π β€ π β§ (π§(ballβπΆ)π ) = (π§(ballβπ·)π ))) |
37 | 22, 19, 30, 36 | syl12anc 836 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π§ β π β§ π β β+)) β
βπ β
β+ (π β€
π β§ (π§(ballβπΆ)π ) = (π§(ballβπ·)π ))) |
38 | 37 | ralrimivva 3201 |
. 2
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β βπ§ β π βπ β β+ βπ β β+
(π β€ π β§ (π§(ballβπΆ)π ) = (π§(ballβπ·)π ))) |
39 | | simp1 1137 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β πΆ β (βMetβπ)) |
40 | 27 | stdbdxmet 24024 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β π· β (βMetβπ)) |
41 | | stdbdmopn.2 |
. . . 4
β’ π½ = (MetOpenβπΆ) |
42 | | eqid 2733 |
. . . 4
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
43 | 41, 42 | metequiv2 24019 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β (βπ§ β π βπ β β+ βπ β β+
(π β€ π β§ (π§(ballβπΆ)π ) = (π§(ballβπ·)π )) β π½ = (MetOpenβπ·))) |
44 | 39, 40, 43 | syl2anc 585 |
. 2
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β (βπ§ β π βπ β β+ βπ β β+
(π β€ π β§ (π§(ballβπΆ)π ) = (π§(ballβπ·)π )) β π½ = (MetOpenβπ·))) |
45 | 38, 44 | mpd 15 |
1
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β π½ = (MetOpenβπ·)) |