Metamath Proof Explorer


Theorem metss2

Description: If the metric D is "strongly finer" than C (meaning that there is a positive real constant R such that C ( x , y ) <_ R x. D ( x , y ) ), then D generates a finer topology. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they generate the same topology.) (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypotheses metequiv.3 J=MetOpenC
metequiv.4 K=MetOpenD
metss2.1 φCMetX
metss2.2 φDMetX
metss2.3 φR+
metss2.4 φxXyXxCyRxDy
Assertion metss2 φJK

Proof

Step Hyp Ref Expression
1 metequiv.3 J=MetOpenC
2 metequiv.4 K=MetOpenD
3 metss2.1 φCMetX
4 metss2.2 φDMetX
5 metss2.3 φR+
6 metss2.4 φxXyXxCyRxDy
7 simpr xXr+r+
8 rpdivcl r+R+rR+
9 7 5 8 syl2anr φxXr+rR+
10 1 2 3 4 5 6 metss2lem φxXr+xballDrRxballCr
11 oveq2 s=rRxballDs=xballDrR
12 11 sseq1d s=rRxballDsxballCrxballDrRxballCr
13 12 rspcev rR+xballDrRxballCrs+xballDsxballCr
14 9 10 13 syl2anc φxXr+s+xballDsxballCr
15 14 ralrimivva φxXr+s+xballDsxballCr
16 metxmet CMetXC∞MetX
17 3 16 syl φC∞MetX
18 metxmet DMetXD∞MetX
19 4 18 syl φD∞MetX
20 1 2 metss C∞MetXD∞MetXJKxXr+s+xballDsxballCr
21 17 19 20 syl2anc φJKxXr+s+xballDsxballCr
22 15 21 mpbird φJK