Metamath Proof Explorer

Theorem metdstri

Description: A generalization of the triangle inequality to the point-set distance function. Under the usual notation where the same symbol d denotes the point-point and point-set distance functions, this theorem would be written d ( a , S ) <_ d ( a , b ) + d ( b , S ) . (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypothesis metdscn.f 
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
Assertion metdstri 
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) <_ ( ( A D B ) +e ( F ` B ) ) )

Proof

Step Hyp Ref Expression
1 metdscn.f 
 |-  F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
2 simprr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( F ` A ) e. RR )
3 simprl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( A D B ) e. RR )
4 rexsub 
 |-  ( ( ( F ` A ) e. RR /\ ( A D B ) e. RR ) -> ( ( F ` A ) +e -e ( A D B ) ) = ( ( F ` A ) - ( A D B ) ) )
5 2 3 4 syl2anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( ( F ` A ) +e -e ( A D B ) ) = ( ( F ` A ) - ( A D B ) ) )
6 5 oveq2d 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) = ( B ( ball ` D ) ( ( F ` A ) - ( A D B ) ) ) )
7 simpll 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> D e. ( *Met ` X ) )
8 7 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> D e. ( *Met ` X ) )
9 simprr 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> B e. X )
10 9 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> B e. X )
11 simprl 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> A e. X )
12 11 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> A e. X )
13 2 3 resubcld 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( ( F ` A ) - ( A D B ) ) e. RR )
14 3 leidd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( A D B ) <_ ( A D B ) )
15 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) )
16 7 11 9 15 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( A D B ) = ( B D A ) )
17 16 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( A D B ) = ( B D A ) )
18 17 eqcomd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( B D A ) = ( A D B ) )
19 2 recnd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( F ` A ) e. CC )
20 3 recnd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( A D B ) e. CC )
21 19 20 nncand 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( ( F ` A ) - ( ( F ` A ) - ( A D B ) ) ) = ( A D B ) )
22 14 18 21 3brtr4d 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( B D A ) <_ ( ( F ` A ) - ( ( F ` A ) - ( A D B ) ) ) )
23 blss2 
 |-  ( ( ( D e. ( *Met ` X ) /\ B e. X /\ A e. X ) /\ ( ( ( F ` A ) - ( A D B ) ) e. RR /\ ( F ` A ) e. RR /\ ( B D A ) <_ ( ( F ` A ) - ( ( F ` A ) - ( A D B ) ) ) ) ) -> ( B ( ball ` D ) ( ( F ` A ) - ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) )
24 8 10 12 13 2 22 23 syl33anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( B ( ball ` D ) ( ( F ` A ) - ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) )
25 6 24 eqsstrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) )
26 25 expr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( ( F ` A ) e. RR -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) ) )
27 7 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> D e. ( *Met ` X ) )
28 9 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> B e. X )
29 1 metdsf 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) )
30 29 adantr 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> F : X --> ( 0 [,] +oo ) )
31 30 11 ffvelrnd 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) e. ( 0 [,] +oo ) )
32 eliccxr 
 |-  ( ( F ` A ) e. ( 0 [,] +oo ) -> ( F ` A ) e. RR* )
33 31 32 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) e. RR* )
34 33 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( F ` A ) e. RR* )
35 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
36 7 11 9 35 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( A D B ) e. RR* )
37 36 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( A D B ) e. RR* )
38 37 xnegcld 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> -e ( A D B ) e. RR* )
39 34 38 xaddcld 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( ( F ` A ) +e -e ( A D B ) ) e. RR* )
40 39 adantrr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( ( F ` A ) +e -e ( A D B ) ) e. RR* )
41 pnfxr 
 |-  +oo e. RR*
42 41 a1i 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> +oo e. RR* )
43 pnfge 
 |-  ( ( ( F ` A ) +e -e ( A D B ) ) e. RR* -> ( ( F ` A ) +e -e ( A D B ) ) <_ +oo )
44 40 43 syl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( ( F ` A ) +e -e ( A D B ) ) <_ +oo )
45 ssbl 
 |-  ( ( ( D e. ( *Met ` X ) /\ B e. X ) /\ ( ( ( F ` A ) +e -e ( A D B ) ) e. RR* /\ +oo e. RR* ) /\ ( ( F ` A ) +e -e ( A D B ) ) <_ +oo ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( B ( ball ` D ) +oo ) )
46 27 28 40 42 44 45 syl221anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( B ( ball ` D ) +oo ) )
47 simprr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( F ` A ) = +oo )
48 47 oveq2d 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( A ( ball ` D ) ( F ` A ) ) = ( A ( ball ` D ) +oo ) )
49 11 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> A e. X )
50 simprl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( A D B ) e. RR )
51 xblpnf 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X ) -> ( B e. ( A ( ball ` D ) +oo ) <-> ( B e. X /\ ( A D B ) e. RR ) ) )
52 27 49 51 syl2anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( B e. ( A ( ball ` D ) +oo ) <-> ( B e. X /\ ( A D B ) e. RR ) ) )
53 28 50 52 mpbir2and 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> B e. ( A ( ball ` D ) +oo ) )
54 blpnfctr 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. ( A ( ball ` D ) +oo ) ) -> ( A ( ball ` D ) +oo ) = ( B ( ball ` D ) +oo ) )
55 27 49 53 54 syl3anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( A ( ball ` D ) +oo ) = ( B ( ball ` D ) +oo ) )
56 48 55 eqtr2d 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( B ( ball ` D ) +oo ) = ( A ( ball ` D ) ( F ` A ) ) )
57 46 56 sseqtrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) )
58 57 expr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( ( F ` A ) = +oo -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) ) )
59 elxrge0 
 |-  ( ( F ` A ) e. ( 0 [,] +oo ) <-> ( ( F ` A ) e. RR* /\ 0 <_ ( F ` A ) ) )
60 59 simprbi 
 |-  ( ( F ` A ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` A ) )
61 31 60 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> 0 <_ ( F ` A ) )
62 ge0nemnf 
 |-  ( ( ( F ` A ) e. RR* /\ 0 <_ ( F ` A ) ) -> ( F ` A ) =/= -oo )
63 33 61 62 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) =/= -oo )
64 33 63 jca 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` A ) e. RR* /\ ( F ` A ) =/= -oo ) )
65 64 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( ( F ` A ) e. RR* /\ ( F ` A ) =/= -oo ) )
66 xrnemnf 
 |-  ( ( ( F ` A ) e. RR* /\ ( F ` A ) =/= -oo ) <-> ( ( F ` A ) e. RR \/ ( F ` A ) = +oo ) )
67 65 66 sylib 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( ( F ` A ) e. RR \/ ( F ` A ) = +oo ) )
68 26 58 67 mpjaod 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) )
69 pnfnlt 
 |-  ( ( F ` A ) e. RR* -> -. +oo < ( F ` A ) )
70 33 69 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> -. +oo < ( F ` A ) )
71 70 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) = +oo ) -> -. +oo < ( F ` A ) )
72 36 xnegcld 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> -e ( A D B ) e. RR* )
73 33 72 xaddcld 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` A ) +e -e ( A D B ) ) e. RR* )
74 xbln0 
 |-  ( ( D e. ( *Met ` X ) /\ B e. X /\ ( ( F ` A ) +e -e ( A D B ) ) e. RR* ) -> ( ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) =/= (/) <-> 0 < ( ( F ` A ) +e -e ( A D B ) ) ) )
75 7 9 73 74 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) =/= (/) <-> 0 < ( ( F ` A ) +e -e ( A D B ) ) ) )
76 xposdif 
 |-  ( ( ( A D B ) e. RR* /\ ( F ` A ) e. RR* ) -> ( ( A D B ) < ( F ` A ) <-> 0 < ( ( F ` A ) +e -e ( A D B ) ) ) )
77 36 33 76 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( A D B ) < ( F ` A ) <-> 0 < ( ( F ` A ) +e -e ( A D B ) ) ) )
78 75 77 bitr4d 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) =/= (/) <-> ( A D B ) < ( F ` A ) ) )
79 breq1 
 |-  ( ( A D B ) = +oo -> ( ( A D B ) < ( F ` A ) <-> +oo < ( F ` A ) ) )
80 78 79 sylan9bb 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) = +oo ) -> ( ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) =/= (/) <-> +oo < ( F ` A ) ) )
81 80 necon1bbid 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) = +oo ) -> ( -. +oo < ( F ` A ) <-> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) = (/) ) )
82 71 81 mpbid 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) = +oo ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) = (/) )
83 0ss 
 |-  (/) C_ ( A ( ball ` D ) ( F ` A ) )
84 82 83 eqsstrdi 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) = +oo ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) )
85 xmetge0 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )
86 7 11 9 85 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> 0 <_ ( A D B ) )
87 ge0nemnf 
 |-  ( ( ( A D B ) e. RR* /\ 0 <_ ( A D B ) ) -> ( A D B ) =/= -oo )
88 36 86 87 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( A D B ) =/= -oo )
89 36 88 jca 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( A D B ) e. RR* /\ ( A D B ) =/= -oo ) )
90 xrnemnf 
 |-  ( ( ( A D B ) e. RR* /\ ( A D B ) =/= -oo ) <-> ( ( A D B ) e. RR \/ ( A D B ) = +oo ) )
91 89 90 sylib 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( A D B ) e. RR \/ ( A D B ) = +oo ) )
92 68 84 91 mpjaodan 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) )
93 sslin 
 |-  ( ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) -> ( S i^i ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) ) C_ ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) )
94 92 93 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( S i^i ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) ) C_ ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) )
95 33 xrleidd 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) <_ ( F ` A ) )
96 simplr 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> S C_ X )
97 1 metdsge 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ ( F ` A ) e. RR* ) -> ( ( F ` A ) <_ ( F ` A ) <-> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) ) )
98 7 96 11 33 97 syl31anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` A ) <_ ( F ` A ) <-> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) ) )
99 95 98 mpbid 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) )
100 sseq0 
 |-  ( ( ( S i^i ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) ) C_ ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) /\ ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) ) -> ( S i^i ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) ) = (/) )
101 94 99 100 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( S i^i ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) ) = (/) )
102 1 metdsge 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ B e. X ) /\ ( ( F ` A ) +e -e ( A D B ) ) e. RR* ) -> ( ( ( F ` A ) +e -e ( A D B ) ) <_ ( F ` B ) <-> ( S i^i ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) ) = (/) ) )
103 7 96 9 73 102 syl31anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( ( F ` A ) +e -e ( A D B ) ) <_ ( F ` B ) <-> ( S i^i ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) ) = (/) ) )
104 101 103 mpbird 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` A ) +e -e ( A D B ) ) <_ ( F ` B ) )
105 30 9 ffvelrnd 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` B ) e. ( 0 [,] +oo ) )
106 eliccxr 
 |-  ( ( F ` B ) e. ( 0 [,] +oo ) -> ( F ` B ) e. RR* )
107 105 106 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` B ) e. RR* )
108 elxrge0 
 |-  ( ( F ` B ) e. ( 0 [,] +oo ) <-> ( ( F ` B ) e. RR* /\ 0 <_ ( F ` B ) ) )
109 108 simprbi 
 |-  ( ( F ` B ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` B ) )
110 105 109 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> 0 <_ ( F ` B ) )
111 xlesubadd 
 |-  ( ( ( ( F ` A ) e. RR* /\ ( A D B ) e. RR* /\ ( F ` B ) e. RR* ) /\ ( 0 <_ ( F ` A ) /\ ( A D B ) =/= -oo /\ 0 <_ ( F ` B ) ) ) -> ( ( ( F ` A ) +e -e ( A D B ) ) <_ ( F ` B ) <-> ( F ` A ) <_ ( ( F ` B ) +e ( A D B ) ) ) )
112 33 36 107 61 88 110 111 syl33anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( ( F ` A ) +e -e ( A D B ) ) <_ ( F ` B ) <-> ( F ` A ) <_ ( ( F ` B ) +e ( A D B ) ) ) )
113 104 112 mpbid 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) <_ ( ( F ` B ) +e ( A D B ) ) )
114 xaddcom 
 |-  ( ( ( F ` B ) e. RR* /\ ( A D B ) e. RR* ) -> ( ( F ` B ) +e ( A D B ) ) = ( ( A D B ) +e ( F ` B ) ) )
115 107 36 114 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` B ) +e ( A D B ) ) = ( ( A D B ) +e ( F ` B ) ) )
116 113 115 breqtrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) <_ ( ( A D B ) +e ( F ` B ) ) )