Metamath Proof Explorer


Theorem xblss2

Description: One ball is contained in another if the center-to-center distance is less than the difference of the radii. In this version of blss2 for extended metrics, we have to assume the balls are a finite distance apart, or else P will not even be in the infinity ball around Q . (Contributed by Mario Carneiro, 23-Aug-2015)

Ref Expression
Hypotheses xblss2.1
|- ( ph -> D e. ( *Met ` X ) )
xblss2.2
|- ( ph -> P e. X )
xblss2.3
|- ( ph -> Q e. X )
xblss2.4
|- ( ph -> R e. RR* )
xblss2.5
|- ( ph -> S e. RR* )
xblss2.6
|- ( ph -> ( P D Q ) e. RR )
xblss2.7
|- ( ph -> ( P D Q ) <_ ( S +e -e R ) )
Assertion xblss2
|- ( ph -> ( P ( ball ` D ) R ) C_ ( Q ( ball ` D ) S ) )

Proof

Step Hyp Ref Expression
1 xblss2.1
 |-  ( ph -> D e. ( *Met ` X ) )
2 xblss2.2
 |-  ( ph -> P e. X )
3 xblss2.3
 |-  ( ph -> Q e. X )
4 xblss2.4
 |-  ( ph -> R e. RR* )
5 xblss2.5
 |-  ( ph -> S e. RR* )
6 xblss2.6
 |-  ( ph -> ( P D Q ) e. RR )
7 xblss2.7
 |-  ( ph -> ( P D Q ) <_ ( S +e -e R ) )
8 elbl
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) )
9 1 2 4 8 syl3anc
 |-  ( ph -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) )
10 9 simprbda
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> x e. X )
11 1 adantr
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> D e. ( *Met ` X ) )
12 3 adantr
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> Q e. X )
13 xmetcl
 |-  ( ( D e. ( *Met ` X ) /\ Q e. X /\ x e. X ) -> ( Q D x ) e. RR* )
14 11 12 10 13 syl3anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( Q D x ) e. RR* )
15 14 adantr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R e. RR ) -> ( Q D x ) e. RR* )
16 6 adantr
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( P D Q ) e. RR )
17 16 rexrd
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( P D Q ) e. RR* )
18 4 adantr
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> R e. RR* )
19 17 18 xaddcld
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( ( P D Q ) +e R ) e. RR* )
20 19 adantr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R e. RR ) -> ( ( P D Q ) +e R ) e. RR* )
21 5 ad2antrr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R e. RR ) -> S e. RR* )
22 2 adantr
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> P e. X )
23 xmetcl
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. X ) -> ( P D x ) e. RR* )
24 11 22 10 23 syl3anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( P D x ) e. RR* )
25 17 24 xaddcld
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( ( P D Q ) +e ( P D x ) ) e. RR* )
26 xmettri2
 |-  ( ( D e. ( *Met ` X ) /\ ( P e. X /\ Q e. X /\ x e. X ) ) -> ( Q D x ) <_ ( ( P D Q ) +e ( P D x ) ) )
27 11 22 12 10 26 syl13anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( Q D x ) <_ ( ( P D Q ) +e ( P D x ) ) )
28 9 simplbda
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( P D x ) < R )
29 xltadd2
 |-  ( ( ( P D x ) e. RR* /\ R e. RR* /\ ( P D Q ) e. RR ) -> ( ( P D x ) < R <-> ( ( P D Q ) +e ( P D x ) ) < ( ( P D Q ) +e R ) ) )
30 24 18 16 29 syl3anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( ( P D x ) < R <-> ( ( P D Q ) +e ( P D x ) ) < ( ( P D Q ) +e R ) ) )
31 28 30 mpbid
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( ( P D Q ) +e ( P D x ) ) < ( ( P D Q ) +e R ) )
32 14 25 19 27 31 xrlelttrd
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( Q D x ) < ( ( P D Q ) +e R ) )
33 32 adantr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R e. RR ) -> ( Q D x ) < ( ( P D Q ) +e R ) )
34 5 adantr
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> S e. RR* )
35 18 xnegcld
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> -e R e. RR* )
36 34 35 xaddcld
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( S +e -e R ) e. RR* )
37 7 adantr
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( P D Q ) <_ ( S +e -e R ) )
38 xleadd1a
 |-  ( ( ( ( P D Q ) e. RR* /\ ( S +e -e R ) e. RR* /\ R e. RR* ) /\ ( P D Q ) <_ ( S +e -e R ) ) -> ( ( P D Q ) +e R ) <_ ( ( S +e -e R ) +e R ) )
39 17 36 18 37 38 syl31anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( ( P D Q ) +e R ) <_ ( ( S +e -e R ) +e R ) )
40 39 adantr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R e. RR ) -> ( ( P D Q ) +e R ) <_ ( ( S +e -e R ) +e R ) )
41 xnpcan
 |-  ( ( S e. RR* /\ R e. RR ) -> ( ( S +e -e R ) +e R ) = S )
42 34 41 sylan
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R e. RR ) -> ( ( S +e -e R ) +e R ) = S )
43 40 42 breqtrd
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R e. RR ) -> ( ( P D Q ) +e R ) <_ S )
44 15 20 21 33 43 xrltletrd
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R e. RR ) -> ( Q D x ) < S )
45 28 adantr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( P D x ) < R )
46 7 ad2antrr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( P D Q ) <_ ( S +e -e R ) )
47 0xr
 |-  0 e. RR*
48 47 a1i
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> 0 e. RR* )
49 xmetge0
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) -> 0 <_ ( P D Q ) )
50 11 22 12 49 syl3anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> 0 <_ ( P D Q ) )
51 48 17 36 50 37 xrletrd
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> 0 <_ ( S +e -e R ) )
52 ge0nemnf
 |-  ( ( ( S +e -e R ) e. RR* /\ 0 <_ ( S +e -e R ) ) -> ( S +e -e R ) =/= -oo )
53 36 51 52 syl2anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( S +e -e R ) =/= -oo )
54 53 adantr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( S +e -e R ) =/= -oo )
55 5 ad2antrr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> S e. RR* )
56 xaddmnf1
 |-  ( ( S e. RR* /\ S =/= +oo ) -> ( S +e -oo ) = -oo )
57 56 ex
 |-  ( S e. RR* -> ( S =/= +oo -> ( S +e -oo ) = -oo ) )
58 55 57 syl
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( S =/= +oo -> ( S +e -oo ) = -oo ) )
59 simpr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> R = +oo )
60 xnegeq
 |-  ( R = +oo -> -e R = -e +oo )
61 59 60 syl
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> -e R = -e +oo )
62 xnegpnf
 |-  -e +oo = -oo
63 61 62 eqtrdi
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> -e R = -oo )
64 63 oveq2d
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( S +e -e R ) = ( S +e -oo ) )
65 64 eqeq1d
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( ( S +e -e R ) = -oo <-> ( S +e -oo ) = -oo ) )
66 58 65 sylibrd
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( S =/= +oo -> ( S +e -e R ) = -oo ) )
67 66 necon1d
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( ( S +e -e R ) =/= -oo -> S = +oo ) )
68 54 67 mpd
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> S = +oo )
69 68 63 oveq12d
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( S +e -e R ) = ( +oo +e -oo ) )
70 pnfaddmnf
 |-  ( +oo +e -oo ) = 0
71 69 70 eqtrdi
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( S +e -e R ) = 0 )
72 46 71 breqtrd
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( P D Q ) <_ 0 )
73 50 biantrud
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( ( P D Q ) <_ 0 <-> ( ( P D Q ) <_ 0 /\ 0 <_ ( P D Q ) ) ) )
74 xrletri3
 |-  ( ( ( P D Q ) e. RR* /\ 0 e. RR* ) -> ( ( P D Q ) = 0 <-> ( ( P D Q ) <_ 0 /\ 0 <_ ( P D Q ) ) ) )
75 17 47 74 sylancl
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( ( P D Q ) = 0 <-> ( ( P D Q ) <_ 0 /\ 0 <_ ( P D Q ) ) ) )
76 xmeteq0
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) -> ( ( P D Q ) = 0 <-> P = Q ) )
77 11 22 12 76 syl3anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( ( P D Q ) = 0 <-> P = Q ) )
78 73 75 77 3bitr2d
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( ( P D Q ) <_ 0 <-> P = Q ) )
79 78 adantr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( ( P D Q ) <_ 0 <-> P = Q ) )
80 72 79 mpbid
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> P = Q )
81 80 oveq1d
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( P D x ) = ( Q D x ) )
82 59 68 eqtr4d
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> R = S )
83 45 81 82 3brtr3d
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( Q D x ) < S )
84 xmetge0
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. X ) -> 0 <_ ( P D x ) )
85 11 22 10 84 syl3anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> 0 <_ ( P D x ) )
86 48 24 18 85 28 xrlelttrd
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> 0 < R )
87 48 18 86 xrltled
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> 0 <_ R )
88 ge0nemnf
 |-  ( ( R e. RR* /\ 0 <_ R ) -> R =/= -oo )
89 18 87 88 syl2anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> R =/= -oo )
90 18 89 jca
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( R e. RR* /\ R =/= -oo ) )
91 xrnemnf
 |-  ( ( R e. RR* /\ R =/= -oo ) <-> ( R e. RR \/ R = +oo ) )
92 90 91 sylib
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( R e. RR \/ R = +oo ) )
93 44 83 92 mpjaodan
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( Q D x ) < S )
94 elbl
 |-  ( ( D e. ( *Met ` X ) /\ Q e. X /\ S e. RR* ) -> ( x e. ( Q ( ball ` D ) S ) <-> ( x e. X /\ ( Q D x ) < S ) ) )
95 11 12 34 94 syl3anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( x e. ( Q ( ball ` D ) S ) <-> ( x e. X /\ ( Q D x ) < S ) ) )
96 10 93 95 mpbir2and
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> x e. ( Q ( ball ` D ) S ) )
97 96 ex
 |-  ( ph -> ( x e. ( P ( ball ` D ) R ) -> x e. ( Q ( ball ` D ) S ) ) )
98 97 ssrdv
 |-  ( ph -> ( P ( ball ` D ) R ) C_ ( Q ( ball ` D ) S ) )