Metamath Proof Explorer

Theorem pstmval

Description: Value of the metric induced by a pseudometric D . (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Hypothesis pstmval.1 
|- .~ = ( ~Met ` D )
Assertion pstmval 
|- ( D e. ( PsMet ` X ) -> ( pstoMet ` D ) = ( a e. ( X /. .~ ) , b e. ( X /. .~ ) |-> U. { z | E. x e. a E. y e. b z = ( x D y ) } ) )

Proof

Step Hyp Ref Expression
1 pstmval.1 
 |-  .~ = ( ~Met ` D )
2 df-pstm 
 |-  pstoMet = ( d e. U. ran PsMet |-> ( a e. ( dom dom d /. ( ~Met ` d ) ) , b e. ( dom dom d /. ( ~Met ` d ) ) |-> U. { z | E. x e. a E. y e. b z = ( x d y ) } ) )
3 2 a1i 
 |-  ( D e. ( PsMet ` X ) -> pstoMet = ( d e. U. ran PsMet |-> ( a e. ( dom dom d /. ( ~Met ` d ) ) , b e. ( dom dom d /. ( ~Met ` d ) ) |-> U. { z | E. x e. a E. y e. b z = ( x d y ) } ) ) )
4 psmetdmdm 
 |-  ( D e. ( PsMet ` X ) -> X = dom dom D )
5 4 adantr 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> X = dom dom D )
6 dmeq 
 |-  ( d = D -> dom d = dom D )
7 6 dmeqd 
 |-  ( d = D -> dom dom d = dom dom D )
8 7 adantl 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> dom dom d = dom dom D )
9 5 8 eqtr4d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> X = dom dom d )
10 qseq1 
 |-  ( X = dom dom d -> ( X /. .~ ) = ( dom dom d /. .~ ) )
11 9 10 syl 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( X /. .~ ) = ( dom dom d /. .~ ) )
12 fveq2 
 |-  ( d = D -> ( ~Met ` d ) = ( ~Met ` D ) )
13 1 12 eqtr4id 
 |-  ( d = D -> .~ = ( ~Met ` d ) )
14 qseq2 
 |-  ( .~ = ( ~Met ` d ) -> ( dom dom d /. .~ ) = ( dom dom d /. ( ~Met ` d ) ) )
15 13 14 syl 
 |-  ( d = D -> ( dom dom d /. .~ ) = ( dom dom d /. ( ~Met ` d ) ) )
16 15 adantl 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( dom dom d /. .~ ) = ( dom dom d /. ( ~Met ` d ) ) )
17 11 16 eqtr2d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( dom dom d /. ( ~Met ` d ) ) = ( X /. .~ ) )
18 mpoeq12 
 |-  ( ( ( dom dom d /. ( ~Met ` d ) ) = ( X /. .~ ) /\ ( dom dom d /. ( ~Met ` d ) ) = ( X /. .~ ) ) -> ( a e. ( dom dom d /. ( ~Met ` d ) ) , b e. ( dom dom d /. ( ~Met ` d ) ) |-> U. { z | E. x e. a E. y e. b z = ( x d y ) } ) = ( a e. ( X /. .~ ) , b e. ( X /. .~ ) |-> U. { z | E. x e. a E. y e. b z = ( x d y ) } ) )
19 17 17 18 syl2anc 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( a e. ( dom dom d /. ( ~Met ` d ) ) , b e. ( dom dom d /. ( ~Met ` d ) ) |-> U. { z | E. x e. a E. y e. b z = ( x d y ) } ) = ( a e. ( X /. .~ ) , b e. ( X /. .~ ) |-> U. { z | E. x e. a E. y e. b z = ( x d y ) } ) )
20 simp1r 
 |-  ( ( ( D e. ( PsMet ` X ) /\ d = D ) /\ a e. ( X /. .~ ) /\ b e. ( X /. .~ ) ) -> d = D )
21 20 oveqd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ d = D ) /\ a e. ( X /. .~ ) /\ b e. ( X /. .~ ) ) -> ( x d y ) = ( x D y ) )
22 21 eqeq2d 
 |-  ( ( ( D e. ( PsMet ` X ) /\ d = D ) /\ a e. ( X /. .~ ) /\ b e. ( X /. .~ ) ) -> ( z = ( x d y ) <-> z = ( x D y ) ) )
23 22 2rexbidv 
 |-  ( ( ( D e. ( PsMet ` X ) /\ d = D ) /\ a e. ( X /. .~ ) /\ b e. ( X /. .~ ) ) -> ( E. x e. a E. y e. b z = ( x d y ) <-> E. x e. a E. y e. b z = ( x D y ) ) )
24 23 abbidv 
 |-  ( ( ( D e. ( PsMet ` X ) /\ d = D ) /\ a e. ( X /. .~ ) /\ b e. ( X /. .~ ) ) -> { z | E. x e. a E. y e. b z = ( x d y ) } = { z | E. x e. a E. y e. b z = ( x D y ) } )
25 24 unieqd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ d = D ) /\ a e. ( X /. .~ ) /\ b e. ( X /. .~ ) ) -> U. { z | E. x e. a E. y e. b z = ( x d y ) } = U. { z | E. x e. a E. y e. b z = ( x D y ) } )
26 25 mpoeq3dva 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( a e. ( X /. .~ ) , b e. ( X /. .~ ) |-> U. { z | E. x e. a E. y e. b z = ( x d y ) } ) = ( a e. ( X /. .~ ) , b e. ( X /. .~ ) |-> U. { z | E. x e. a E. y e. b z = ( x D y ) } ) )
27 19 26 eqtrd 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( a e. ( dom dom d /. ( ~Met ` d ) ) , b e. ( dom dom d /. ( ~Met ` d ) ) |-> U. { z | E. x e. a E. y e. b z = ( x d y ) } ) = ( a e. ( X /. .~ ) , b e. ( X /. .~ ) |-> U. { z | E. x e. a E. y e. b z = ( x D y ) } ) )
28 elfvdm 
 |-  ( D e. ( PsMet ` X ) -> X e. dom PsMet )
29 fveq2 
 |-  ( x = X -> ( PsMet ` x ) = ( PsMet ` X ) )
30 29 eleq2d 
 |-  ( x = X -> ( D e. ( PsMet ` x ) <-> D e. ( PsMet ` X ) ) )
31 30 rspcev 
 |-  ( ( X e. dom PsMet /\ D e. ( PsMet ` X ) ) -> E. x e. dom PsMet D e. ( PsMet ` x ) )
32 28 31 mpancom 
 |-  ( D e. ( PsMet ` X ) -> E. x e. dom PsMet D e. ( PsMet ` x ) )
33 df-psmet 
 |-  PsMet = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. a e. x ( ( a d a ) = 0 /\ A. b e. x A. c e. x ( a d b ) <_ ( ( c d a ) +e ( c d b ) ) ) } )
34 33 funmpt2 
 |-  Fun PsMet
35 elunirn 
 |-  ( Fun PsMet -> ( D e. U. ran PsMet <-> E. x e. dom PsMet D e. ( PsMet ` x ) ) )
36 34 35 ax-mp 
 |-  ( D e. U. ran PsMet <-> E. x e. dom PsMet D e. ( PsMet ` x ) )
37 32 36 sylibr 
 |-  ( D e. ( PsMet ` X ) -> D e. U. ran PsMet )
38 elfvex 
 |-  ( D e. ( PsMet ` X ) -> X e. _V )
39 qsexg 
 |-  ( X e. _V -> ( X /. .~ ) e. _V )
40 38 39 syl 
 |-  ( D e. ( PsMet ` X ) -> ( X /. .~ ) e. _V )
41 mpoexga 
 |-  ( ( ( X /. .~ ) e. _V /\ ( X /. .~ ) e. _V ) -> ( a e. ( X /. .~ ) , b e. ( X /. .~ ) |-> U. { z | E. x e. a E. y e. b z = ( x D y ) } ) e. _V )
42 40 40 41 syl2anc 
 |-  ( D e. ( PsMet ` X ) -> ( a e. ( X /. .~ ) , b e. ( X /. .~ ) |-> U. { z | E. x e. a E. y e. b z = ( x D y ) } ) e. _V )
43 3 27 37 42 fvmptd 
 |-  ( D e. ( PsMet ` X ) -> ( pstoMet ` D ) = ( a e. ( X /. .~ ) , b e. ( X /. .~ ) |-> U. { z | E. x e. a E. y e. b z = ( x D y ) } ) )