Metamath Proof Explorer


Theorem metideq

Description: Basic property of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion metideq ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐴 𝐷 𝐸 ) = ( 𝐵 𝐷 𝐹 ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
2 metidss ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ~Met𝐷 ) ⊆ ( 𝑋 × 𝑋 ) )
3 dmss ( ( ~Met𝐷 ) ⊆ ( 𝑋 × 𝑋 ) → dom ( ~Met𝐷 ) ⊆ dom ( 𝑋 × 𝑋 ) )
4 2 3 syl ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → dom ( ~Met𝐷 ) ⊆ dom ( 𝑋 × 𝑋 ) )
5 dmxpid dom ( 𝑋 × 𝑋 ) = 𝑋
6 4 5 sseqtrdi ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → dom ( ~Met𝐷 ) ⊆ 𝑋 )
7 1 6 syl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → dom ( ~Met𝐷 ) ⊆ 𝑋 )
8 xpss ( 𝑋 × 𝑋 ) ⊆ ( V × V )
9 2 8 sstrdi ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ~Met𝐷 ) ⊆ ( V × V ) )
10 df-rel ( Rel ( ~Met𝐷 ) ↔ ( ~Met𝐷 ) ⊆ ( V × V ) )
11 9 10 sylibr ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → Rel ( ~Met𝐷 ) )
12 1 11 syl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → Rel ( ~Met𝐷 ) )
13 simprl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → 𝐴 ( ~Met𝐷 ) 𝐵 )
14 releldm ( ( Rel ( ~Met𝐷 ) ∧ 𝐴 ( ~Met𝐷 ) 𝐵 ) → 𝐴 ∈ dom ( ~Met𝐷 ) )
15 12 13 14 syl2anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → 𝐴 ∈ dom ( ~Met𝐷 ) )
16 7 15 sseldd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → 𝐴𝑋 )
17 simprr ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → 𝐸 ( ~Met𝐷 ) 𝐹 )
18 releldm ( ( Rel ( ~Met𝐷 ) ∧ 𝐸 ( ~Met𝐷 ) 𝐹 ) → 𝐸 ∈ dom ( ~Met𝐷 ) )
19 12 17 18 syl2anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → 𝐸 ∈ dom ( ~Met𝐷 ) )
20 7 19 sseldd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → 𝐸𝑋 )
21 psmetsym ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐸𝑋 ) → ( 𝐴 𝐷 𝐸 ) = ( 𝐸 𝐷 𝐴 ) )
22 1 16 20 21 syl3anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐴 𝐷 𝐸 ) = ( 𝐸 𝐷 𝐴 ) )
23 psmetf ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
24 23 fovrnda ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐸𝑋𝐴𝑋 ) ) → ( 𝐸 𝐷 𝐴 ) ∈ ℝ* )
25 1 20 16 24 syl12anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐸 𝐷 𝐴 ) ∈ ℝ* )
26 22 25 eqeltrd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐴 𝐷 𝐸 ) ∈ ℝ* )
27 rnss ( ( ~Met𝐷 ) ⊆ ( 𝑋 × 𝑋 ) → ran ( ~Met𝐷 ) ⊆ ran ( 𝑋 × 𝑋 ) )
28 2 27 syl ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ran ( ~Met𝐷 ) ⊆ ran ( 𝑋 × 𝑋 ) )
29 rnxpid ran ( 𝑋 × 𝑋 ) = 𝑋
30 28 29 sseqtrdi ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ran ( ~Met𝐷 ) ⊆ 𝑋 )
31 1 30 syl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ran ( ~Met𝐷 ) ⊆ 𝑋 )
32 relelrn ( ( Rel ( ~Met𝐷 ) ∧ 𝐴 ( ~Met𝐷 ) 𝐵 ) → 𝐵 ∈ ran ( ~Met𝐷 ) )
33 12 13 32 syl2anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → 𝐵 ∈ ran ( ~Met𝐷 ) )
34 31 33 sseldd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → 𝐵𝑋 )
35 23 fovrnda ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐵𝑋𝐸𝑋 ) ) → ( 𝐵 𝐷 𝐸 ) ∈ ℝ* )
36 1 34 20 35 syl12anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐵 𝐷 𝐸 ) ∈ ℝ* )
37 relelrn ( ( Rel ( ~Met𝐷 ) ∧ 𝐸 ( ~Met𝐷 ) 𝐹 ) → 𝐹 ∈ ran ( ~Met𝐷 ) )
38 12 17 37 syl2anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → 𝐹 ∈ ran ( ~Met𝐷 ) )
39 31 38 sseldd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → 𝐹𝑋 )
40 psmetsym ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐹𝑋𝐵𝑋 ) → ( 𝐹 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐹 ) )
41 1 39 34 40 syl3anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐹 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐹 ) )
42 23 fovrnda ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐹𝑋𝐵𝑋 ) ) → ( 𝐹 𝐷 𝐵 ) ∈ ℝ* )
43 1 39 34 42 syl12anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐹 𝐷 𝐵 ) ∈ ℝ* )
44 41 43 eqeltrrd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐵 𝐷 𝐹 ) ∈ ℝ* )
45 psmettri2 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐵𝑋𝐴𝑋𝐸𝑋 ) ) → ( 𝐴 𝐷 𝐸 ) ≤ ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐵 𝐷 𝐸 ) ) )
46 1 34 16 20 45 syl13anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐴 𝐷 𝐸 ) ≤ ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐵 𝐷 𝐸 ) ) )
47 psmetsym ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) )
48 1 16 34 47 syl3anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) )
49 16 34 jca ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐴𝑋𝐵𝑋 ) )
50 metidv ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( 𝐴 ( ~Met𝐷 ) 𝐵 ↔ ( 𝐴 𝐷 𝐵 ) = 0 ) )
51 50 biimpa ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) ∧ 𝐴 ( ~Met𝐷 ) 𝐵 ) → ( 𝐴 𝐷 𝐵 ) = 0 )
52 1 49 13 51 syl21anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐴 𝐷 𝐵 ) = 0 )
53 48 52 eqtr3d ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐵 𝐷 𝐴 ) = 0 )
54 53 oveq1d ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐵 𝐷 𝐸 ) ) = ( 0 +𝑒 ( 𝐵 𝐷 𝐸 ) ) )
55 xaddid2 ( ( 𝐵 𝐷 𝐸 ) ∈ ℝ* → ( 0 +𝑒 ( 𝐵 𝐷 𝐸 ) ) = ( 𝐵 𝐷 𝐸 ) )
56 36 55 syl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 0 +𝑒 ( 𝐵 𝐷 𝐸 ) ) = ( 𝐵 𝐷 𝐸 ) )
57 54 56 eqtrd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐵 𝐷 𝐸 ) ) = ( 𝐵 𝐷 𝐸 ) )
58 46 57 breqtrd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐴 𝐷 𝐸 ) ≤ ( 𝐵 𝐷 𝐸 ) )
59 psmettri2 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐹𝑋𝐵𝑋𝐸𝑋 ) ) → ( 𝐵 𝐷 𝐸 ) ≤ ( ( 𝐹 𝐷 𝐵 ) +𝑒 ( 𝐹 𝐷 𝐸 ) ) )
60 1 39 34 20 59 syl13anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐵 𝐷 𝐸 ) ≤ ( ( 𝐹 𝐷 𝐵 ) +𝑒 ( 𝐹 𝐷 𝐸 ) ) )
61 psmetsym ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐹𝑋𝐸𝑋 ) → ( 𝐹 𝐷 𝐸 ) = ( 𝐸 𝐷 𝐹 ) )
62 1 39 20 61 syl3anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐹 𝐷 𝐸 ) = ( 𝐸 𝐷 𝐹 ) )
63 20 39 jca ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐸𝑋𝐹𝑋 ) )
64 metidv ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐸𝑋𝐹𝑋 ) ) → ( 𝐸 ( ~Met𝐷 ) 𝐹 ↔ ( 𝐸 𝐷 𝐹 ) = 0 ) )
65 64 biimpa ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐸𝑋𝐹𝑋 ) ) ∧ 𝐸 ( ~Met𝐷 ) 𝐹 ) → ( 𝐸 𝐷 𝐹 ) = 0 )
66 1 63 17 65 syl21anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐸 𝐷 𝐹 ) = 0 )
67 62 66 eqtrd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐹 𝐷 𝐸 ) = 0 )
68 67 oveq2d ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( ( 𝐹 𝐷 𝐵 ) +𝑒 ( 𝐹 𝐷 𝐸 ) ) = ( ( 𝐹 𝐷 𝐵 ) +𝑒 0 ) )
69 xaddid1 ( ( 𝐹 𝐷 𝐵 ) ∈ ℝ* → ( ( 𝐹 𝐷 𝐵 ) +𝑒 0 ) = ( 𝐹 𝐷 𝐵 ) )
70 43 69 syl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( ( 𝐹 𝐷 𝐵 ) +𝑒 0 ) = ( 𝐹 𝐷 𝐵 ) )
71 68 70 41 3eqtrd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( ( 𝐹 𝐷 𝐵 ) +𝑒 ( 𝐹 𝐷 𝐸 ) ) = ( 𝐵 𝐷 𝐹 ) )
72 60 71 breqtrd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐵 𝐷 𝐸 ) ≤ ( 𝐵 𝐷 𝐹 ) )
73 26 36 44 58 72 xrletrd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐴 𝐷 𝐸 ) ≤ ( 𝐵 𝐷 𝐹 ) )
74 23 fovrnda ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐹𝑋 ) ) → ( 𝐴 𝐷 𝐹 ) ∈ ℝ* )
75 1 16 39 74 syl12anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐴 𝐷 𝐹 ) ∈ ℝ* )
76 psmettri2 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐹𝑋 ) ) → ( 𝐵 𝐷 𝐹 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐹 ) ) )
77 1 16 34 39 76 syl13anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐵 𝐷 𝐹 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐹 ) ) )
78 52 oveq1d ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐹 ) ) = ( 0 +𝑒 ( 𝐴 𝐷 𝐹 ) ) )
79 xaddid2 ( ( 𝐴 𝐷 𝐹 ) ∈ ℝ* → ( 0 +𝑒 ( 𝐴 𝐷 𝐹 ) ) = ( 𝐴 𝐷 𝐹 ) )
80 75 79 syl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 0 +𝑒 ( 𝐴 𝐷 𝐹 ) ) = ( 𝐴 𝐷 𝐹 ) )
81 78 80 eqtrd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐹 ) ) = ( 𝐴 𝐷 𝐹 ) )
82 77 81 breqtrd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐵 𝐷 𝐹 ) ≤ ( 𝐴 𝐷 𝐹 ) )
83 psmettri2 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐸𝑋𝐴𝑋𝐹𝑋 ) ) → ( 𝐴 𝐷 𝐹 ) ≤ ( ( 𝐸 𝐷 𝐴 ) +𝑒 ( 𝐸 𝐷 𝐹 ) ) )
84 1 20 16 39 83 syl13anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐴 𝐷 𝐹 ) ≤ ( ( 𝐸 𝐷 𝐴 ) +𝑒 ( 𝐸 𝐷 𝐹 ) ) )
85 xaddid1 ( ( 𝐸 𝐷 𝐴 ) ∈ ℝ* → ( ( 𝐸 𝐷 𝐴 ) +𝑒 0 ) = ( 𝐸 𝐷 𝐴 ) )
86 25 85 syl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( ( 𝐸 𝐷 𝐴 ) +𝑒 0 ) = ( 𝐸 𝐷 𝐴 ) )
87 66 oveq2d ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( ( 𝐸 𝐷 𝐴 ) +𝑒 ( 𝐸 𝐷 𝐹 ) ) = ( ( 𝐸 𝐷 𝐴 ) +𝑒 0 ) )
88 86 87 22 3eqtr4d ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( ( 𝐸 𝐷 𝐴 ) +𝑒 ( 𝐸 𝐷 𝐹 ) ) = ( 𝐴 𝐷 𝐸 ) )
89 84 88 breqtrd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐴 𝐷 𝐹 ) ≤ ( 𝐴 𝐷 𝐸 ) )
90 44 75 26 82 89 xrletrd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐵 𝐷 𝐹 ) ≤ ( 𝐴 𝐷 𝐸 ) )
91 xrletri3 ( ( ( 𝐴 𝐷 𝐸 ) ∈ ℝ* ∧ ( 𝐵 𝐷 𝐹 ) ∈ ℝ* ) → ( ( 𝐴 𝐷 𝐸 ) = ( 𝐵 𝐷 𝐹 ) ↔ ( ( 𝐴 𝐷 𝐸 ) ≤ ( 𝐵 𝐷 𝐹 ) ∧ ( 𝐵 𝐷 𝐹 ) ≤ ( 𝐴 𝐷 𝐸 ) ) ) )
92 26 44 91 syl2anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( ( 𝐴 𝐷 𝐸 ) = ( 𝐵 𝐷 𝐹 ) ↔ ( ( 𝐴 𝐷 𝐸 ) ≤ ( 𝐵 𝐷 𝐹 ) ∧ ( 𝐵 𝐷 𝐹 ) ≤ ( 𝐴 𝐷 𝐸 ) ) ) )
93 73 90 92 mpbir2and ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ( ~Met𝐷 ) 𝐵𝐸 ( ~Met𝐷 ) 𝐹 ) ) → ( 𝐴 𝐷 𝐸 ) = ( 𝐵 𝐷 𝐹 ) )