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