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 ‘ 𝑋 ) ) )