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⁡DB∧E~Met⁡DF→ADE=BDF

Proof

Step Hyp Ref Expression
1 simpl ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→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⁡DB∧E~Met⁡DF→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⁡DB∧E~Met⁡DF→Rel⁡~Met⁡D
13 simprl ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→A~Met⁡DB
14 releldm ⊢Rel⁡~Met⁡D∧A~Met⁡DB→A∈dom⁡~Met⁡D
15 12 13 14 syl2anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→A∈dom⁡~Met⁡D
16 7 15 sseldd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→A∈X
17 simprr ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→E~Met⁡DF
18 releldm ⊢Rel⁡~Met⁡D∧E~Met⁡DF→E∈dom⁡~Met⁡D
19 12 17 18 syl2anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→E∈dom⁡~Met⁡D
20 7 19 sseldd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→E∈X
21 psmetsym ⊢D∈PsMet⁡X∧A∈X∧E∈X→ADE=EDA
22 1 16 20 21 syl3anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→ADE=EDA
23 psmetf ⊢D∈PsMet⁡X→D:X×X⟶ℝ*
24 23 fovcdmda ⊢D∈PsMet⁡X∧E∈X∧A∈X→EDA∈ℝ*
25 1 20 16 24 syl12anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→EDA∈ℝ*
26 22 25 eqeltrd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→ADE∈ℝ*
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⁡DB∧E~Met⁡DF→ran⁡~Met⁡D⊆X
32 relelrn ⊢Rel⁡~Met⁡D∧A~Met⁡DB→B∈ran⁡~Met⁡D
33 12 13 32 syl2anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→B∈ran⁡~Met⁡D
34 31 33 sseldd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→B∈X
35 23 fovcdmda ⊢D∈PsMet⁡X∧B∈X∧E∈X→BDE∈ℝ*
36 1 34 20 35 syl12anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→BDE∈ℝ*
37 relelrn ⊢Rel⁡~Met⁡D∧E~Met⁡DF→F∈ran⁡~Met⁡D
38 12 17 37 syl2anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→F∈ran⁡~Met⁡D
39 31 38 sseldd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→F∈X
40 psmetsym ⊢D∈PsMet⁡X∧F∈X∧B∈X→FDB=BDF
41 1 39 34 40 syl3anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→FDB=BDF
42 23 fovcdmda ⊢D∈PsMet⁡X∧F∈X∧B∈X→FDB∈ℝ*
43 1 39 34 42 syl12anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→FDB∈ℝ*
44 41 43 eqeltrrd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→BDF∈ℝ*
45 psmettri2 ⊢D∈PsMet⁡X∧B∈X∧A∈X∧E∈X→ADE≤BDA+𝑒BDE
46 1 34 16 20 45 syl13anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→ADE≤BDA+𝑒BDE
47 psmetsym ⊢D∈PsMet⁡X∧A∈X∧B∈X→ADB=BDA
48 1 16 34 47 syl3anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→ADB=BDA
49 16 34 jca ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→A∈X∧B∈X
50 metidv ⊢D∈PsMet⁡X∧A∈X∧B∈X→A~Met⁡DB↔ADB=0
51 50 biimpa ⊢D∈PsMet⁡X∧A∈X∧B∈X∧A~Met⁡DB→ADB=0
52 1 49 13 51 syl21anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→ADB=0
53 48 52 eqtr3d ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→BDA=0
54 53 oveq1d ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→BDA+𝑒BDE=0+𝑒BDE
55 xaddlid ⊢BDE∈ℝ*→0+𝑒BDE=BDE
56 36 55 syl ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→0+𝑒BDE=BDE
57 54 56 eqtrd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→BDA+𝑒BDE=BDE
58 46 57 breqtrd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→ADE≤BDE
59 psmettri2 ⊢D∈PsMet⁡X∧F∈X∧B∈X∧E∈X→BDE≤FDB+𝑒FDE
60 1 39 34 20 59 syl13anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→BDE≤FDB+𝑒FDE
61 psmetsym ⊢D∈PsMet⁡X∧F∈X∧E∈X→FDE=EDF
62 1 39 20 61 syl3anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→FDE=EDF
63 20 39 jca ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→E∈X∧F∈X
64 metidv ⊢D∈PsMet⁡X∧E∈X∧F∈X→E~Met⁡DF↔EDF=0
65 64 biimpa ⊢D∈PsMet⁡X∧E∈X∧F∈X∧E~Met⁡DF→EDF=0
66 1 63 17 65 syl21anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→EDF=0
67 62 66 eqtrd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→FDE=0
68 67 oveq2d ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→FDB+𝑒FDE=FDB+𝑒0
69 xaddrid ⊢FDB∈ℝ*→FDB+𝑒0=FDB
70 43 69 syl ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→FDB+𝑒0=FDB
71 68 70 41 3eqtrd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→FDB+𝑒FDE=BDF
72 60 71 breqtrd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→BDE≤BDF
73 26 36 44 58 72 xrletrd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→ADE≤BDF
74 23 fovcdmda ⊢D∈PsMet⁡X∧A∈X∧F∈X→ADF∈ℝ*
75 1 16 39 74 syl12anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→ADF∈ℝ*
76 psmettri2 ⊢D∈PsMet⁡X∧A∈X∧B∈X∧F∈X→BDF≤ADB+𝑒ADF
77 1 16 34 39 76 syl13anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→BDF≤ADB+𝑒ADF
78 52 oveq1d ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→ADB+𝑒ADF=0+𝑒ADF
79 xaddlid ⊢ADF∈ℝ*→0+𝑒ADF=ADF
80 75 79 syl ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→0+𝑒ADF=ADF
81 78 80 eqtrd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→ADB+𝑒ADF=ADF
82 77 81 breqtrd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→BDF≤ADF
83 psmettri2 ⊢D∈PsMet⁡X∧E∈X∧A∈X∧F∈X→ADF≤EDA+𝑒EDF
84 1 20 16 39 83 syl13anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→ADF≤EDA+𝑒EDF
85 xaddrid ⊢EDA∈ℝ*→EDA+𝑒0=EDA
86 25 85 syl ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→EDA+𝑒0=EDA
87 66 oveq2d ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→EDA+𝑒EDF=EDA+𝑒0
88 86 87 22 3eqtr4d ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→EDA+𝑒EDF=ADE
89 84 88 breqtrd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→ADF≤ADE
90 44 75 26 82 89 xrletrd ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→BDF≤ADE
91 xrletri3 ⊢ADE∈ℝ*∧BDF∈ℝ*→ADE=BDF↔ADE≤BDF∧BDF≤ADE
92 26 44 91 syl2anc ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→ADE=BDF↔ADE≤BDF∧BDF≤ADE
93 73 90 92 mpbir2and ⊢D∈PsMet⁡X∧A~Met⁡DB∧E~Met⁡DF→ADE=BDF