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 ⊢ φ → C ∈ Met ⁡ X
equivcmet.2 ⊢ φ → D ∈ Met ⁡ X
equivcmet.3 ⊢ φ → R ∈ ℝ +
equivcmet.4 ⊢ φ → S ∈ ℝ +
equivcmet.5 ⊢ φ ∧ x ∈ X ∧ y ∈ X → x C y ≤ R ⁢ x D y
equivcmet.6 ⊢ φ ∧ x ∈ X ∧ y ∈ X → x D y ≤ S ⁢ x C y
Assertion equivcmet ⊢ φ → C ∈ CMet ⁡ X ↔ D ∈ CMet ⁡ X

Proof

Step Hyp Ref Expression
1 equivcmet.1 ⊢ φ → C ∈ Met ⁡ X
2 equivcmet.2 ⊢ φ → D ∈ Met ⁡ X
3 equivcmet.3 ⊢ φ → R ∈ ℝ +
4 equivcmet.4 ⊢ φ → S ∈ ℝ +
5 equivcmet.5 ⊢ φ ∧ x ∈ X ∧ y ∈ X → x C y ≤ R ⁢ x D y
6 equivcmet.6 ⊢ φ ∧ x ∈ X ∧ y ∈ X → x D y ≤ S ⁢ x C y
7 1 2 2thd ⊢ φ → C ∈ Met ⁡ X ↔ D ∈ Met ⁡ X
8 2 1 4 6 equivcfil ⊢ φ → CauFil ⁡ C ⊆ CauFil ⁡ D
9 1 2 3 5 equivcfil ⊢ φ → CauFil ⁡ D ⊆ CauFil ⁡ C
10 8 9 eqssd ⊢ φ → CauFil ⁡ C = CauFil ⁡ D
11 eqid ⊢ MetOpen ⁡ C = MetOpen ⁡ C
12 eqid ⊢ MetOpen ⁡ D = MetOpen ⁡ D
13 11 12 1 2 3 5 metss2 ⊢ φ → MetOpen ⁡ C ⊆ MetOpen ⁡ D
14 12 11 2 1 4 6 metss2 ⊢ φ → MetOpen ⁡ D ⊆ MetOpen ⁡ C
15 13 14 eqssd ⊢ φ → MetOpen ⁡ C = MetOpen ⁡ D
16 15 oveq1d ⊢ φ → MetOpen ⁡ C fLim f = MetOpen ⁡ D fLim f
17 16 neeq1d ⊢ φ → MetOpen ⁡ C fLim f ≠ ∅ ↔ MetOpen ⁡ D fLim f ≠ ∅
18 10 17 raleqbidv ⊢ φ → ∀ f ∈ CauFil ⁡ C MetOpen ⁡ C fLim f ≠ ∅ ↔ ∀ f ∈ CauFil ⁡ D MetOpen ⁡ D fLim f ≠ ∅
19 7 18 anbi12d ⊢ φ → C ∈ Met ⁡ X ∧ ∀ f ∈ CauFil ⁡ C MetOpen ⁡ C fLim f ≠ ∅ ↔ D ∈ Met ⁡ X ∧ ∀ f ∈ CauFil ⁡ D MetOpen ⁡ D fLim f ≠ ∅
20 11 iscmet ⊢ C ∈ CMet ⁡ X ↔ C ∈ Met ⁡ X ∧ ∀ f ∈ CauFil ⁡ C MetOpen ⁡ C fLim f ≠ ∅
21 12 iscmet ⊢ D ∈ CMet ⁡ X ↔ D ∈ Met ⁡ X ∧ ∀ f ∈ CauFil ⁡ D MetOpen ⁡ D fLim f ≠ ∅
22 19 20 21 3bitr4g ⊢ φ → C ∈ CMet ⁡ X ↔ D ∈ CMet ⁡ X