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