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 ⊢ 𝑋 = ( Base ‘ 𝐹 )
xmsusp.d ⊢ 𝐷 = ( ( dist ‘ 𝐹 ) ↾ ( 𝑋 × 𝑋 ) )
xmsusp.u ⊢ 𝑈 = ( UnifSt ‘ 𝐹 )
Assertion xmsusp ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → 𝐹 ∈ UnifSp )

Proof

Step Hyp Ref Expression
1 xmsusp.x ⊢ 𝑋 = ( Base ‘ 𝐹 )
2 xmsusp.d ⊢ 𝐷 = ( ( dist ‘ 𝐹 ) ↾ ( 𝑋 × 𝑋 ) )
3 xmsusp.u ⊢ 𝑈 = ( UnifSt ‘ 𝐹 )
4 simp3 ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → 𝑈 = ( metUnif ‘ 𝐷 ) )
5 simp1 ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → 𝑋 ≠ ∅ )
6 1 2 xmsxmet ⊢ ( 𝐹 ∈ ∞MetSp → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
7 6 3ad2ant2 ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
8 xmetpsmet ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
9 metuust ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) )
10 8 9 sylan2 ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) )
11 5 7 10 syl2anc ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) )
12 4 11 eqeltrd ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
13 xmetutop ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) )
14 5 7 13 syl2anc ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) )
15 4 fveq2d ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → ( unifTop ‘ 𝑈 ) = ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) )
16 eqid ⊢ ( TopOpen ‘ 𝐹 ) = ( TopOpen ‘ 𝐹 )
17 16 1 2 xmstopn ⊢ ( 𝐹 ∈ ∞MetSp → ( TopOpen ‘ 𝐹 ) = ( MetOpen ‘ 𝐷 ) )
18 17 3ad2ant2 ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → ( TopOpen ‘ 𝐹 ) = ( MetOpen ‘ 𝐷 ) )
19 14 15 18 3eqtr4rd ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → ( TopOpen ‘ 𝐹 ) = ( unifTop ‘ 𝑈 ) )
20 1 3 16 isusp ⊢ ( 𝐹 ∈ UnifSp ↔ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( TopOpen ‘ 𝐹 ) = ( unifTop ‘ 𝑈 ) ) )
21 12 19 20 sylanbrc ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → 𝐹 ∈ UnifSp )