Metamath Proof Explorer


Theorem blssps

Description: Any point P in a ball B can be centered in another ball that is a subset of B . (Contributed by NM, 31-Aug-2006) (Revised by Mario Carneiro, 24-Aug-2015) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion blssps D PsMet X B ran ball D P B x + P ball D x B

Proof

Step Hyp Ref Expression
1 blrnps D PsMet X B ran ball D y X r * B = y ball D r
2 elblps D PsMet X y X r * P y ball D r P X y D P < r
3 simpl1 D PsMet X y X r * P X D PsMet X
4 simpl2 D PsMet X y X r * P X y X
5 simpr D PsMet X y X r * P X P X
6 psmetcl D PsMet X y X P X y D P *
7 3 4 5 6 syl3anc D PsMet X y X r * P X y D P *
8 simpl3 D PsMet X y X r * P X r *
9 qbtwnxr y D P * r * y D P < r z y D P < z z < r
10 9 3expia y D P * r * y D P < r z y D P < z z < r
11 7 8 10 syl2anc D PsMet X y X r * P X y D P < r z y D P < z z < r
12 qre z z
13 simpll1 D PsMet X y X r * P X z y D P < z z < r D PsMet X
14 simplr D PsMet X y X r * P X z y D P < z z < r P X
15 simpll2 D PsMet X y X r * P X z y D P < z z < r y X
16 psmetsym D PsMet X P X y X P D y = y D P
17 13 14 15 16 syl3anc D PsMet X y X r * P X z y D P < z z < r P D y = y D P
18 simprrl D PsMet X y X r * P X z y D P < z z < r y D P < z
19 17 18 eqbrtrd D PsMet X y X r * P X z y D P < z z < r P D y < z
20 simprl D PsMet X y X r * P X z y D P < z z < r z
21 psmetcl D PsMet X P X y X P D y *
22 13 14 15 21 syl3anc D PsMet X y X r * P X z y D P < z z < r P D y *
23 rexr z z *
24 23 ad2antrl D PsMet X y X r * P X z y D P < z z < r z *
25 22 24 19 xrltled D PsMet X y X r * P X z y D P < z z < r P D y z
26 psmetlecl D PsMet X P X y X z P D y z P D y
27 13 14 15 20 25 26 syl122anc D PsMet X y X r * P X z y D P < z z < r P D y
28 difrp P D y z P D y < z z P D y +
29 27 20 28 syl2anc D PsMet X y X r * P X z y D P < z z < r P D y < z z P D y +
30 19 29 mpbid D PsMet X y X r * P X z y D P < z z < r z P D y +
31 20 27 resubcld D PsMet X y X r * P X z y D P < z z < r z P D y
32 22 xrleidd D PsMet X y X r * P X z y D P < z z < r P D y P D y
33 20 recnd D PsMet X y X r * P X z y D P < z z < r z
34 27 recnd D PsMet X y X r * P X z y D P < z z < r P D y
35 33 34 nncand D PsMet X y X r * P X z y D P < z z < r z z P D y = P D y
36 32 35 breqtrrd D PsMet X y X r * P X z y D P < z z < r P D y z z P D y
37 blss2ps D PsMet X P X y X z P D y z P D y z z P D y P ball D z P D y y ball D z
38 13 14 15 31 20 36 37 syl33anc D PsMet X y X r * P X z y D P < z z < r P ball D z P D y y ball D z
39 simpll3 D PsMet X y X r * P X z y D P < z z < r r *
40 simprrr D PsMet X y X r * P X z y D P < z z < r z < r
41 24 39 40 xrltled D PsMet X y X r * P X z y D P < z z < r z r
42 ssblps D PsMet X y X z * r * z r y ball D z y ball D r
43 13 15 24 39 41 42 syl221anc D PsMet X y X r * P X z y D P < z z < r y ball D z y ball D r
44 38 43 sstrd D PsMet X y X r * P X z y D P < z z < r P ball D z P D y y ball D r
45 oveq2 x = z P D y P ball D x = P ball D z P D y
46 45 sseq1d x = z P D y P ball D x y ball D r P ball D z P D y y ball D r
47 46 rspcev z P D y + P ball D z P D y y ball D r x + P ball D x y ball D r
48 30 44 47 syl2anc D PsMet X y X r * P X z y D P < z z < r x + P ball D x y ball D r
49 48 expr D PsMet X y X r * P X z y D P < z z < r x + P ball D x y ball D r
50 12 49 sylan2 D PsMet X y X r * P X z y D P < z z < r x + P ball D x y ball D r
51 50 rexlimdva D PsMet X y X r * P X z y D P < z z < r x + P ball D x y ball D r
52 11 51 syld D PsMet X y X r * P X y D P < r x + P ball D x y ball D r
53 52 expimpd D PsMet X y X r * P X y D P < r x + P ball D x y ball D r
54 2 53 sylbid D PsMet X y X r * P y ball D r x + P ball D x y ball D r
55 eleq2 B = y ball D r P B P y ball D r
56 sseq2 B = y ball D r P ball D x B P ball D x y ball D r
57 56 rexbidv B = y ball D r x + P ball D x B x + P ball D x y ball D r
58 55 57 imbi12d B = y ball D r P B x + P ball D x B P y ball D r x + P ball D x y ball D r
59 54 58 syl5ibrcom D PsMet X y X r * B = y ball D r P B x + P ball D x B
60 59 3expib D PsMet X y X r * B = y ball D r P B x + P ball D x B
61 60 rexlimdvv D PsMet X y X r * B = y ball D r P B x + P ball D x B
62 1 61 sylbid D PsMet X B ran ball D P B x + P ball D x B
63 62 3imp D PsMet X B ran ball D P B x + P ball D x B