Metamath Proof Explorer


Theorem metuust

Description: The uniform structure generated by metric D is a uniform structure. (Contributed by Thierry Arnoux, 1-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion metuust XDPsMetXmetUnifDUnifOnX

Proof

Step Hyp Ref Expression
1 metuval DPsMetXmetUnifD=X×XfilGenrana+D-10a
2 1 adantl XDPsMetXmetUnifD=X×XfilGenrana+D-10a
3 oveq2 a=b0a=0b
4 3 imaeq2d a=bD-10a=D-10b
5 4 cbvmptv a+D-10a=b+D-10b
6 5 rneqi rana+D-10a=ranb+D-10b
7 6 metust XDPsMetXX×XfilGenrana+D-10aUnifOnX
8 2 7 eqeltrd XDPsMetXmetUnifDUnifOnX