Metamath Proof Explorer

Theorem metider

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

Ref Expression
Assertion metider ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ~Met ‘ 𝐷 ) Er 𝑋 )

Proof

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