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𝐷 )
Assertion pstmxmet ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( pstoMet ‘ 𝐷 ) ∈ ( ∞Met ‘ ( 𝑋 / ) ) )

Proof

Step Hyp Ref Expression
1 pstmval.1 = ( ~Met𝐷 )
2 eqid ( 𝑥 ∈ ( 𝑋 / ) , 𝑦 ∈ ( 𝑋 / ) ↦ { 𝑧 ∣ ∃ 𝑎𝑥𝑏𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ) = ( 𝑥 ∈ ( 𝑋 / ) , 𝑦 ∈ ( 𝑋 / ) ↦ { 𝑧 ∣ ∃ 𝑎𝑥𝑏𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } )
3 vex 𝑥 ∈ V
4 vex 𝑦 ∈ V
5 3 4 ab2rexex { 𝑧 ∣ ∃ 𝑎𝑥𝑏𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ∈ V
6 5 uniex { 𝑧 ∣ ∃ 𝑎𝑥𝑏𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ∈ V
7 2 6 fnmpoi ( 𝑥 ∈ ( 𝑋 / ) , 𝑦 ∈ ( 𝑋 / ) ↦ { 𝑧 ∣ ∃ 𝑎𝑥𝑏𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ) Fn ( ( 𝑋 / ) × ( 𝑋 / ) )
8 1 pstmval ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( pstoMet ‘ 𝐷 ) = ( 𝑥 ∈ ( 𝑋 / ) , 𝑦 ∈ ( 𝑋 / ) ↦ { 𝑧 ∣ ∃ 𝑎𝑥𝑏𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ) )
9 8 fneq1d ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ( pstoMet ‘ 𝐷 ) Fn ( ( 𝑋 / ) × ( 𝑋 / ) ) ↔ ( 𝑥 ∈ ( 𝑋 / ) , 𝑦 ∈ ( 𝑋 / ) ↦ { 𝑧 ∣ ∃ 𝑎𝑥𝑏𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ) Fn ( ( 𝑋 / ) × ( 𝑋 / ) ) ) )
10 7 9 mpbiri ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( pstoMet ‘ 𝐷 ) Fn ( ( 𝑋 / ) × ( 𝑋 / ) ) )
11 simpllr ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → 𝑥 = [ 𝑎 ] )
12 simpr ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → 𝑦 = [ 𝑏 ] )
13 11 12 oveq12d ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = ( [ 𝑎 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) )
14 simp-5l ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
15 simp-4r ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → 𝑎𝑋 )
16 simplr ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → 𝑏𝑋 )
17 1 pstmfval ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋𝑏𝑋 ) → ( [ 𝑎 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) = ( 𝑎 𝐷 𝑏 ) )
18 14 15 16 17 syl3anc ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → ( [ 𝑎 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) = ( 𝑎 𝐷 𝑏 ) )
19 13 18 eqtrd ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = ( 𝑎 𝐷 𝑏 ) )
20 psmetf ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
21 14 20 syl ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
22 21 15 16 fovrnd ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → ( 𝑎 𝐷 𝑏 ) ∈ ℝ* )
23 19 22 eqeltrd ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ∈ ℝ* )
24 elqsi ( 𝑦 ∈ ( 𝑋 / ) → ∃ 𝑏𝑋 𝑦 = [ 𝑏 ] )
25 24 ad2antll ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) → ∃ 𝑏𝑋 𝑦 = [ 𝑏 ] )
26 25 ad2antrr ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) → ∃ 𝑏𝑋 𝑦 = [ 𝑏 ] )
27 23 26 r19.29a ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ∈ ℝ* )
28 elqsi ( 𝑥 ∈ ( 𝑋 / ) → ∃ 𝑎𝑋 𝑥 = [ 𝑎 ] )
29 28 ad2antrl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) → ∃ 𝑎𝑋 𝑥 = [ 𝑎 ] )
30 27 29 r19.29a ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ∈ ℝ* )
31 30 ralrimivva ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑥 ∈ ( 𝑋 / ) ∀ 𝑦 ∈ ( 𝑋 / ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ∈ ℝ* )
32 ffnov ( ( pstoMet ‘ 𝐷 ) : ( ( 𝑋 / ) × ( 𝑋 / ) ) ⟶ ℝ* ↔ ( ( pstoMet ‘ 𝐷 ) Fn ( ( 𝑋 / ) × ( 𝑋 / ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 / ) ∀ 𝑦 ∈ ( 𝑋 / ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ∈ ℝ* ) )
33 10 31 32 sylanbrc ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( pstoMet ‘ 𝐷 ) : ( ( 𝑋 / ) × ( 𝑋 / ) ) ⟶ ℝ* )
34 17 3expa ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑏𝑋 ) → ( [ 𝑎 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) = ( 𝑎 𝐷 𝑏 ) )
35 34 eqeq1d ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑏𝑋 ) → ( ( [ 𝑎 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) = 0 ↔ ( 𝑎 𝐷 𝑏 ) = 0 ) )
36 1 breqi ( 𝑎 𝑏𝑎 ( ~Met𝐷 ) 𝑏 )
37 metidv ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑎𝑋𝑏𝑋 ) ) → ( 𝑎 ( ~Met𝐷 ) 𝑏 ↔ ( 𝑎 𝐷 𝑏 ) = 0 ) )
38 37 anassrs ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑏𝑋 ) → ( 𝑎 ( ~Met𝐷 ) 𝑏 ↔ ( 𝑎 𝐷 𝑏 ) = 0 ) )
39 36 38 syl5bb ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑏𝑋 ) → ( 𝑎 𝑏 ↔ ( 𝑎 𝐷 𝑏 ) = 0 ) )
40 metider ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ~Met𝐷 ) Er 𝑋 )
41 40 ad2antrr ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑏𝑋 ) → ( ~Met𝐷 ) Er 𝑋 )
42 ereq1 ( = ( ~Met𝐷 ) → ( Er 𝑋 ↔ ( ~Met𝐷 ) Er 𝑋 ) )
43 1 42 ax-mp ( Er 𝑋 ↔ ( ~Met𝐷 ) Er 𝑋 )
44 41 43 sylibr ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑏𝑋 ) → Er 𝑋 )
45 simplr ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑏𝑋 ) → 𝑎𝑋 )
46 44 45 erth ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑏𝑋 ) → ( 𝑎 𝑏 ↔ [ 𝑎 ] = [ 𝑏 ] ) )
47 35 39 46 3bitr2d ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑏𝑋 ) → ( ( [ 𝑎 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) = 0 ↔ [ 𝑎 ] = [ 𝑏 ] ) )
48 47 adantllr ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑏𝑋 ) → ( ( [ 𝑎 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) = 0 ↔ [ 𝑎 ] = [ 𝑏 ] ) )
49 48 adantlr ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) → ( ( [ 𝑎 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) = 0 ↔ [ 𝑎 ] = [ 𝑏 ] ) )
50 49 adantr ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → ( ( [ 𝑎 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) = 0 ↔ [ 𝑎 ] = [ 𝑏 ] ) )
51 13 eqeq1d ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ ( [ 𝑎 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) = 0 ) )
52 11 12 eqeq12d ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → ( 𝑥 = 𝑦 ↔ [ 𝑎 ] = [ 𝑏 ] ) )
53 50 51 52 3bitr4d ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
54 53 26 r19.29a ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) → ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
55 54 29 r19.29a ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) → ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
56 simp-6l ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
57 simplr ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → 𝑐𝑋 )
58 simp-6r ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → 𝑎𝑋 )
59 simp-4r ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → 𝑏𝑋 )
60 psmettri2 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑐𝑋𝑎𝑋𝑏𝑋 ) ) → ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) )
61 56 57 58 59 60 syl13anc ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) )
62 simp-5r ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → 𝑥 = [ 𝑎 ] )
63 simpllr ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → 𝑦 = [ 𝑏 ] )
64 62 63 oveq12d ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = ( [ 𝑎 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) )
65 56 58 59 17 syl3anc ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → ( [ 𝑎 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) = ( 𝑎 𝐷 𝑏 ) )
66 64 65 eqtrd ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = ( 𝑎 𝐷 𝑏 ) )
67 simpr ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → 𝑧 = [ 𝑐 ] )
68 67 62 oveq12d ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) = ( [ 𝑐 ] ( pstoMet ‘ 𝐷 ) [ 𝑎 ] ) )
69 1 pstmfval ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑐𝑋𝑎𝑋 ) → ( [ 𝑐 ] ( pstoMet ‘ 𝐷 ) [ 𝑎 ] ) = ( 𝑐 𝐷 𝑎 ) )
70 56 57 58 69 syl3anc ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → ( [ 𝑐 ] ( pstoMet ‘ 𝐷 ) [ 𝑎 ] ) = ( 𝑐 𝐷 𝑎 ) )
71 68 70 eqtrd ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) = ( 𝑐 𝐷 𝑎 ) )
72 67 63 oveq12d ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) = ( [ 𝑐 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) )
73 1 pstmfval ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑐𝑋𝑏𝑋 ) → ( [ 𝑐 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) = ( 𝑐 𝐷 𝑏 ) )
74 56 57 59 73 syl3anc ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → ( [ 𝑐 ] ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ) = ( 𝑐 𝐷 𝑏 ) )
75 72 74 eqtrd ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) = ( 𝑐 𝐷 𝑏 ) )
76 71 75 oveq12d ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) = ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) )
77 61 66 76 3brtr4d ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
78 77 adantl6r ( ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 / ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) ∧ 𝑐𝑋 ) ∧ 𝑧 = [ 𝑐 ] ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
79 elqsi ( 𝑧 ∈ ( 𝑋 / ) → ∃ 𝑐𝑋 𝑧 = [ 𝑐 ] )
80 79 ad5antlr ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 / ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → ∃ 𝑐𝑋 𝑧 = [ 𝑐 ] )
81 78 80 r19.29a ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 / ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
82 81 adantl5r ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ∧ 𝑧 ∈ ( 𝑋 / ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) ∧ 𝑏𝑋 ) ∧ 𝑦 = [ 𝑏 ] ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
83 24 ad4antlr ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ∧ 𝑧 ∈ ( 𝑋 / ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) → ∃ 𝑏𝑋 𝑦 = [ 𝑏 ] )
84 82 83 r19.29a ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ∧ 𝑧 ∈ ( 𝑋 / ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
85 84 adantl4r ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝑋 / ) ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ∧ 𝑧 ∈ ( 𝑋 / ) ) ∧ 𝑎𝑋 ) ∧ 𝑥 = [ 𝑎 ] ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
86 28 ad3antlr ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝑋 / ) ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ∧ 𝑧 ∈ ( 𝑋 / ) ) → ∃ 𝑎𝑋 𝑥 = [ 𝑎 ] )
87 85 86 r19.29a ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝑋 / ) ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ∧ 𝑧 ∈ ( 𝑋 / ) ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
88 87 ralrimiva ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝑋 / ) ) ∧ 𝑦 ∈ ( 𝑋 / ) ) → ∀ 𝑧 ∈ ( 𝑋 / ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
89 88 anasss ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) → ∀ 𝑧 ∈ ( 𝑋 / ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
90 55 89 jca ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ) ∧ 𝑦 ∈ ( 𝑋 / ) ) ) → ( ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ ( 𝑋 / ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) ) )
91 90 ralrimivva ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑥 ∈ ( 𝑋 / ) ∀ 𝑦 ∈ ( 𝑋 / ) ( ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ ( 𝑋 / ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) ) )
92 elfvex ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
93 qsexg ( 𝑋 ∈ V → ( 𝑋 / ) ∈ V )
94 isxmet ( ( 𝑋 / ) ∈ V → ( ( pstoMet ‘ 𝐷 ) ∈ ( ∞Met ‘ ( 𝑋 / ) ) ↔ ( ( pstoMet ‘ 𝐷 ) : ( ( 𝑋 / ) × ( 𝑋 / ) ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ ( 𝑋 / ) ∀ 𝑦 ∈ ( 𝑋 / ) ( ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ ( 𝑋 / ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) ) ) ) )
95 92 93 94 3syl ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ( pstoMet ‘ 𝐷 ) ∈ ( ∞Met ‘ ( 𝑋 / ) ) ↔ ( ( pstoMet ‘ 𝐷 ) : ( ( 𝑋 / ) × ( 𝑋 / ) ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ ( 𝑋 / ) ∀ 𝑦 ∈ ( 𝑋 / ) ( ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ ( 𝑋 / ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) ) ) ) )
96 33 91 95 mpbir2and ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( pstoMet ‘ 𝐷 ) ∈ ( ∞Met ‘ ( 𝑋 / ) ) )