Theorem metuval

Description: Value of the uniform structure generated by metric D . (Contributed by Thierry Arnoux, 1-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

	Ref	Expression
Assertion	metuval	|- ( D e. ( PsMet ` X ) -> ( metUnif ` D ) = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-metu	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
2		simpr	|- ( ( D e. ( PsMet ` X ) /\ d = D ) -> d = D )
3	2	dmeqd	|- ( ( D e. ( PsMet ` X ) /\ d = D ) -> dom d = dom D )
4	3	dmeqd	|- ( ( D e. ( PsMet ` X ) /\ d = D ) -> dom dom d = dom dom D )
5		psmetdmdm	|- ( D e. ( PsMet ` X ) -> X = dom dom D )
6	5	adantr	|- ( ( D e. ( PsMet ` X ) /\ d = D ) -> X = dom dom D )
7	4 6	eqtr4d	|- ( ( D e. ( PsMet ` X ) /\ d = D ) -> dom dom d = X )
8	7	sqxpeqd	|- ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( dom dom d X. dom dom d ) = ( X X. X ) )
9		simplr	|- ( ( ( D e. ( PsMet ` X ) /\ d = D ) /\ a e. RR+ ) -> d = D )
10	9	cnveqd	|- ( ( ( D e. ( PsMet ` X ) /\ d = D ) /\ a e. RR+ ) -> `' d = `' D )
11	10	imaeq1d	|- ( ( ( D e. ( PsMet ` X ) /\ d = D ) /\ a e. RR+ ) -> ( `' d " ( 0 [,) a ) ) = ( `' D " ( 0 [,) a ) ) )
12	11	mpteq2dva	|- ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) = ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) )
13	12	rneqd	|- ( ( D e. ( PsMet ` X ) /\ d = D ) -> ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) )
14	8 13	oveq12d	|- ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) )
15		elfvunirn	|- ( D e. ( PsMet ` X ) -> D e. U. ran PsMet )
16		ovexd	|- ( D e. ( PsMet ` X ) -> ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) e. _V )
17	1 14 15 16	fvmptd2	|- ( D e. ( PsMet ` X ) -> ( metUnif ` D ) = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) )