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 ) ) )