Metamath Proof Explorer


Theorem metequiv2

Description: If there is a sequence of radii approaching zero for which the balls of both metrics coincide, then the generated topologies are equivalent. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses metequiv.3 J = MetOpen C
metequiv.4 K = MetOpen D
Assertion metequiv2 C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s J = K

Proof

Step Hyp Ref Expression
1 metequiv.3 J = MetOpen C
2 metequiv.4 K = MetOpen D
3 simprrr C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s x ball C s = x ball D s
4 simplll C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s C ∞Met X
5 simplr C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s x X
6 simprlr C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s s +
7 6 rpxrd C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s s *
8 simprll C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s r +
9 8 rpxrd C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s r *
10 simprrl C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s s r
11 ssbl C ∞Met X x X s * r * s r x ball C s x ball C r
12 4 5 7 9 10 11 syl221anc C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s x ball C s x ball C r
13 3 12 eqsstrrd C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s x ball D s x ball C r
14 simpllr C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s D ∞Met X
15 ssbl D ∞Met X x X s * r * s r x ball D s x ball D r
16 14 5 7 9 10 15 syl221anc C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s x ball D s x ball D r
17 3 16 eqsstrd C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s x ball C s x ball D r
18 13 17 jca C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s x ball D s x ball C r x ball C s x ball D r
19 18 expr C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s x ball D s x ball C r x ball C s x ball D r
20 19 anassrs C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s x ball D s x ball C r x ball C s x ball D r
21 20 reximdva C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s s + x ball D s x ball C r x ball C s x ball D r
22 r19.40 s + x ball D s x ball C r x ball C s x ball D r s + x ball D s x ball C r s + x ball C s x ball D r
23 21 22 syl6 C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s s + x ball D s x ball C r s + x ball C s x ball D r
24 23 ralimdva C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s r + s + x ball D s x ball C r s + x ball C s x ball D r
25 r19.26 r + s + x ball D s x ball C r s + x ball C s x ball D r r + s + x ball D s x ball C r r + s + x ball C s x ball D r
26 24 25 syl6ib C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s r + s + x ball D s x ball C r r + s + x ball C s x ball D r
27 26 ralimdva C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s x X r + s + x ball D s x ball C r r + s + x ball C s x ball D r
28 1 2 metequiv C ∞Met X D ∞Met X J = K x X r + s + x ball D s x ball C r r + s + x ball C s x ball D r
29 27 28 sylibrd C ∞Met X D ∞Met X x X r + s + s r x ball C s = x ball D s J = K