Metamath Proof Explorer


Theorem xblss2ps

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) (Revised by Thierry Arnoux, 11-Mar-2018)

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

Proof

Step Hyp Ref Expression
1 xblss2ps.1
 |-  ( ph -> D e. ( PsMet ` X ) )
2 xblss2ps.2
 |-  ( ph -> P e. X )
3 xblss2ps.3
 |-  ( ph -> Q e. X )
4 xblss2ps.4
 |-  ( ph -> R e. RR* )
5 xblss2ps.5
 |-  ( ph -> S e. RR* )
6 xblss2ps.6
 |-  ( ph -> ( P D Q ) e. RR )
7 xblss2ps.7
 |-  ( ph -> ( P D Q ) <_ ( S +e -e R ) )
8 elblps
 |-  ( ( D e. ( PsMet ` 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. ( PsMet ` X ) )
12 3 adantr
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> Q e. X )
13 psmetcl
 |-  ( ( D e. ( PsMet ` 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 psmetcl
 |-  ( ( D e. ( PsMet ` 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 psmettri2
 |-  ( ( D e. ( PsMet ` 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 14 adantr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( Q D x ) e. RR* )
46 6 ad2antrr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( P D Q ) e. RR )
47 simpll
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ph )
48 simplr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> x e. ( P ( ball ` D ) R ) )
49 simpr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> R = +oo )
50 49 oveq2d
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( P ( ball ` D ) R ) = ( P ( ball ` D ) +oo ) )
51 48 50 eleqtrd
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> x e. ( P ( ball ` D ) +oo ) )
52 xblpnfps
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X ) -> ( x e. ( P ( ball ` D ) +oo ) <-> ( x e. X /\ ( P D x ) e. RR ) ) )
53 1 2 52 syl2anc
 |-  ( ph -> ( x e. ( P ( ball ` D ) +oo ) <-> ( x e. X /\ ( P D x ) e. RR ) ) )
54 53 simplbda
 |-  ( ( ph /\ x e. ( P ( ball ` D ) +oo ) ) -> ( P D x ) e. RR )
55 47 51 54 syl2anc
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( P D x ) e. RR )
56 46 55 readdcld
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( ( P D Q ) + ( P D x ) ) e. RR )
57 56 rexrd
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( ( P D Q ) + ( P D x ) ) e. RR* )
58 pnfxr
 |-  +oo e. RR*
59 58 a1i
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> +oo e. RR* )
60 1 ad2antrr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> D e. ( PsMet ` X ) )
61 2 ad2antrr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> P e. X )
62 3 ad2antrr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> Q e. X )
63 10 adantr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> x e. X )
64 60 61 62 63 26 syl13anc
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( Q D x ) <_ ( ( P D Q ) +e ( P D x ) ) )
65 46 55 rexaddd
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( ( P D Q ) +e ( P D x ) ) = ( ( P D Q ) + ( P D x ) ) )
66 64 65 breqtrd
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( Q D x ) <_ ( ( P D Q ) + ( P D x ) ) )
67 56 ltpnfd
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( ( P D Q ) + ( P D x ) ) < +oo )
68 45 57 59 66 67 xrlelttrd
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( Q D x ) < +oo )
69 0xr
 |-  0 e. RR*
70 69 a1i
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> 0 e. RR* )
71 psmetge0
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) -> 0 <_ ( P D Q ) )
72 11 22 12 71 syl3anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> 0 <_ ( P D Q ) )
73 70 17 36 72 37 xrletrd
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> 0 <_ ( S +e -e R ) )
74 ge0nemnf
 |-  ( ( ( S +e -e R ) e. RR* /\ 0 <_ ( S +e -e R ) ) -> ( S +e -e R ) =/= -oo )
75 36 73 74 syl2anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( S +e -e R ) =/= -oo )
76 75 adantr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( S +e -e R ) =/= -oo )
77 5 ad2antrr
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> S e. RR* )
78 xaddmnf1
 |-  ( ( S e. RR* /\ S =/= +oo ) -> ( S +e -oo ) = -oo )
79 78 ex
 |-  ( S e. RR* -> ( S =/= +oo -> ( S +e -oo ) = -oo ) )
80 77 79 syl
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( S =/= +oo -> ( S +e -oo ) = -oo ) )
81 xnegeq
 |-  ( R = +oo -> -e R = -e +oo )
82 49 81 syl
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> -e R = -e +oo )
83 xnegpnf
 |-  -e +oo = -oo
84 82 83 eqtrdi
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> -e R = -oo )
85 84 oveq2d
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( S +e -e R ) = ( S +e -oo ) )
86 85 eqeq1d
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( ( S +e -e R ) = -oo <-> ( S +e -oo ) = -oo ) )
87 80 86 sylibrd
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( S =/= +oo -> ( S +e -e R ) = -oo ) )
88 87 necon1d
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( ( S +e -e R ) =/= -oo -> S = +oo ) )
89 76 88 mpd
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> S = +oo )
90 68 89 breqtrrd
 |-  ( ( ( ph /\ x e. ( P ( ball ` D ) R ) ) /\ R = +oo ) -> ( Q D x ) < S )
91 psmetge0
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X /\ x e. X ) -> 0 <_ ( P D x ) )
92 11 22 10 91 syl3anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> 0 <_ ( P D x ) )
93 70 24 18 92 28 xrlelttrd
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> 0 < R )
94 70 18 93 xrltled
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> 0 <_ R )
95 ge0nemnf
 |-  ( ( R e. RR* /\ 0 <_ R ) -> R =/= -oo )
96 18 94 95 syl2anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> R =/= -oo )
97 18 96 jca
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( R e. RR* /\ R =/= -oo ) )
98 xrnemnf
 |-  ( ( R e. RR* /\ R =/= -oo ) <-> ( R e. RR \/ R = +oo ) )
99 97 98 sylib
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( R e. RR \/ R = +oo ) )
100 44 90 99 mpjaodan
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( Q D x ) < S )
101 elblps
 |-  ( ( D e. ( PsMet ` X ) /\ Q e. X /\ S e. RR* ) -> ( x e. ( Q ( ball ` D ) S ) <-> ( x e. X /\ ( Q D x ) < S ) ) )
102 11 12 34 101 syl3anc
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> ( x e. ( Q ( ball ` D ) S ) <-> ( x e. X /\ ( Q D x ) < S ) ) )
103 10 100 102 mpbir2and
 |-  ( ( ph /\ x e. ( P ( ball ` D ) R ) ) -> x e. ( Q ( ball ` D ) S ) )
104 103 ex
 |-  ( ph -> ( x e. ( P ( ball ` D ) R ) -> x e. ( Q ( ball ` D ) S ) ) )
105 104 ssrdv
 |-  ( ph -> ( P ( ball ` D ) R ) C_ ( Q ( ball ` D ) S ) )