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