Metamath Proof Explorer


Theorem metider

Description: The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion metider D PsMet X ~ Met D Er X

Proof

Step Hyp Ref Expression
1 metidss D PsMet X ~ Met D X × X
2 xpss X × X V × V
3 1 2 sstrdi D PsMet X ~ Met D V × V
4 df-rel Rel ~ Met D ~ Met D V × V
5 3 4 sylibr D PsMet X Rel ~ Met D
6 1 ssbrd D PsMet X x ~ Met D y x X × X y
7 6 imp D PsMet X x ~ Met D y x X × X y
8 brxp x X × X y x X y X
9 7 8 sylib D PsMet X x ~ Met D y x X y X
10 psmetsym D PsMet X x X y X x D y = y D x
11 10 3expb D PsMet X x X y X x D y = y D x
12 11 eqeq1d D PsMet X x X y X x D y = 0 y D x = 0
13 metidv D PsMet X x X y X x ~ Met D y x D y = 0
14 metidv D PsMet X y X x X y ~ Met D x y D x = 0
15 14 ancom2s D PsMet X x X y X y ~ Met D x y D x = 0
16 12 13 15 3bitr4d D PsMet X x X y X x ~ Met D y y ~ Met D x
17 16 biimpd D PsMet X x X y X x ~ Met D y y ~ Met D x
18 17 impancom D PsMet X x ~ Met D y x X y X y ~ Met D x
19 9 18 mpd D PsMet X x ~ Met D y y ~ Met D x
20 simpl D PsMet X x ~ Met D y y ~ Met D z D PsMet X
21 simprr D PsMet X x ~ Met D y y ~ Met D z y ~ Met D z
22 1 ssbrd D PsMet X y ~ Met D z y X × X z
23 22 imp D PsMet X y ~ Met D z y X × X z
24 brxp y X × X z y X z X
25 23 24 sylib D PsMet X y ~ Met D z y X z X
26 21 25 syldan D PsMet X x ~ Met D y y ~ Met D z y X z X
27 26 simpld D PsMet X x ~ Met D y y ~ Met D z y X
28 simprl D PsMet X x ~ Met D y y ~ Met D z x ~ Met D y
29 28 9 syldan D PsMet X x ~ Met D y y ~ Met D z x X y X
30 29 simpld D PsMet X x ~ Met D y y ~ Met D z x X
31 26 simprd D PsMet X x ~ Met D y y ~ Met D z z X
32 psmettri2 D PsMet X y X x X z X x D z y D x + 𝑒 y D z
33 20 27 30 31 32 syl13anc D PsMet X x ~ Met D y y ~ Met D z x D z y D x + 𝑒 y D z
34 29 11 syldan D PsMet X x ~ Met D y y ~ Met D z x D y = y D x
35 29 13 syldan D PsMet X x ~ Met D y y ~ Met D z x ~ Met D y x D y = 0
36 28 35 mpbid D PsMet X x ~ Met D y y ~ Met D z x D y = 0
37 34 36 eqtr3d D PsMet X x ~ Met D y y ~ Met D z y D x = 0
38 metidv D PsMet X y X z X y ~ Met D z y D z = 0
39 26 38 syldan D PsMet X x ~ Met D y y ~ Met D z y ~ Met D z y D z = 0
40 21 39 mpbid D PsMet X x ~ Met D y y ~ Met D z y D z = 0
41 37 40 oveq12d D PsMet X x ~ Met D y y ~ Met D z y D x + 𝑒 y D z = 0 + 𝑒 0
42 0xr 0 *
43 xaddid1 0 * 0 + 𝑒 0 = 0
44 42 43 ax-mp 0 + 𝑒 0 = 0
45 41 44 eqtrdi D PsMet X x ~ Met D y y ~ Met D z y D x + 𝑒 y D z = 0
46 33 45 breqtrd D PsMet X x ~ Met D y y ~ Met D z x D z 0
47 psmetge0 D PsMet X x X z X 0 x D z
48 20 30 31 47 syl3anc D PsMet X x ~ Met D y y ~ Met D z 0 x D z
49 psmetcl D PsMet X x X z X x D z *
50 20 30 31 49 syl3anc D PsMet X x ~ Met D y y ~ Met D z x D z *
51 xrletri3 x D z * 0 * x D z = 0 x D z 0 0 x D z
52 50 42 51 sylancl D PsMet X x ~ Met D y y ~ Met D z x D z = 0 x D z 0 0 x D z
53 46 48 52 mpbir2and D PsMet X x ~ Met D y y ~ Met D z x D z = 0
54 metidv D PsMet X x X z X x ~ Met D z x D z = 0
55 20 30 31 54 syl12anc D PsMet X x ~ Met D y y ~ Met D z x ~ Met D z x D z = 0
56 53 55 mpbird D PsMet X x ~ Met D y y ~ Met D z x ~ Met D z
57 psmet0 D PsMet X x X x D x = 0
58 metidv D PsMet X x X x X x ~ Met D x x D x = 0
59 58 anabsan2 D PsMet X x X x ~ Met D x x D x = 0
60 57 59 mpbird D PsMet X x X x ~ Met D x
61 1 ssbrd D PsMet X x ~ Met D x x X × X x
62 61 imp D PsMet X x ~ Met D x x X × X x
63 brxp x X × X x x X x X
64 62 63 sylib D PsMet X x ~ Met D x x X x X
65 64 simpld D PsMet X x ~ Met D x x X
66 60 65 impbida D PsMet X x X x ~ Met D x
67 5 19 56 66 iserd D PsMet X ~ Met D Er X