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. X ) )
xmsusp.u
|- U = ( UnifSt ` F )
Assertion xmsusp
|- ( ( X =/= (/) /\ F e. *MetSp /\ U = ( metUnif ` D ) ) -> F e. UnifSp )

Proof

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