Metamath Proof Explorer

Theorem metss2

Description: If the metric D is "strongly finer" than C (meaning that there is a positive real constant R such that C ( x , y ) <_ R x. D ( x , y ) ), then D generates a finer topology. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they generate the same topology.) (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 metss2 
|- ( ph -> J C_ K )

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 simpr 
 |-  ( ( x e. X /\ r e. RR+ ) -> r e. RR+ )
8 rpdivcl 
 |-  ( ( r e. RR+ /\ R e. RR+ ) -> ( r / R ) e. RR+ )
9 7 5 8 syl2anr 
 |-  ( ( ph /\ ( x e. X /\ r e. RR+ ) ) -> ( r / R ) e. RR+ )
10 1 2 3 4 5 6 metss2lem 
 |-  ( ( ph /\ ( x e. X /\ r e. RR+ ) ) -> ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) )
11 oveq2 
 |-  ( s = ( r / R ) -> ( x ( ball ` D ) s ) = ( x ( ball ` D ) ( r / R ) ) )
12 11 sseq1d 
 |-  ( s = ( r / R ) -> ( ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) <-> ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) ) )
13 12 rspcev 
 |-  ( ( ( r / R ) e. RR+ /\ ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) ) -> E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) )
14 9 10 13 syl2anc 
 |-  ( ( ph /\ ( x e. X /\ r e. RR+ ) ) -> E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) )
15 14 ralrimivva 
 |-  ( ph -> A. x e. X A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) )
16 metxmet 
 |-  ( C e. ( Met ` X ) -> C e. ( *Met ` X ) )
17 3 16 syl 
 |-  ( ph -> C e. ( *Met ` X ) )
18 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
19 4 18 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
20 1 2 metss 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( J C_ K <-> A. x e. X A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )
21 17 19 20 syl2anc 
 |-  ( ph -> ( J C_ K <-> A. x e. X A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )
22 15 21 mpbird 
 |-  ( ph -> J C_ K )