Metamath Proof Explorer

Theorem pstmxmet

Description: The metric induced by a pseudometric is a full-fledged metric on the equivalence classes of the metric identification. (Contributed by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis pstmval.1 
|- .~ = ( ~Met ` D )
Assertion pstmxmet 
|- ( D e. ( PsMet ` X ) -> ( pstoMet ` D ) e. ( *Met ` ( X /. .~ ) ) )

Proof

Step Hyp Ref Expression
1 pstmval.1 
 |-  .~ = ( ~Met ` D )
2 eqid 
 |-  ( x e. ( X /. .~ ) , y e. ( X /. .~ ) |-> U. { z | E. a e. x E. b e. y z = ( a D b ) } ) = ( x e. ( X /. .~ ) , y e. ( X /. .~ ) |-> U. { z | E. a e. x E. b e. y z = ( a D b ) } )
3 vex 
 |-  x e. _V
4 vex 
 |-  y e. _V
5 3 4 ab2rexex 
 |-  { z | E. a e. x E. b e. y z = ( a D b ) } e. _V
6 5 uniex 
 |-  U. { z | E. a e. x E. b e. y z = ( a D b ) } e. _V
7 2 6 fnmpoi 
 |-  ( x e. ( X /. .~ ) , y e. ( X /. .~ ) |-> U. { z | E. a e. x E. b e. y z = ( a D b ) } ) Fn ( ( X /. .~ ) X. ( X /. .~ ) )
8 1 pstmval 
 |-  ( D e. ( PsMet ` X ) -> ( pstoMet ` D ) = ( x e. ( X /. .~ ) , y e. ( X /. .~ ) |-> U. { z | E. a e. x E. b e. y z = ( a D b ) } ) )
9 8 fneq1d 
 |-  ( D e. ( PsMet ` X ) -> ( ( pstoMet ` D ) Fn ( ( X /. .~ ) X. ( X /. .~ ) ) <-> ( x e. ( X /. .~ ) , y e. ( X /. .~ ) |-> U. { z | E. a e. x E. b e. y z = ( a D b ) } ) Fn ( ( X /. .~ ) X. ( X /. .~ ) ) ) )
10 7 9 mpbiri 
 |-  ( D e. ( PsMet ` X ) -> ( pstoMet ` D ) Fn ( ( X /. .~ ) X. ( X /. .~ ) ) )
11 simpllr 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> x = [ a ] .~ )
12 simpr 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> y = [ b ] .~ )
13 11 12 oveq12d 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> ( x ( pstoMet ` D ) y ) = ( [ a ] .~ ( pstoMet ` D ) [ b ] .~ ) )
14 simp-5l 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> D e. ( PsMet ` X ) )
15 simp-4r 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> a e. X )
16 simplr 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> b e. X )
17 1 pstmfval 
 |-  ( ( D e. ( PsMet ` X ) /\ a e. X /\ b e. X ) -> ( [ a ] .~ ( pstoMet ` D ) [ b ] .~ ) = ( a D b ) )
18 14 15 16 17 syl3anc 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> ( [ a ] .~ ( pstoMet ` D ) [ b ] .~ ) = ( a D b ) )
19 13 18 eqtrd 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> ( x ( pstoMet ` D ) y ) = ( a D b ) )
20 psmetf 
 |-  ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> RR* )
21 14 20 syl 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> D : ( X X. X ) --> RR* )
22 21 15 16 fovcdmd 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> ( a D b ) e. RR* )
23 19 22 eqeltrd 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> ( x ( pstoMet ` D ) y ) e. RR* )
24 elqsi 
 |-  ( y e. ( X /. .~ ) -> E. b e. X y = [ b ] .~ )
25 24 ad2antll 
 |-  ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) -> E. b e. X y = [ b ] .~ )
26 25 ad2antrr 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) -> E. b e. X y = [ b ] .~ )
27 23 26 r19.29a 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) -> ( x ( pstoMet ` D ) y ) e. RR* )
28 elqsi 
 |-  ( x e. ( X /. .~ ) -> E. a e. X x = [ a ] .~ )
29 28 ad2antrl 
 |-  ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) -> E. a e. X x = [ a ] .~ )
30 27 29 r19.29a 
 |-  ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) -> ( x ( pstoMet ` D ) y ) e. RR* )
31 30 ralrimivva 
 |-  ( D e. ( PsMet ` X ) -> A. x e. ( X /. .~ ) A. y e. ( X /. .~ ) ( x ( pstoMet ` D ) y ) e. RR* )
32 ffnov 
 |-  ( ( pstoMet ` D ) : ( ( X /. .~ ) X. ( X /. .~ ) ) --> RR* <-> ( ( pstoMet ` D ) Fn ( ( X /. .~ ) X. ( X /. .~ ) ) /\ A. x e. ( X /. .~ ) A. y e. ( X /. .~ ) ( x ( pstoMet ` D ) y ) e. RR* ) )
33 10 31 32 sylanbrc 
 |-  ( D e. ( PsMet ` X ) -> ( pstoMet ` D ) : ( ( X /. .~ ) X. ( X /. .~ ) ) --> RR* )
34 17 3expa 
 |-  ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ b e. X ) -> ( [ a ] .~ ( pstoMet ` D ) [ b ] .~ ) = ( a D b ) )
35 34 eqeq1d 
 |-  ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ b e. X ) -> ( ( [ a ] .~ ( pstoMet ` D ) [ b ] .~ ) = 0 <-> ( a D b ) = 0 ) )
36 1 breqi 
 |-  ( a .~ b <-> a ( ~Met ` D ) b )
37 metidv 
 |-  ( ( D e. ( PsMet ` X ) /\ ( a e. X /\ b e. X ) ) -> ( a ( ~Met ` D ) b <-> ( a D b ) = 0 ) )
38 37 anassrs 
 |-  ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ b e. X ) -> ( a ( ~Met ` D ) b <-> ( a D b ) = 0 ) )
39 36 38 bitrid 
 |-  ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ b e. X ) -> ( a .~ b <-> ( a D b ) = 0 ) )
40 metider 
 |-  ( D e. ( PsMet ` X ) -> ( ~Met ` D ) Er X )
41 40 ad2antrr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ b e. X ) -> ( ~Met ` D ) Er X )
42 ereq1 
 |-  ( .~ = ( ~Met ` D ) -> ( .~ Er X <-> ( ~Met ` D ) Er X ) )
43 1 42 ax-mp 
 |-  ( .~ Er X <-> ( ~Met ` D ) Er X )
44 41 43 sylibr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ b e. X ) -> .~ Er X )
45 simplr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ b e. X ) -> a e. X )
46 44 45 erth 
 |-  ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ b e. X ) -> ( a .~ b <-> [ a ] .~ = [ b ] .~ ) )
47 35 39 46 3bitr2d 
 |-  ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ b e. X ) -> ( ( [ a ] .~ ( pstoMet ` D ) [ b ] .~ ) = 0 <-> [ a ] .~ = [ b ] .~ ) )
48 47 adantllr 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ b e. X ) -> ( ( [ a ] .~ ( pstoMet ` D ) [ b ] .~ ) = 0 <-> [ a ] .~ = [ b ] .~ ) )
49 48 adantlr 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) -> ( ( [ a ] .~ ( pstoMet ` D ) [ b ] .~ ) = 0 <-> [ a ] .~ = [ b ] .~ ) )
50 49 adantr 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> ( ( [ a ] .~ ( pstoMet ` D ) [ b ] .~ ) = 0 <-> [ a ] .~ = [ b ] .~ ) )
51 13 eqeq1d 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> ( ( x ( pstoMet ` D ) y ) = 0 <-> ( [ a ] .~ ( pstoMet ` D ) [ b ] .~ ) = 0 ) )
52 11 12 eqeq12d 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> ( x = y <-> [ a ] .~ = [ b ] .~ ) )
53 50 51 52 3bitr4d 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> ( ( x ( pstoMet ` D ) y ) = 0 <-> x = y ) )
54 53 26 r19.29a 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) /\ a e. X ) /\ x = [ a ] .~ ) -> ( ( x ( pstoMet ` D ) y ) = 0 <-> x = y ) )
55 54 29 r19.29a 
 |-  ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) -> ( ( x ( pstoMet ` D ) y ) = 0 <-> x = y ) )
56 simp-6l 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> D e. ( PsMet ` X ) )
57 simplr 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> c e. X )
58 simp-6r 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> a e. X )
59 simp-4r 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> b e. X )
60 psmettri2 
 |-  ( ( D e. ( PsMet ` X ) /\ ( c e. X /\ a e. X /\ b e. X ) ) -> ( a D b ) <_ ( ( c D a ) +e ( c D b ) ) )
61 56 57 58 59 60 syl13anc 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> ( a D b ) <_ ( ( c D a ) +e ( c D b ) ) )
62 simp-5r 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> x = [ a ] .~ )
63 simpllr 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> y = [ b ] .~ )
64 62 63 oveq12d 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> ( x ( pstoMet ` D ) y ) = ( [ a ] .~ ( pstoMet ` D ) [ b ] .~ ) )
65 56 58 59 17 syl3anc 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> ( [ a ] .~ ( pstoMet ` D ) [ b ] .~ ) = ( a D b ) )
66 64 65 eqtrd 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> ( x ( pstoMet ` D ) y ) = ( a D b ) )
67 simpr 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> z = [ c ] .~ )
68 67 62 oveq12d 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> ( z ( pstoMet ` D ) x ) = ( [ c ] .~ ( pstoMet ` D ) [ a ] .~ ) )
69 1 pstmfval 
 |-  ( ( D e. ( PsMet ` X ) /\ c e. X /\ a e. X ) -> ( [ c ] .~ ( pstoMet ` D ) [ a ] .~ ) = ( c D a ) )
70 56 57 58 69 syl3anc 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> ( [ c ] .~ ( pstoMet ` D ) [ a ] .~ ) = ( c D a ) )
71 68 70 eqtrd 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> ( z ( pstoMet ` D ) x ) = ( c D a ) )
72 67 63 oveq12d 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> ( z ( pstoMet ` D ) y ) = ( [ c ] .~ ( pstoMet ` D ) [ b ] .~ ) )
73 1 pstmfval 
 |-  ( ( D e. ( PsMet ` X ) /\ c e. X /\ b e. X ) -> ( [ c ] .~ ( pstoMet ` D ) [ b ] .~ ) = ( c D b ) )
74 56 57 59 73 syl3anc 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> ( [ c ] .~ ( pstoMet ` D ) [ b ] .~ ) = ( c D b ) )
75 72 74 eqtrd 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> ( z ( pstoMet ` D ) y ) = ( c D b ) )
76 71 75 oveq12d 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> ( ( z ( pstoMet ` D ) x ) +e ( z ( pstoMet ` D ) y ) ) = ( ( c D a ) +e ( c D b ) ) )
77 61 66 76 3brtr4d 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> ( x ( pstoMet ` D ) y ) <_ ( ( z ( pstoMet ` D ) x ) +e ( z ( pstoMet ` D ) y ) ) )
78 77 adantl6r 
 |-  ( ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ z e. ( X /. .~ ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) /\ c e. X ) /\ z = [ c ] .~ ) -> ( x ( pstoMet ` D ) y ) <_ ( ( z ( pstoMet ` D ) x ) +e ( z ( pstoMet ` D ) y ) ) )
79 elqsi 
 |-  ( z e. ( X /. .~ ) -> E. c e. X z = [ c ] .~ )
80 79 ad5antlr 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ z e. ( X /. .~ ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> E. c e. X z = [ c ] .~ )
81 78 80 r19.29a 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ z e. ( X /. .~ ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> ( x ( pstoMet ` D ) y ) <_ ( ( z ( pstoMet ` D ) x ) +e ( z ( pstoMet ` D ) y ) ) )
82 81 adantl5r 
 |-  ( ( ( ( ( ( ( D e. ( PsMet ` X ) /\ y e. ( X /. .~ ) ) /\ z e. ( X /. .~ ) ) /\ a e. X ) /\ x = [ a ] .~ ) /\ b e. X ) /\ y = [ b ] .~ ) -> ( x ( pstoMet ` D ) y ) <_ ( ( z ( pstoMet ` D ) x ) +e ( z ( pstoMet ` D ) y ) ) )
83 24 ad4antlr 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ y e. ( X /. .~ ) ) /\ z e. ( X /. .~ ) ) /\ a e. X ) /\ x = [ a ] .~ ) -> E. b e. X y = [ b ] .~ )
84 82 83 r19.29a 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ y e. ( X /. .~ ) ) /\ z e. ( X /. .~ ) ) /\ a e. X ) /\ x = [ a ] .~ ) -> ( x ( pstoMet ` D ) y ) <_ ( ( z ( pstoMet ` D ) x ) +e ( z ( pstoMet ` D ) y ) ) )
85 84 adantl4r 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ x e. ( X /. .~ ) ) /\ y e. ( X /. .~ ) ) /\ z e. ( X /. .~ ) ) /\ a e. X ) /\ x = [ a ] .~ ) -> ( x ( pstoMet ` D ) y ) <_ ( ( z ( pstoMet ` D ) x ) +e ( z ( pstoMet ` D ) y ) ) )
86 28 ad3antlr 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ x e. ( X /. .~ ) ) /\ y e. ( X /. .~ ) ) /\ z e. ( X /. .~ ) ) -> E. a e. X x = [ a ] .~ )
87 85 86 r19.29a 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ x e. ( X /. .~ ) ) /\ y e. ( X /. .~ ) ) /\ z e. ( X /. .~ ) ) -> ( x ( pstoMet ` D ) y ) <_ ( ( z ( pstoMet ` D ) x ) +e ( z ( pstoMet ` D ) y ) ) )
88 87 ralrimiva 
 |-  ( ( ( D e. ( PsMet ` X ) /\ x e. ( X /. .~ ) ) /\ y e. ( X /. .~ ) ) -> A. z e. ( X /. .~ ) ( x ( pstoMet ` D ) y ) <_ ( ( z ( pstoMet ` D ) x ) +e ( z ( pstoMet ` D ) y ) ) )
89 88 anasss 
 |-  ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) -> A. z e. ( X /. .~ ) ( x ( pstoMet ` D ) y ) <_ ( ( z ( pstoMet ` D ) x ) +e ( z ( pstoMet ` D ) y ) ) )
90 55 89 jca 
 |-  ( ( D e. ( PsMet ` X ) /\ ( x e. ( X /. .~ ) /\ y e. ( X /. .~ ) ) ) -> ( ( ( x ( pstoMet ` D ) y ) = 0 <-> x = y ) /\ A. z e. ( X /. .~ ) ( x ( pstoMet ` D ) y ) <_ ( ( z ( pstoMet ` D ) x ) +e ( z ( pstoMet ` D ) y ) ) ) )
91 90 ralrimivva 
 |-  ( D e. ( PsMet ` X ) -> A. x e. ( X /. .~ ) A. y e. ( X /. .~ ) ( ( ( x ( pstoMet ` D ) y ) = 0 <-> x = y ) /\ A. z e. ( X /. .~ ) ( x ( pstoMet ` D ) y ) <_ ( ( z ( pstoMet ` D ) x ) +e ( z ( pstoMet ` D ) y ) ) ) )
92 elfvex 
 |-  ( D e. ( PsMet ` X ) -> X e. _V )
93 qsexg 
 |-  ( X e. _V -> ( X /. .~ ) e. _V )
94 isxmet 
 |-  ( ( X /. .~ ) e. _V -> ( ( pstoMet ` D ) e. ( *Met ` ( X /. .~ ) ) <-> ( ( pstoMet ` D ) : ( ( X /. .~ ) X. ( X /. .~ ) ) --> RR* /\ A. x e. ( X /. .~ ) A. y e. ( X /. .~ ) ( ( ( x ( pstoMet ` D ) y ) = 0 <-> x = y ) /\ A. z e. ( X /. .~ ) ( x ( pstoMet ` D ) y ) <_ ( ( z ( pstoMet ` D ) x ) +e ( z ( pstoMet ` D ) y ) ) ) ) ) )
95 92 93 94 3syl 
 |-  ( D e. ( PsMet ` X ) -> ( ( pstoMet ` D ) e. ( *Met ` ( X /. .~ ) ) <-> ( ( pstoMet ` D ) : ( ( X /. .~ ) X. ( X /. .~ ) ) --> RR* /\ A. x e. ( X /. .~ ) A. y e. ( X /. .~ ) ( ( ( x ( pstoMet ` D ) y ) = 0 <-> x = y ) /\ A. z e. ( X /. .~ ) ( x ( pstoMet ` D ) y ) <_ ( ( z ( pstoMet ` D ) x ) +e ( z ( pstoMet ` D ) y ) ) ) ) ) )
96 33 91 95 mpbir2and 
 |-  ( D e. ( PsMet ` X ) -> ( pstoMet ` D ) e. ( *Met ` ( X /. .~ ) ) )