This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	\|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( metUnif ` D ) e. ( UnifOn ` X ) )

Proof

Step	Hyp	Ref	Expression
1		metuval	\|- ( D e. ( PsMet ` X ) -> ( metUnif ` D ) = ( ( X X. X ) filGen ran ( a e. RR+ \|-> ( `' D " ( 0 [,) a ) ) ) ) )
2	1	adantl	\|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( metUnif ` D ) = ( ( X X. X ) filGen ran ( a e. RR+ \|-> ( `' D " ( 0 [,) a ) ) ) ) )
3		oveq2	\|- ( a = b -> ( 0 [,) a ) = ( 0 [,) b ) )
4	3	imaeq2d	\|- ( a = b -> ( `' D " ( 0 [,) a ) ) = ( `' D " ( 0 [,) b ) ) )
5	4	cbvmptv	\|- ( a e. RR+ \|-> ( `' D " ( 0 [,) a ) ) ) = ( b e. RR+ \|-> ( `' D " ( 0 [,) b ) ) )
6	5	rneqi	\|- ran ( a e. RR+ \|-> ( `' D " ( 0 [,) a ) ) ) = ran ( b e. RR+ \|-> ( `' D " ( 0 [,) b ) ) )
7	6	metust	\|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( ( X X. X ) filGen ran ( a e. RR+ \|-> ( `' D " ( 0 [,) a ) ) ) ) e. ( UnifOn ` X ) )
8	2 7	eqeltrd	\|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( metUnif ` D ) e. ( UnifOn ` X ) )