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

Metamath Proof Explorer

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 ) ) ) ) )