Metamath Proof Explorer

Theorem equivcau

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 sequences 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 equivcau 
|- ( ph -> ( Cau ` D ) C_ ( Cau ` 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. ( X ^pm CC ) ) /\ r e. RR+ ) -> r e. RR+ )
6 3 ad2antrr 
 |-  ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) -> R e. RR+ )
7 5 6 rpdivcld 
 |-  ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) -> ( r / R ) e. RR+ )
8 oveq2 
 |-  ( s = ( r / R ) -> ( ( f ` k ) ( ball ` D ) s ) = ( ( f ` k ) ( ball ` D ) ( r / R ) ) )
9 8 feq3d 
 |-  ( s = ( r / R ) -> ( ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) s ) <-> ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) )
10 9 rexbidv 
 |-  ( s = ( r / R ) -> ( E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) s ) <-> E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) )
11 10 rspcv 
 |-  ( ( r / R ) e. RR+ -> ( A. s e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) s ) -> E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) )
12 7 11 syl 
 |-  ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) -> ( A. s e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) s ) -> E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) )
13 simprr 
 |-  ( ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) /\ ( k e. ZZ /\ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) ) -> ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) )
14 elpmi 
 |-  ( f e. ( X ^pm CC ) -> ( f : dom f --> X /\ dom f C_ CC ) )
15 14 simpld 
 |-  ( f e. ( X ^pm CC ) -> f : dom f --> X )
16 15 ad3antlr 
 |-  ( ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) /\ ( k e. ZZ /\ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) ) -> f : dom f --> X )
17 resss 
 |-  ( f |` ( ZZ>= ` k ) ) C_ f
18 dmss 
 |-  ( ( f |` ( ZZ>= ` k ) ) C_ f -> dom ( f |` ( ZZ>= ` k ) ) C_ dom f )
19 17 18 ax-mp 
 |-  dom ( f |` ( ZZ>= ` k ) ) C_ dom f
20 uzid 
 |-  ( k e. ZZ -> k e. ( ZZ>= ` k ) )
21 20 ad2antrl 
 |-  ( ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) /\ ( k e. ZZ /\ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) ) -> k e. ( ZZ>= ` k ) )
22 fdm 
 |-  ( ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) -> dom ( f |` ( ZZ>= ` k ) ) = ( ZZ>= ` k ) )
23 22 ad2antll 
 |-  ( ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) /\ ( k e. ZZ /\ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) ) -> dom ( f |` ( ZZ>= ` k ) ) = ( ZZ>= ` k ) )
24 21 23 eleqtrrd 
 |-  ( ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) /\ ( k e. ZZ /\ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) ) -> k e. dom ( f |` ( ZZ>= ` k ) ) )
25 19 24 sseldi 
 |-  ( ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) /\ ( k e. ZZ /\ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) ) -> k e. dom f )
26 16 25 ffvelrnd 
 |-  ( ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) /\ ( k e. ZZ /\ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) ) -> ( f ` k ) e. X )
27 eqid 
 |-  ( MetOpen ` C ) = ( MetOpen ` C )
28 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
29 27 28 1 2 3 4 metss2lem 
 |-  ( ( ph /\ ( x e. X /\ r e. RR+ ) ) -> ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) )
30 29 expr 
 |-  ( ( ph /\ x e. X ) -> ( r e. RR+ -> ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) ) )
31 30 ralrimiva 
 |-  ( ph -> A. x e. X ( r e. RR+ -> ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) ) )
32 31 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) /\ ( k e. ZZ /\ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) ) -> A. x e. X ( r e. RR+ -> ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) ) )
33 simplr 
 |-  ( ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) /\ ( k e. ZZ /\ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) ) -> r e. RR+ )
34 oveq1 
 |-  ( x = ( f ` k ) -> ( x ( ball ` D ) ( r / R ) ) = ( ( f ` k ) ( ball ` D ) ( r / R ) ) )
35 oveq1 
 |-  ( x = ( f ` k ) -> ( x ( ball ` C ) r ) = ( ( f ` k ) ( ball ` C ) r ) )
36 34 35 sseq12d 
 |-  ( x = ( f ` k ) -> ( ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) <-> ( ( f ` k ) ( ball ` D ) ( r / R ) ) C_ ( ( f ` k ) ( ball ` C ) r ) ) )
37 36 imbi2d 
 |-  ( x = ( f ` k ) -> ( ( r e. RR+ -> ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) ) <-> ( r e. RR+ -> ( ( f ` k ) ( ball ` D ) ( r / R ) ) C_ ( ( f ` k ) ( ball ` C ) r ) ) ) )
38 37 rspcv 
 |-  ( ( f ` k ) e. X -> ( A. x e. X ( r e. RR+ -> ( x ( ball ` D ) ( r / R ) ) C_ ( x ( ball ` C ) r ) ) -> ( r e. RR+ -> ( ( f ` k ) ( ball ` D ) ( r / R ) ) C_ ( ( f ` k ) ( ball ` C ) r ) ) ) )
39 26 32 33 38 syl3c 
 |-  ( ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) /\ ( k e. ZZ /\ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) ) -> ( ( f ` k ) ( ball ` D ) ( r / R ) ) C_ ( ( f ` k ) ( ball ` C ) r ) )
40 13 39 fssd 
 |-  ( ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) /\ ( k e. ZZ /\ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) ) ) -> ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` C ) r ) )
41 40 expr 
 |-  ( ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) /\ k e. ZZ ) -> ( ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) -> ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` C ) r ) ) )
42 41 reximdva 
 |-  ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) -> ( E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) ( r / R ) ) -> E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` C ) r ) ) )
43 12 42 syld 
 |-  ( ( ( ph /\ f e. ( X ^pm CC ) ) /\ r e. RR+ ) -> ( A. s e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) s ) -> E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` C ) r ) ) )
44 43 ralrimdva 
 |-  ( ( ph /\ f e. ( X ^pm CC ) ) -> ( A. s e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) s ) -> A. r e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` C ) r ) ) )
45 44 ss2rabdv 
 |-  ( ph -> { f e. ( X ^pm CC ) | A. s e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) s ) } C_ { f e. ( X ^pm CC ) | A. r e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` C ) r ) } )
46 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
47 caufval 
 |-  ( D e. ( *Met ` X ) -> ( Cau ` D ) = { f e. ( X ^pm CC ) | A. s e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) s ) } )
48 2 46 47 3syl 
 |-  ( ph -> ( Cau ` D ) = { f e. ( X ^pm CC ) | A. s e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) s ) } )
49 metxmet 
 |-  ( C e. ( Met ` X ) -> C e. ( *Met ` X ) )
50 caufval 
 |-  ( C e. ( *Met ` X ) -> ( Cau ` C ) = { f e. ( X ^pm CC ) | A. r e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` C ) r ) } )
51 1 49 50 3syl 
 |-  ( ph -> ( Cau ` C ) = { f e. ( X ^pm CC ) | A. r e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` C ) r ) } )
52 45 48 51 3sstr4d 
 |-  ( ph -> ( Cau ` D ) C_ ( Cau ` C ) )