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

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