Metamath Proof Explorer

Theorem metss2lem

Description: Lemma for metss2 . (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypotheses metequiv.3 
|- J = ( MetOpen ` C )
metequiv.4 
|- K = ( MetOpen ` D )
metss2.1 
|- ( ph -> C e. ( Met ` X ) )
metss2.2 
|- ( ph -> D e. ( Met ` X ) )
metss2.3 
|- ( ph -> R e. RR+ )
metss2.4 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x C y ) <_ ( R x. ( x D y ) ) )
Assertion metss2lem 
|- ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> ( x ( ball ` D ) ( S / R ) ) C_ ( x ( ball ` C ) S ) )

Proof

Step Hyp Ref Expression
1 metequiv.3 
 |-  J = ( MetOpen ` C )
2 metequiv.4 
 |-  K = ( MetOpen ` D )
3 metss2.1 
 |-  ( ph -> C e. ( Met ` X ) )
4 metss2.2 
 |-  ( ph -> D e. ( Met ` X ) )
5 metss2.3 
 |-  ( ph -> R e. RR+ )
6 metss2.4 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x C y ) <_ ( R x. ( x D y ) ) )
7 4 ad2antrr 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> D e. ( Met ` X ) )
8 simplrl 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> x e. X )
9 simpr 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> y e. X )
10 metcl 
 |-  ( ( D e. ( Met ` X ) /\ x e. X /\ y e. X ) -> ( x D y ) e. RR )
11 7 8 9 10 syl3anc 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( x D y ) e. RR )
12 simplrr 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> S e. RR+ )
13 12 rpred 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> S e. RR )
14 5 ad2antrr 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> R e. RR+ )
15 11 13 14 ltmuldiv2d 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( ( R x. ( x D y ) ) < S <-> ( x D y ) < ( S / R ) ) )
16 6 anassrs 
 |-  ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( x C y ) <_ ( R x. ( x D y ) ) )
17 16 adantlrr 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( x C y ) <_ ( R x. ( x D y ) ) )
18 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> C e. ( Met ` X ) )
19 metcl 
 |-  ( ( C e. ( Met ` X ) /\ x e. X /\ y e. X ) -> ( x C y ) e. RR )
20 18 8 9 19 syl3anc 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( x C y ) e. RR )
21 14 rpred 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> R e. RR )
22 21 11 remulcld 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( R x. ( x D y ) ) e. RR )
23 lelttr 
 |-  ( ( ( x C y ) e. RR /\ ( R x. ( x D y ) ) e. RR /\ S e. RR ) -> ( ( ( x C y ) <_ ( R x. ( x D y ) ) /\ ( R x. ( x D y ) ) < S ) -> ( x C y ) < S ) )
24 20 22 13 23 syl3anc 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( ( ( x C y ) <_ ( R x. ( x D y ) ) /\ ( R x. ( x D y ) ) < S ) -> ( x C y ) < S ) )
25 17 24 mpand 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( ( R x. ( x D y ) ) < S -> ( x C y ) < S ) )
26 15 25 sylbird 
 |-  ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( ( x D y ) < ( S / R ) -> ( x C y ) < S ) )
27 26 ss2rabdv 
 |-  ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> { y e. X | ( x D y ) < ( S / R ) } C_ { y e. X | ( x C y ) < S } )
28 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
29 4 28 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
30 29 adantr 
 |-  ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> D e. ( *Met ` X ) )
31 simprl 
 |-  ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> x e. X )
32 simpr 
 |-  ( ( x e. X /\ S e. RR+ ) -> S e. RR+ )
33 rpdivcl 
 |-  ( ( S e. RR+ /\ R e. RR+ ) -> ( S / R ) e. RR+ )
34 32 5 33 syl2anr 
 |-  ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> ( S / R ) e. RR+ )
35 34 rpxrd 
 |-  ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> ( S / R ) e. RR* )
36 blval 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ ( S / R ) e. RR* ) -> ( x ( ball ` D ) ( S / R ) ) = { y e. X | ( x D y ) < ( S / R ) } )
37 30 31 35 36 syl3anc 
 |-  ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> ( x ( ball ` D ) ( S / R ) ) = { y e. X | ( x D y ) < ( S / R ) } )
38 metxmet 
 |-  ( C e. ( Met ` X ) -> C e. ( *Met ` X ) )
39 3 38 syl 
 |-  ( ph -> C e. ( *Met ` X ) )
40 39 adantr 
 |-  ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> C e. ( *Met ` X ) )
41 rpxr 
 |-  ( S e. RR+ -> S e. RR* )
42 41 ad2antll 
 |-  ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> S e. RR* )
43 blval 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ S e. RR* ) -> ( x ( ball ` C ) S ) = { y e. X | ( x C y ) < S } )
44 40 31 42 43 syl3anc 
 |-  ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> ( x ( ball ` C ) S ) = { y e. X | ( x C y ) < S } )
45 27 37 44 3sstr4d 
 |-  ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> ( x ( ball ` D ) ( S / R ) ) C_ ( x ( ball ` C ) S ) )