Metamath Proof Explorer


Theorem xmsusp

Description: If the uniform set of a metric space is the uniform structure generated by its metric, then it is a uniform space. (Contributed by Thierry Arnoux, 14-Dec-2017)

Ref Expression
Hypotheses xmsusp.x X = Base F
xmsusp.d D = dist F X × X
xmsusp.u U = UnifSt F
Assertion xmsusp X F ∞MetSp U = metUnif D F UnifSp

Proof

Step Hyp Ref Expression
1 xmsusp.x X = Base F
2 xmsusp.d D = dist F X × X
3 xmsusp.u U = UnifSt F
4 simp3 X F ∞MetSp U = metUnif D U = metUnif D
5 simp1 X F ∞MetSp U = metUnif D X
6 1 2 xmsxmet F ∞MetSp D ∞Met X
7 6 3ad2ant2 X F ∞MetSp U = metUnif D D ∞Met X
8 xmetpsmet D ∞Met X D PsMet X
9 metuust X D PsMet X metUnif D UnifOn X
10 8 9 sylan2 X D ∞Met X metUnif D UnifOn X
11 5 7 10 syl2anc X F ∞MetSp U = metUnif D metUnif D UnifOn X
12 4 11 eqeltrd X F ∞MetSp U = metUnif D U UnifOn X
13 xmetutop X D ∞Met X unifTop metUnif D = MetOpen D
14 5 7 13 syl2anc X F ∞MetSp U = metUnif D unifTop metUnif D = MetOpen D
15 4 fveq2d X F ∞MetSp U = metUnif D unifTop U = unifTop metUnif D
16 eqid TopOpen F = TopOpen F
17 16 1 2 xmstopn F ∞MetSp TopOpen F = MetOpen D
18 17 3ad2ant2 X F ∞MetSp U = metUnif D TopOpen F = MetOpen D
19 14 15 18 3eqtr4rd X F ∞MetSp U = metUnif D TopOpen F = unifTop U
20 1 3 16 isusp F UnifSp U UnifOn X TopOpen F = unifTop U
21 12 19 20 sylanbrc X F ∞MetSp U = metUnif D F UnifSp