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 )