Metamath Proof Explorer

Theorem stdbdbl

Description: The standard bounded metric corresponding to C generates the same balls as C for radii less than R . (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypothesis stdbdmet.1 
|- D = ( x e. X , y e. X |-> if ( ( x C y ) <_ R , ( x C y ) , R ) )
Assertion stdbdbl 
|- ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) -> ( P ( ball ` D ) S ) = ( P ( ball ` C ) S ) )

Proof

Step Hyp Ref Expression
1 stdbdmet.1 
 |-  D = ( x e. X , y e. X |-> if ( ( x C y ) <_ R , ( x C y ) , R ) )
2 simpll2 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> R e. RR* )
3 simpr1 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) -> P e. X )
4 3 adantr 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> P e. X )
5 simpr 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> z e. X )
6 1 stdbdmetval 
 |-  ( ( R e. RR* /\ P e. X /\ z e. X ) -> ( P D z ) = if ( ( P C z ) <_ R , ( P C z ) , R ) )
7 2 4 5 6 syl3anc 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> ( P D z ) = if ( ( P C z ) <_ R , ( P C z ) , R ) )
8 7 breq1d 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> ( ( P D z ) < S <-> if ( ( P C z ) <_ R , ( P C z ) , R ) < S ) )
9 simplr3 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> S <_ R )
10 9 biantrud 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> ( S <_ ( P C z ) <-> ( S <_ ( P C z ) /\ S <_ R ) ) )
11 simpr2 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) -> S e. RR* )
12 11 adantr 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> S e. RR* )
13 simpl1 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) -> C e. ( *Met ` X ) )
14 13 adantr 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> C e. ( *Met ` X ) )
15 xmetcl 
 |-  ( ( C e. ( *Met ` X ) /\ P e. X /\ z e. X ) -> ( P C z ) e. RR* )
16 14 4 5 15 syl3anc 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> ( P C z ) e. RR* )
17 xrlemin 
 |-  ( ( S e. RR* /\ ( P C z ) e. RR* /\ R e. RR* ) -> ( S <_ if ( ( P C z ) <_ R , ( P C z ) , R ) <-> ( S <_ ( P C z ) /\ S <_ R ) ) )
18 12 16 2 17 syl3anc 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> ( S <_ if ( ( P C z ) <_ R , ( P C z ) , R ) <-> ( S <_ ( P C z ) /\ S <_ R ) ) )
19 10 18 bitr4d 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> ( S <_ ( P C z ) <-> S <_ if ( ( P C z ) <_ R , ( P C z ) , R ) ) )
20 19 notbid 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> ( -. S <_ ( P C z ) <-> -. S <_ if ( ( P C z ) <_ R , ( P C z ) , R ) ) )
21 xrltnle 
 |-  ( ( ( P C z ) e. RR* /\ S e. RR* ) -> ( ( P C z ) < S <-> -. S <_ ( P C z ) ) )
22 16 12 21 syl2anc 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> ( ( P C z ) < S <-> -. S <_ ( P C z ) ) )
23 16 2 ifcld 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> if ( ( P C z ) <_ R , ( P C z ) , R ) e. RR* )
24 xrltnle 
 |-  ( ( if ( ( P C z ) <_ R , ( P C z ) , R ) e. RR* /\ S e. RR* ) -> ( if ( ( P C z ) <_ R , ( P C z ) , R ) < S <-> -. S <_ if ( ( P C z ) <_ R , ( P C z ) , R ) ) )
25 23 12 24 syl2anc 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> ( if ( ( P C z ) <_ R , ( P C z ) , R ) < S <-> -. S <_ if ( ( P C z ) <_ R , ( P C z ) , R ) ) )
26 20 22 25 3bitr4d 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> ( ( P C z ) < S <-> if ( ( P C z ) <_ R , ( P C z ) , R ) < S ) )
27 8 26 bitr4d 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) /\ z e. X ) -> ( ( P D z ) < S <-> ( P C z ) < S ) )
28 27 rabbidva 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) -> { z e. X | ( P D z ) < S } = { z e. X | ( P C z ) < S } )
29 1 stdbdxmet 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> D e. ( *Met ` X ) )
30 29 adantr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) -> D e. ( *Met ` X ) )
31 blval 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ S e. RR* ) -> ( P ( ball ` D ) S ) = { z e. X | ( P D z ) < S } )
32 30 3 11 31 syl3anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) -> ( P ( ball ` D ) S ) = { z e. X | ( P D z ) < S } )
33 blval 
 |-  ( ( C e. ( *Met ` X ) /\ P e. X /\ S e. RR* ) -> ( P ( ball ` C ) S ) = { z e. X | ( P C z ) < S } )
34 13 3 11 33 syl3anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) -> ( P ( ball ` C ) S ) = { z e. X | ( P C z ) < S } )
35 28 32 34 3eqtr4d 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) -> ( P ( ball ` D ) S ) = ( P ( ball ` C ) S ) )