Metamath Proof Explorer

Theorem metideq

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

Ref Expression
Assertion metideq ⊢ D ∈ PsMet ⁡ X ∧ A ~ Met ⁡ D B ∧ E ~ Met ⁡ D F → A D E = B D F

Proof

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