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 elfvdm 
 |-  ( D e. ( PsMet ` X ) -> X e. dom PsMet )
16 fveq2 
 |-  ( x = X -> ( PsMet ` x ) = ( PsMet ` X ) )
17 16 eleq2d 
 |-  ( x = X -> ( D e. ( PsMet ` x ) <-> D e. ( PsMet ` X ) ) )
18 17 rspcev 
 |-  ( ( X e. dom PsMet /\ D e. ( PsMet ` X ) ) -> E. x e. dom PsMet D e. ( PsMet ` x ) )
19 15 18 mpancom 
 |-  ( D e. ( PsMet ` X ) -> E. x e. dom PsMet D e. ( PsMet ` x ) )
20 df-psmet 
 |-  PsMet = ( y e. _V |-> { u e. ( RR* ^m ( y X. y ) ) | A. z e. y ( ( z u z ) = 0 /\ A. w e. y A. v e. y ( z u w ) <_ ( ( v u z ) +e ( v u w ) ) ) } )
21 20 funmpt2 
 |-  Fun PsMet
22 elunirn 
 |-  ( Fun PsMet -> ( D e. U. ran PsMet <-> E. x e. dom PsMet D e. ( PsMet ` x ) ) )
23 21 22 ax-mp 
 |-  ( D e. U. ran PsMet <-> E. x e. dom PsMet D e. ( PsMet ` x ) )
24 19 23 sylibr 
 |-  ( D e. ( PsMet ` X ) -> D e. U. ran PsMet )
25 ovexd 
 |-  ( D e. ( PsMet ` X ) -> ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) e. _V )
26 1 14 24 25 fvmptd2 
 |-  ( D e. ( PsMet ` X ) -> ( metUnif ` D ) = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) )