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 e. ( PsMet ` X ) /\ B e. ran ( ball ` D ) /\ P e. B ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ B )

Proof

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