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 e. ( PsMet ` X ) /\ ( A ( ~Met ` D ) B /\ E ( ~Met ` D ) F ) ) -> ( A D E ) = ( B D F ) )

Proof

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