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 e. ( PsMet ` X ) -> ( ~Met ` D ) Er X )

Proof

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