Metamath Proof Explorer

Theorem stdbdxmet

Description: The standard bounded metric is an extended metric given an extended metric and a positive extended real cutoff. (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 stdbdxmet 
|- ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> D e. ( *Met ` X ) )

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 simp1 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> C e. ( *Met ` X ) )
3 xmetcl 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ y e. X ) -> ( x C y ) e. RR* )
4 xmetge0 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ y e. X ) -> 0 <_ ( x C y ) )
5 elxrge0 
 |-  ( ( x C y ) e. ( 0 [,] +oo ) <-> ( ( x C y ) e. RR* /\ 0 <_ ( x C y ) ) )
6 3 4 5 sylanbrc 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ y e. X ) -> ( x C y ) e. ( 0 [,] +oo ) )
7 6 3expb 
 |-  ( ( C e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) -> ( x C y ) e. ( 0 [,] +oo ) )
8 2 7 sylan 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( x e. X /\ y e. X ) ) -> ( x C y ) e. ( 0 [,] +oo ) )
9 xmetf 
 |-  ( C e. ( *Met ` X ) -> C : ( X X. X ) --> RR* )
10 9 3ad2ant1 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> C : ( X X. X ) --> RR* )
11 10 ffnd 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> C Fn ( X X. X ) )
12 fnov 
 |-  ( C Fn ( X X. X ) <-> C = ( x e. X , y e. X |-> ( x C y ) ) )
13 11 12 sylib 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> C = ( x e. X , y e. X |-> ( x C y ) ) )
14 eqidd 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) = ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) )
15 breq1 
 |-  ( z = ( x C y ) -> ( z <_ R <-> ( x C y ) <_ R ) )
16 id 
 |-  ( z = ( x C y ) -> z = ( x C y ) )
17 15 16 ifbieq1d 
 |-  ( z = ( x C y ) -> if ( z <_ R , z , R ) = if ( ( x C y ) <_ R , ( x C y ) , R ) )
18 8 13 14 17 fmpoco 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) o. C ) = ( x e. X , y e. X |-> if ( ( x C y ) <_ R , ( x C y ) , R ) ) )
19 18 1 eqtr4di 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) o. C ) = D )
20 eliccxr 
 |-  ( z e. ( 0 [,] +oo ) -> z e. RR* )
21 simp2 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> R e. RR* )
22 ifcl 
 |-  ( ( z e. RR* /\ R e. RR* ) -> if ( z <_ R , z , R ) e. RR* )
23 20 21 22 syl2anr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ z e. ( 0 [,] +oo ) ) -> if ( z <_ R , z , R ) e. RR* )
24 23 fmpttd 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) : ( 0 [,] +oo ) --> RR* )
25 id 
 |-  ( a e. ( 0 [,] +oo ) -> a e. ( 0 [,] +oo ) )
26 vex 
 |-  a e. _V
27 ifexg 
 |-  ( ( a e. _V /\ R e. RR* ) -> if ( a <_ R , a , R ) e. _V )
28 26 21 27 sylancr 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> if ( a <_ R , a , R ) e. _V )
29 breq1 
 |-  ( z = a -> ( z <_ R <-> a <_ R ) )
30 id 
 |-  ( z = a -> z = a )
31 29 30 ifbieq1d 
 |-  ( z = a -> if ( z <_ R , z , R ) = if ( a <_ R , a , R ) )
32 eqid 
 |-  ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) = ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) )
33 31 32 fvmptg 
 |-  ( ( a e. ( 0 [,] +oo ) /\ if ( a <_ R , a , R ) e. _V ) -> ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` a ) = if ( a <_ R , a , R ) )
34 25 28 33 syl2anr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ a e. ( 0 [,] +oo ) ) -> ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` a ) = if ( a <_ R , a , R ) )
35 34 eqeq1d 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ a e. ( 0 [,] +oo ) ) -> ( ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` a ) = 0 <-> if ( a <_ R , a , R ) = 0 ) )
36 eqeq1 
 |-  ( a = if ( a <_ R , a , R ) -> ( a = 0 <-> if ( a <_ R , a , R ) = 0 ) )
37 36 bibi1d 
 |-  ( a = if ( a <_ R , a , R ) -> ( ( a = 0 <-> a = 0 ) <-> ( if ( a <_ R , a , R ) = 0 <-> a = 0 ) ) )
38 eqeq1 
 |-  ( R = if ( a <_ R , a , R ) -> ( R = 0 <-> if ( a <_ R , a , R ) = 0 ) )
39 38 bibi1d 
 |-  ( R = if ( a <_ R , a , R ) -> ( ( R = 0 <-> a = 0 ) <-> ( if ( a <_ R , a , R ) = 0 <-> a = 0 ) ) )
40 biidd 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ a e. ( 0 [,] +oo ) ) /\ a <_ R ) -> ( a = 0 <-> a = 0 ) )
41 simp3 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> 0 < R )
42 41 gt0ne0d 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> R =/= 0 )
43 42 neneqd 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> -. R = 0 )
44 43 ad2antrr 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ a e. ( 0 [,] +oo ) ) /\ -. a <_ R ) -> -. R = 0 )
45 0xr 
 |-  0 e. RR*
46 xrltle 
 |-  ( ( 0 e. RR* /\ R e. RR* ) -> ( 0 < R -> 0 <_ R ) )
47 45 21 46 sylancr 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> ( 0 < R -> 0 <_ R ) )
48 41 47 mpd 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> 0 <_ R )
49 48 adantr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ a e. ( 0 [,] +oo ) ) -> 0 <_ R )
50 breq1 
 |-  ( a = 0 -> ( a <_ R <-> 0 <_ R ) )
51 49 50 syl5ibrcom 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ a e. ( 0 [,] +oo ) ) -> ( a = 0 -> a <_ R ) )
52 51 con3dimp 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ a e. ( 0 [,] +oo ) ) /\ -. a <_ R ) -> -. a = 0 )
53 44 52 2falsed 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ a e. ( 0 [,] +oo ) ) /\ -. a <_ R ) -> ( R = 0 <-> a = 0 ) )
54 37 39 40 53 ifbothda 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ a e. ( 0 [,] +oo ) ) -> ( if ( a <_ R , a , R ) = 0 <-> a = 0 ) )
55 35 54 bitrd 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ a e. ( 0 [,] +oo ) ) -> ( ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` a ) = 0 <-> a = 0 ) )
56 eliccxr 
 |-  ( a e. ( 0 [,] +oo ) -> a e. RR* )
57 56 ad2antrl 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> a e. RR* )
58 21 adantr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> R e. RR* )
59 xrmin1 
 |-  ( ( a e. RR* /\ R e. RR* ) -> if ( a <_ R , a , R ) <_ a )
60 57 58 59 syl2anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> if ( a <_ R , a , R ) <_ a )
61 57 58 ifcld 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> if ( a <_ R , a , R ) e. RR* )
62 eliccxr 
 |-  ( b e. ( 0 [,] +oo ) -> b e. RR* )
63 62 ad2antll 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> b e. RR* )
64 xrletr 
 |-  ( ( if ( a <_ R , a , R ) e. RR* /\ a e. RR* /\ b e. RR* ) -> ( ( if ( a <_ R , a , R ) <_ a /\ a <_ b ) -> if ( a <_ R , a , R ) <_ b ) )
65 61 57 63 64 syl3anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( ( if ( a <_ R , a , R ) <_ a /\ a <_ b ) -> if ( a <_ R , a , R ) <_ b ) )
66 60 65 mpand 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( a <_ b -> if ( a <_ R , a , R ) <_ b ) )
67 xrmin2 
 |-  ( ( a e. RR* /\ R e. RR* ) -> if ( a <_ R , a , R ) <_ R )
68 57 58 67 syl2anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> if ( a <_ R , a , R ) <_ R )
69 66 68 jctird 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( a <_ b -> ( if ( a <_ R , a , R ) <_ b /\ if ( a <_ R , a , R ) <_ R ) ) )
70 xrlemin 
 |-  ( ( if ( a <_ R , a , R ) e. RR* /\ b e. RR* /\ R e. RR* ) -> ( if ( a <_ R , a , R ) <_ if ( b <_ R , b , R ) <-> ( if ( a <_ R , a , R ) <_ b /\ if ( a <_ R , a , R ) <_ R ) ) )
71 61 63 58 70 syl3anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( if ( a <_ R , a , R ) <_ if ( b <_ R , b , R ) <-> ( if ( a <_ R , a , R ) <_ b /\ if ( a <_ R , a , R ) <_ R ) ) )
72 69 71 sylibrd 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( a <_ b -> if ( a <_ R , a , R ) <_ if ( b <_ R , b , R ) ) )
73 34 adantrr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` a ) = if ( a <_ R , a , R ) )
74 simpr 
 |-  ( ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) -> b e. ( 0 [,] +oo ) )
75 vex 
 |-  b e. _V
76 ifexg 
 |-  ( ( b e. _V /\ R e. RR* ) -> if ( b <_ R , b , R ) e. _V )
77 75 21 76 sylancr 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> if ( b <_ R , b , R ) e. _V )
78 breq1 
 |-  ( z = b -> ( z <_ R <-> b <_ R ) )
79 id 
 |-  ( z = b -> z = b )
80 78 79 ifbieq1d 
 |-  ( z = b -> if ( z <_ R , z , R ) = if ( b <_ R , b , R ) )
81 80 32 fvmptg 
 |-  ( ( b e. ( 0 [,] +oo ) /\ if ( b <_ R , b , R ) e. _V ) -> ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` b ) = if ( b <_ R , b , R ) )
82 74 77 81 syl2anr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` b ) = if ( b <_ R , b , R ) )
83 73 82 breq12d 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` a ) <_ ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` b ) <-> if ( a <_ R , a , R ) <_ if ( b <_ R , b , R ) ) )
84 72 83 sylibrd 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( a <_ b -> ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` a ) <_ ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` b ) ) )
85 57 63 xaddcld 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( a +e b ) e. RR* )
86 xrmin1 
 |-  ( ( ( a +e b ) e. RR* /\ R e. RR* ) -> if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( a +e b ) )
87 85 58 86 syl2anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( a +e b ) )
88 85 58 ifcld 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> if ( ( a +e b ) <_ R , ( a +e b ) , R ) e. RR* )
89 57 58 xaddcld 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( a +e R ) e. RR* )
90 xrmin2 
 |-  ( ( ( a +e b ) e. RR* /\ R e. RR* ) -> if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ R )
91 85 58 90 syl2anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ R )
92 xaddid2 
 |-  ( R e. RR* -> ( 0 +e R ) = R )
93 58 92 syl 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( 0 +e R ) = R )
94 45 a1i 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> 0 e. RR* )
95 elxrge0 
 |-  ( a e. ( 0 [,] +oo ) <-> ( a e. RR* /\ 0 <_ a ) )
96 95 simprbi 
 |-  ( a e. ( 0 [,] +oo ) -> 0 <_ a )
97 96 ad2antrl 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> 0 <_ a )
98 xleadd1a 
 |-  ( ( ( 0 e. RR* /\ a e. RR* /\ R e. RR* ) /\ 0 <_ a ) -> ( 0 +e R ) <_ ( a +e R ) )
99 94 57 58 97 98 syl31anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( 0 +e R ) <_ ( a +e R ) )
100 93 99 eqbrtrrd 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> R <_ ( a +e R ) )
101 88 58 89 91 100 xrletrd 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( a +e R ) )
102 oveq2 
 |-  ( b = if ( b <_ R , b , R ) -> ( a +e b ) = ( a +e if ( b <_ R , b , R ) ) )
103 102 breq2d 
 |-  ( b = if ( b <_ R , b , R ) -> ( if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( a +e b ) <-> if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( a +e if ( b <_ R , b , R ) ) ) )
104 oveq2 
 |-  ( R = if ( b <_ R , b , R ) -> ( a +e R ) = ( a +e if ( b <_ R , b , R ) ) )
105 104 breq2d 
 |-  ( R = if ( b <_ R , b , R ) -> ( if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( a +e R ) <-> if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( a +e if ( b <_ R , b , R ) ) ) )
106 103 105 ifboth 
 |-  ( ( if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( a +e b ) /\ if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( a +e R ) ) -> if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( a +e if ( b <_ R , b , R ) ) )
107 87 101 106 syl2anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( a +e if ( b <_ R , b , R ) ) )
108 63 58 ifcld 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> if ( b <_ R , b , R ) e. RR* )
109 58 108 xaddcld 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( R +e if ( b <_ R , b , R ) ) e. RR* )
110 58 xaddid1d 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( R +e 0 ) = R )
111 elxrge0 
 |-  ( b e. ( 0 [,] +oo ) <-> ( b e. RR* /\ 0 <_ b ) )
112 111 simprbi 
 |-  ( b e. ( 0 [,] +oo ) -> 0 <_ b )
113 112 ad2antll 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> 0 <_ b )
114 48 adantr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> 0 <_ R )
115 breq2 
 |-  ( b = if ( b <_ R , b , R ) -> ( 0 <_ b <-> 0 <_ if ( b <_ R , b , R ) ) )
116 breq2 
 |-  ( R = if ( b <_ R , b , R ) -> ( 0 <_ R <-> 0 <_ if ( b <_ R , b , R ) ) )
117 115 116 ifboth 
 |-  ( ( 0 <_ b /\ 0 <_ R ) -> 0 <_ if ( b <_ R , b , R ) )
118 113 114 117 syl2anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> 0 <_ if ( b <_ R , b , R ) )
119 xleadd2a 
 |-  ( ( ( 0 e. RR* /\ if ( b <_ R , b , R ) e. RR* /\ R e. RR* ) /\ 0 <_ if ( b <_ R , b , R ) ) -> ( R +e 0 ) <_ ( R +e if ( b <_ R , b , R ) ) )
120 94 108 58 118 119 syl31anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( R +e 0 ) <_ ( R +e if ( b <_ R , b , R ) ) )
121 110 120 eqbrtrrd 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> R <_ ( R +e if ( b <_ R , b , R ) ) )
122 88 58 109 91 121 xrletrd 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( R +e if ( b <_ R , b , R ) ) )
123 oveq1 
 |-  ( a = if ( a <_ R , a , R ) -> ( a +e if ( b <_ R , b , R ) ) = ( if ( a <_ R , a , R ) +e if ( b <_ R , b , R ) ) )
124 123 breq2d 
 |-  ( a = if ( a <_ R , a , R ) -> ( if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( a +e if ( b <_ R , b , R ) ) <-> if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( if ( a <_ R , a , R ) +e if ( b <_ R , b , R ) ) ) )
125 oveq1 
 |-  ( R = if ( a <_ R , a , R ) -> ( R +e if ( b <_ R , b , R ) ) = ( if ( a <_ R , a , R ) +e if ( b <_ R , b , R ) ) )
126 125 breq2d 
 |-  ( R = if ( a <_ R , a , R ) -> ( if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( R +e if ( b <_ R , b , R ) ) <-> if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( if ( a <_ R , a , R ) +e if ( b <_ R , b , R ) ) ) )
127 124 126 ifboth 
 |-  ( ( if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( a +e if ( b <_ R , b , R ) ) /\ if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( R +e if ( b <_ R , b , R ) ) ) -> if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( if ( a <_ R , a , R ) +e if ( b <_ R , b , R ) ) )
128 107 122 127 syl2anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> if ( ( a +e b ) <_ R , ( a +e b ) , R ) <_ ( if ( a <_ R , a , R ) +e if ( b <_ R , b , R ) ) )
129 ge0xaddcl 
 |-  ( ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) -> ( a +e b ) e. ( 0 [,] +oo ) )
130 ovex 
 |-  ( a +e b ) e. _V
131 ifexg 
 |-  ( ( ( a +e b ) e. _V /\ R e. RR* ) -> if ( ( a +e b ) <_ R , ( a +e b ) , R ) e. _V )
132 130 21 131 sylancr 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> if ( ( a +e b ) <_ R , ( a +e b ) , R ) e. _V )
133 breq1 
 |-  ( z = ( a +e b ) -> ( z <_ R <-> ( a +e b ) <_ R ) )
134 id 
 |-  ( z = ( a +e b ) -> z = ( a +e b ) )
135 133 134 ifbieq1d 
 |-  ( z = ( a +e b ) -> if ( z <_ R , z , R ) = if ( ( a +e b ) <_ R , ( a +e b ) , R ) )
136 135 32 fvmptg 
 |-  ( ( ( a +e b ) e. ( 0 [,] +oo ) /\ if ( ( a +e b ) <_ R , ( a +e b ) , R ) e. _V ) -> ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` ( a +e b ) ) = if ( ( a +e b ) <_ R , ( a +e b ) , R ) )
137 129 132 136 syl2anr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` ( a +e b ) ) = if ( ( a +e b ) <_ R , ( a +e b ) , R ) )
138 73 82 oveq12d 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` a ) +e ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` b ) ) = ( if ( a <_ R , a , R ) +e if ( b <_ R , b , R ) ) )
139 128 137 138 3brtr4d 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) ) -> ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` ( a +e b ) ) <_ ( ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` a ) +e ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) ` b ) ) )
140 2 24 55 84 139 comet 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> ( ( z e. ( 0 [,] +oo ) |-> if ( z <_ R , z , R ) ) o. C ) e. ( *Met ` X ) )
141 19 140 eqeltrrd 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> D e. ( *Met ` X ) )