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 )