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