Metamath Proof Explorer

Theorem equivcmet

Description: If two metrics are strongly equivalent, one is complete iff the other is. Unlike equivcau , metss2 , this theorem does not have a one-directional form - it is possible for a metric C that is strongly finer than the complete metric D to be incomplete and vice versa. Consider D = the metric on RR induced by the usual homeomorphism from ( 0 , 1 ) against the usual metric C on RR and against the discrete metric E on RR . Then both C and E are complete but D is not, and C is strongly finer than D , which is strongly finer than E . (Contributed by Mario Carneiro, 15-Sep-2015)

Ref Expression
Hypotheses equivcmet.1 
|- ( ph -> C e. ( Met ` X ) )
equivcmet.2 
|- ( ph -> D e. ( Met ` X ) )
equivcmet.3 
|- ( ph -> R e. RR+ )
equivcmet.4 
|- ( ph -> S e. RR+ )
equivcmet.5 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x C y ) <_ ( R x. ( x D y ) ) )
equivcmet.6 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x D y ) <_ ( S x. ( x C y ) ) )
Assertion equivcmet 
|- ( ph -> ( C e. ( CMet ` X ) <-> D e. ( CMet ` X ) ) )

Proof

Step Hyp Ref Expression
1 equivcmet.1 
 |-  ( ph -> C e. ( Met ` X ) )
2 equivcmet.2 
 |-  ( ph -> D e. ( Met ` X ) )
3 equivcmet.3 
 |-  ( ph -> R e. RR+ )
4 equivcmet.4 
 |-  ( ph -> S e. RR+ )
5 equivcmet.5 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x C y ) <_ ( R x. ( x D y ) ) )
6 equivcmet.6 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x D y ) <_ ( S x. ( x C y ) ) )
7 1 2 2thd 
 |-  ( ph -> ( C e. ( Met ` X ) <-> D e. ( Met ` X ) ) )
8 2 1 4 6 equivcfil 
 |-  ( ph -> ( CauFil ` C ) C_ ( CauFil ` D ) )
9 1 2 3 5 equivcfil 
 |-  ( ph -> ( CauFil ` D ) C_ ( CauFil ` C ) )
10 8 9 eqssd 
 |-  ( ph -> ( CauFil ` C ) = ( CauFil ` D ) )
11 eqid 
 |-  ( MetOpen ` C ) = ( MetOpen ` C )
12 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
13 11 12 1 2 3 5 metss2 
 |-  ( ph -> ( MetOpen ` C ) C_ ( MetOpen ` D ) )
14 12 11 2 1 4 6 metss2 
 |-  ( ph -> ( MetOpen ` D ) C_ ( MetOpen ` C ) )
15 13 14 eqssd 
 |-  ( ph -> ( MetOpen ` C ) = ( MetOpen ` D ) )
16 15 oveq1d 
 |-  ( ph -> ( ( MetOpen ` C ) fLim f ) = ( ( MetOpen ` D ) fLim f ) )
17 16 neeq1d 
 |-  ( ph -> ( ( ( MetOpen ` C ) fLim f ) =/= (/) <-> ( ( MetOpen ` D ) fLim f ) =/= (/) ) )
18 10 17 raleqbidv 
 |-  ( ph -> ( A. f e. ( CauFil ` C ) ( ( MetOpen ` C ) fLim f ) =/= (/) <-> A. f e. ( CauFil ` D ) ( ( MetOpen ` D ) fLim f ) =/= (/) ) )
19 7 18 anbi12d 
 |-  ( ph -> ( ( C e. ( Met ` X ) /\ A. f e. ( CauFil ` C ) ( ( MetOpen ` C ) fLim f ) =/= (/) ) <-> ( D e. ( Met ` X ) /\ A. f e. ( CauFil ` D ) ( ( MetOpen ` D ) fLim f ) =/= (/) ) ) )
20 11 iscmet 
 |-  ( C e. ( CMet ` X ) <-> ( C e. ( Met ` X ) /\ A. f e. ( CauFil ` C ) ( ( MetOpen ` C ) fLim f ) =/= (/) ) )
21 12 iscmet 
 |-  ( D e. ( CMet ` X ) <-> ( D e. ( Met ` X ) /\ A. f e. ( CauFil ` D ) ( ( MetOpen ` D ) fLim f ) =/= (/) ) )
22 19 20 21 3bitr4g 
 |-  ( ph -> ( C e. ( CMet ` X ) <-> D e. ( CMet ` X ) ) )