Metamath Proof Explorer

Theorem reust

Description: The Uniform structure of the real numbers. (Contributed by Thierry Arnoux, 14-Feb-2018)

Ref Expression
Assertion reust 
|- ( UnifSt ` RRfld ) = ( metUnif ` ( ( dist ` RRfld ) |` ( RR X. RR ) ) )

Proof

Step Hyp Ref Expression
1 df-refld 
 |-  RRfld = ( CCfld |`s RR )
2 1 fveq2i 
 |-  ( UnifSt ` RRfld ) = ( UnifSt ` ( CCfld |`s RR ) )
3 reex 
 |-  RR e. _V
4 ressuss 
 |-  ( RR e. _V -> ( UnifSt ` ( CCfld |`s RR ) ) = ( ( UnifSt ` CCfld ) |`t ( RR X. RR ) ) )
5 3 4 ax-mp 
 |-  ( UnifSt ` ( CCfld |`s RR ) ) = ( ( UnifSt ` CCfld ) |`t ( RR X. RR ) )
6 eqid 
 |-  ( UnifSt ` CCfld ) = ( UnifSt ` CCfld )
7 6 cnflduss 
 |-  ( UnifSt ` CCfld ) = ( metUnif ` ( abs o. - ) )
8 7 oveq1i 
 |-  ( ( UnifSt ` CCfld ) |`t ( RR X. RR ) ) = ( ( metUnif ` ( abs o. - ) ) |`t ( RR X. RR ) )
9 2 5 8 3eqtri 
 |-  ( UnifSt ` RRfld ) = ( ( metUnif ` ( abs o. - ) ) |`t ( RR X. RR ) )
10 0re 
 |-  0 e. RR
11 10 ne0ii 
 |-  RR =/= (/)
12 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
13 xmetpsmet 
 |-  ( ( abs o. - ) e. ( *Met ` CC ) -> ( abs o. - ) e. ( PsMet ` CC ) )
14 12 13 ax-mp 
 |-  ( abs o. - ) e. ( PsMet ` CC )
15 ax-resscn 
 |-  RR C_ CC
16 restmetu 
 |-  ( ( RR =/= (/) /\ ( abs o. - ) e. ( PsMet ` CC ) /\ RR C_ CC ) -> ( ( metUnif ` ( abs o. - ) ) |`t ( RR X. RR ) ) = ( metUnif ` ( ( abs o. - ) |` ( RR X. RR ) ) ) )
17 11 14 15 16 mp3an 
 |-  ( ( metUnif ` ( abs o. - ) ) |`t ( RR X. RR ) ) = ( metUnif ` ( ( abs o. - ) |` ( RR X. RR ) ) )
18 reds 
 |-  ( abs o. - ) = ( dist ` RRfld )
19 18 reseq1i 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( dist ` RRfld ) |` ( RR X. RR ) )
20 19 fveq2i 
 |-  ( metUnif ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( metUnif ` ( ( dist ` RRfld ) |` ( RR X. RR ) ) )
21 9 17 20 3eqtri 
 |-  ( UnifSt ` RRfld ) = ( metUnif ` ( ( dist ` RRfld ) |` ( RR X. RR ) ) )