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 psmetdmdm 
 |-  ( D e. ( PsMet ` X ) -> X = dom dom D )
4 3 adantr 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> X = dom dom D )
5 dmeq 
 |-  ( d = D -> dom d = dom D )
6 5 dmeqd 
 |-  ( d = D -> dom dom d = dom dom D )
7 6 adantl 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> dom dom d = dom dom D )
8 4 7 eqtr4d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> X = dom dom d )
9 qseq1 
 |-  ( X = dom dom d -> ( X /. .~ ) = ( dom dom d /. .~ ) )
10 8 9 syl 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( X /. .~ ) = ( dom dom d /. .~ ) )
11 fveq2 
 |-  ( d = D -> ( ~Met ` d ) = ( ~Met ` D ) )
12 1 11 eqtr4id 
 |-  ( d = D -> .~ = ( ~Met ` d ) )
13 12 qseq2d 
 |-  ( d = D -> ( dom dom d /. .~ ) = ( dom dom d /. ( ~Met ` d ) ) )
14 13 adantl 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( dom dom d /. .~ ) = ( dom dom d /. ( ~Met ` d ) ) )
15 10 14 eqtr2d 
 |-  ( ( D e. ( PsMet ` X ) /\ d = D ) -> ( dom dom d /. ( ~Met ` d ) ) = ( X /. .~ ) )
16 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 ) } ) )
17 15 15 16 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 ) } ) )
18 simp1r 
 |-  ( ( ( D e. ( PsMet ` X ) /\ d = D ) /\ a e. ( X /. .~ ) /\ b e. ( X /. .~ ) ) -> d = D )
19 18 oveqd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ d = D ) /\ a e. ( X /. .~ ) /\ b e. ( X /. .~ ) ) -> ( x d y ) = ( x D y ) )
20 19 eqeq2d 
 |-  ( ( ( D e. ( PsMet ` X ) /\ d = D ) /\ a e. ( X /. .~ ) /\ b e. ( X /. .~ ) ) -> ( z = ( x d y ) <-> z = ( x D y ) ) )
21 20 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 ) ) )
22 21 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 ) } )
23 22 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 ) } )
24 23 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 ) } ) )
25 17 24 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 ) } ) )
26 elfvunirn 
 |-  ( D e. ( PsMet ` X ) -> D e. U. ran PsMet )
27 elfvex 
 |-  ( D e. ( PsMet ` X ) -> X e. _V )
28 qsexg 
 |-  ( X e. _V -> ( X /. .~ ) e. _V )
29 27 28 syl 
 |-  ( D e. ( PsMet ` X ) -> ( X /. .~ ) e. _V )
30 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 )
31 29 29 30 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 )
32 2 25 26 31 fvmptd2 
 |-  ( 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 ) } ) )