Metamath Proof Explorer

Theorem equivcfil

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 ) ), all the D -Cauchy filters are also C -Cauchy. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they have the same Cauchy sequences.) (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypotheses equivcau.1 
|- ( ph -> C e. ( Met ` X ) )
equivcau.2 
|- ( ph -> D e. ( Met ` X ) )
equivcau.3 
|- ( ph -> R e. RR+ )
equivcau.4 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x C y ) <_ ( R x. ( x D y ) ) )
Assertion equivcfil 
|- ( ph -> ( CauFil ` D ) C_ ( CauFil ` C ) )

Proof

Step Hyp Ref Expression
1 equivcau.1 
 |-  ( ph -> C e. ( Met ` X ) )
2 equivcau.2 
 |-  ( ph -> D e. ( Met ` X ) )
3 equivcau.3 
 |-  ( ph -> R e. RR+ )
4 equivcau.4 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x C y ) <_ ( R x. ( x D y ) ) )
5 simpr 
 |-  ( ( ( ph /\ f e. ( Fil ` X ) ) /\ r e. RR+ ) -> r e. RR+ )
6 3 ad2antrr 
 |-  ( ( ( ph /\ f e. ( Fil ` X ) ) /\ r e. RR+ ) -> R e. RR+ )
7 5 6 rpdivcld 
 |-  ( ( ( ph /\ f e. ( Fil ` X ) ) /\ r e. RR+ ) -> ( r / R ) e. RR+ )
8 oveq2 
 |-  ( s = ( r / R ) -> ( x ( ball ` D ) s ) = ( x ( ball ` D ) ( r / R ) ) )
9 8 eleq1d 
 |-  ( s = ( r / R ) -> ( ( x ( ball ` D ) s ) e. f <-> ( x ( ball ` D ) ( r / R ) ) e. f ) )
10 9 rexbidv 
 |-  ( s = ( r / R ) -> ( E. x e. X ( x ( ball ` D ) s ) e. f <-> E. x e. X ( x ( ball ` D ) ( r / R ) ) e. f ) )
11 10 rspcv 
 |-  ( ( r / R ) e. RR+ -> ( A. s e. RR+ E. x e. X ( x ( ball ` D ) s ) e. f -> E. x e. X ( x ( ball ` D ) ( r / R ) ) e. f ) )
12 7 11 syl 
 |-  ( ( ( ph /\ f e. ( Fil ` X ) ) /\ r e. RR+ ) -> ( A. s e. RR+ E. x e. X ( x ( ball ` D ) s ) e. f -> E. x e. X ( x ( ball ` D ) ( r / R ) ) e. f ) )
13 simpllr 
 |-  ( ( ( ( ph /\ f e. ( Fil ` X ) ) /\ r e. RR+ ) /\ x e. X ) -> f e. ( Fil ` X ) )
14 eqid 
 |-  ( MetOpen ` C ) = ( MetOpen ` C )
15 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
16 14 15 1 2 3 4 metss2lem 
 |-  ( ( ph /\ ( x e. X /\ r e. RR+ ) ) -> ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) )
17 16 ancom2s 
 |-  ( ( ph /\ ( r e. RR+ /\ x e. X ) ) -> ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) )
18 17 adantlr 
 |-  ( ( ( ph /\ f e. ( Fil ` X ) ) /\ ( r e. RR+ /\ x e. X ) ) -> ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) )
19 18 anassrs 
 |-  ( ( ( ( ph /\ f e. ( Fil ` X ) ) /\ r e. RR+ ) /\ x e. X ) -> ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) )
20 1 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( Fil ` X ) ) /\ r e. RR+ ) /\ x e. X ) -> C e. ( Met ` X ) )
21 metxmet 
 |-  ( C e. ( Met ` X ) -> C e. ( *Met ` X ) )
22 20 21 syl 
 |-  ( ( ( ( ph /\ f e. ( Fil ` X ) ) /\ r e. RR+ ) /\ x e. X ) -> C e. ( *Met ` X ) )
23 simpr 
 |-  ( ( ( ( ph /\ f e. ( Fil ` X ) ) /\ r e. RR+ ) /\ x e. X ) -> x e. X )
24 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
25 24 ad2antlr 
 |-  ( ( ( ( ph /\ f e. ( Fil ` X ) ) /\ r e. RR+ ) /\ x e. X ) -> r e. RR* )
26 blssm 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ r e. RR* ) -> ( x ( ball ` C ) r ) C_ X )
27 22 23 25 26 syl3anc 
 |-  ( ( ( ( ph /\ f e. ( Fil ` X ) ) /\ r e. RR+ ) /\ x e. X ) -> ( x ( ball ` C ) r ) C_ X )
28 filss 
 |-  ( ( f e. ( Fil ` X ) /\ ( ( x ( ball ` D ) ( r / R ) ) e. f /\ ( x ( ball ` C ) r ) C_ X /\ ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) ) ) -> ( x ( ball ` C ) r ) e. f )
29 28 3exp2 
 |-  ( f e. ( Fil ` X ) -> ( ( x ( ball ` D ) ( r / R ) ) e. f -> ( ( x ( ball ` C ) r ) C_ X -> ( ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) -> ( x ( ball ` C ) r ) e. f ) ) ) )
30 29 com24 
 |-  ( f e. ( Fil ` X ) -> ( ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) -> ( ( x ( ball ` C ) r ) C_ X -> ( ( x ( ball ` D ) ( r / R ) ) e. f -> ( x ( ball ` C ) r ) e. f ) ) ) )
31 13 19 27 30 syl3c 
 |-  ( ( ( ( ph /\ f e. ( Fil ` X ) ) /\ r e. RR+ ) /\ x e. X ) -> ( ( x ( ball ` D ) ( r / R ) ) e. f -> ( x ( ball ` C ) r ) e. f ) )
32 31 reximdva 
 |-  ( ( ( ph /\ f e. ( Fil ` X ) ) /\ r e. RR+ ) -> ( E. x e. X ( x ( ball ` D ) ( r / R ) ) e. f -> E. x e. X ( x ( ball ` C ) r ) e. f ) )
33 12 32 syld 
 |-  ( ( ( ph /\ f e. ( Fil ` X ) ) /\ r e. RR+ ) -> ( A. s e. RR+ E. x e. X ( x ( ball ` D ) s ) e. f -> E. x e. X ( x ( ball ` C ) r ) e. f ) )
34 33 ralrimdva 
 |-  ( ( ph /\ f e. ( Fil ` X ) ) -> ( A. s e. RR+ E. x e. X ( x ( ball ` D ) s ) e. f -> A. r e. RR+ E. x e. X ( x ( ball ` C ) r ) e. f ) )
35 34 imdistanda 
 |-  ( ph -> ( ( f e. ( Fil ` X ) /\ A. s e. RR+ E. x e. X ( x ( ball ` D ) s ) e. f ) -> ( f e. ( Fil ` X ) /\ A. r e. RR+ E. x e. X ( x ( ball ` C ) r ) e. f ) ) )
36 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
37 iscfil3 
 |-  ( D e. ( *Met ` X ) -> ( f e. ( CauFil ` D ) <-> ( f e. ( Fil ` X ) /\ A. s e. RR+ E. x e. X ( x ( ball ` D ) s ) e. f ) ) )
38 2 36 37 3syl 
 |-  ( ph -> ( f e. ( CauFil ` D ) <-> ( f e. ( Fil ` X ) /\ A. s e. RR+ E. x e. X ( x ( ball ` D ) s ) e. f ) ) )
39 iscfil3 
 |-  ( C e. ( *Met ` X ) -> ( f e. ( CauFil ` C ) <-> ( f e. ( Fil ` X ) /\ A. r e. RR+ E. x e. X ( x ( ball ` C ) r ) e. f ) ) )
40 1 21 39 3syl 
 |-  ( ph -> ( f e. ( CauFil ` C ) <-> ( f e. ( Fil ` X ) /\ A. r e. RR+ E. x e. X ( x ( ball ` C ) r ) e. f ) ) )
41 35 38 40 3imtr4d 
 |-  ( ph -> ( f e. ( CauFil ` D ) -> f e. ( CauFil ` C ) ) )
42 41 ssrdv 
 |-  ( ph -> ( CauFil ` D ) C_ ( CauFil ` C ) )