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 ⊢ ( 𝜑 → 𝐶 ∈ ( Met ‘ 𝑋 ) )
equivcmet.2 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
equivcmet.3 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
equivcmet.4 ⊢ ( 𝜑 → 𝑆 ∈ ℝ+ )
equivcmet.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) )
equivcmet.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( 𝑆 · ( 𝑥 𝐶 𝑦 ) ) )
Assertion equivcmet ( 𝜑 → ( 𝐶 ∈ ( CMet ‘ 𝑋 ) ↔ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 equivcmet.1 ⊢ ( 𝜑 → 𝐶 ∈ ( Met ‘ 𝑋 ) )
2 equivcmet.2 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3 equivcmet.3 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
4 equivcmet.4 ⊢ ( 𝜑 → 𝑆 ∈ ℝ+ )
5 equivcmet.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) )
6 equivcmet.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( 𝑆 · ( 𝑥 𝐶 𝑦 ) ) )
7 1 2 2thd ⊢ ( 𝜑 → ( 𝐶 ∈ ( Met ‘ 𝑋 ) ↔ 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
8 2 1 4 6 equivcfil ⊢ ( 𝜑 → ( CauFil ‘ 𝐶 ) ⊆ ( CauFil ‘ 𝐷 ) )
9 1 2 3 5 equivcfil ⊢ ( 𝜑 → ( CauFil ‘ 𝐷 ) ⊆ ( CauFil ‘ 𝐶 ) )
10 8 9 eqssd ⊢ ( 𝜑 → ( CauFil ‘ 𝐶 ) = ( CauFil ‘ 𝐷 ) )
11 eqid ⊢ ( MetOpen ‘ 𝐶 ) = ( MetOpen ‘ 𝐶 )
12 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
13 11 12 1 2 3 5 metss2 ⊢ ( 𝜑 → ( MetOpen ‘ 𝐶 ) ⊆ ( MetOpen ‘ 𝐷 ) )
14 12 11 2 1 4 6 metss2 ⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) ⊆ ( MetOpen ‘ 𝐶 ) )
15 13 14 eqssd ⊢ ( 𝜑 → ( MetOpen ‘ 𝐶 ) = ( MetOpen ‘ 𝐷 ) )
16 15 oveq1d ⊢ ( 𝜑 → ( ( MetOpen ‘ 𝐶 ) fLim 𝑓 ) = ( ( MetOpen ‘ 𝐷 ) fLim 𝑓 ) )
17 16 neeq1d ⊢ ( 𝜑 → ( ( ( MetOpen ‘ 𝐶 ) fLim 𝑓 ) ≠ ∅ ↔ ( ( MetOpen ‘ 𝐷 ) fLim 𝑓 ) ≠ ∅ ) )
18 10 17 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑓 ∈ ( CauFil ‘ 𝐶 ) ( ( MetOpen ‘ 𝐶 ) fLim 𝑓 ) ≠ ∅ ↔ ∀ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ( ( MetOpen ‘ 𝐷 ) fLim 𝑓 ) ≠ ∅ ) )
19 7 18 anbi12d ⊢ ( 𝜑 → ( ( 𝐶 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( CauFil ‘ 𝐶 ) ( ( MetOpen ‘ 𝐶 ) fLim 𝑓 ) ≠ ∅ ) ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ( ( MetOpen ‘ 𝐷 ) fLim 𝑓 ) ≠ ∅ ) ) )
20 11 iscmet ⊢ ( 𝐶 ∈ ( CMet ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( CauFil ‘ 𝐶 ) ( ( MetOpen ‘ 𝐶 ) fLim 𝑓 ) ≠ ∅ ) )
21 12 iscmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ( ( MetOpen ‘ 𝐷 ) fLim 𝑓 ) ≠ ∅ ) )
22 19 20 21 3bitr4g ⊢ ( 𝜑 → ( 𝐶 ∈ ( CMet ‘ 𝑋 ) ↔ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )