This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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