Theorem metider 28577

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

Assertion

Ref	Expression
metider	|- ( D e. (PsMet ` X ) -> (~Met ` D ) Er X )

Proof of Theorem metider

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		metidss 28574	. . . 4 |- ( D e. (PsMet ` X ) -> (~Met ` D ) C_ ( X X. X ) )
2		xpss 4952	. . . 4 |- ( X X. X ) C_ ( _V X. _V )
3	1, 2	syl6ss 3473	. . 3 |- ( D e. (PsMet ` X ) -> (~Met ` D ) C_ ( _V X. _V ) )
4		df-rel 4852	. . 3 |- ( Rel (~Met ` D ) <-> (~Met ` D ) C_ ( _V X. _V ) )
5	3, 4	sylibr 215	. 2 |- ( D e. (PsMet ` X ) -> Rel (~Met ` D ) )
6	1	ssbrd 4458	. . . . 5 |- ( D e. (PsMet ` X ) -> ( x (~Met ` D ) y -> x ( X X. X ) y ) )
7	6	imp 430	. . . 4 |- ( ( D e. (PsMet ` X ) /\ x (~Met ` D ) y ) -> x ( X X. X ) y )
8		brxp 4876	. . . 4 |- ( x ( X X. X ) y <-> ( x e. X /\ y e. X ) )
9	7, 8	sylib 199	. . 3 |- ( ( D e. (PsMet ` X ) /\ x (~Met ` D ) y ) -> ( x e. X /\ y e. X ) )
10		psmetsym 21263	. . . . . . . 8 |- ( ( D e. (PsMet ` X ) /\ x e. X /\ y e. X ) -> ( x D y ) = ( y D x ) )
11	10	3expb 1206	. . . . . . 7 |- ( ( D e. (PsMet ` X ) /\ ( x e. X /\ y e. X ) ) -> ( x D y ) = ( y D x ) )
12	11	eqeq1d 2422	. . . . . 6 |- ( ( D e. (PsMet ` X ) /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) = 0 <-> ( y D x ) = 0 ) )
13		metidv 28575	. . . . . 6 |- ( ( D e. (PsMet ` X ) /\ ( x e. X /\ y e. X ) ) -> ( x (~Met ` D ) y <-> ( x D y ) = 0 ) )
14		metidv 28575	. . . . . . 7 |- ( ( D e. (PsMet ` X ) /\ ( y e. X /\ x e. X ) ) -> ( y (~Met ` D ) x <-> ( y D x ) = 0 ) )
15	14	ancom2s 809	. . . . . 6 |- ( ( D e. (PsMet ` X ) /\ ( x e. X /\ y e. X ) ) -> ( y (~Met ` D ) x <-> ( y D x ) = 0 ) )
16	12, 13, 15	3bitr4d 288	. . . . 5 |- ( ( D e. (PsMet ` X ) /\ ( x e. X /\ y e. X ) ) -> ( x (~Met ` D ) y <-> y (~Met ` D ) x ) )
17	16	biimpd 210	. . . 4 |- ( ( D e. (PsMet ` X ) /\ ( x e. X /\ y e. X ) ) -> ( x (~Met ` D ) y -> y (~Met ` D ) x ) )
18	17	impancom 441	. . 3 |- ( ( D e. (PsMet ` X ) /\ x (~Met ` D ) y ) -> ( ( x e. X /\ y e. X ) -> y (~Met ` D ) x ) )
19	9, 18	mpd 15	. 2 |- ( ( D e. (PsMet ` X ) /\ x (~Met ` D ) y ) -> y (~Met ` D ) x )
20		simpl 458	. . . . . 6 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> D e. (PsMet ` X ) )
21		simprr 764	. . . . . . . 8 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> y (~Met ` D ) z )
22	1	ssbrd 4458	. . . . . . . . . 10 |- ( D e. (PsMet ` X ) -> ( y (~Met ` D ) z -> y ( X X. X ) z ) )
23	22	imp 430	. . . . . . . . 9 |- ( ( D e. (PsMet ` X ) /\ y (~Met ` D ) z ) -> y ( X X. X ) z )
24		brxp 4876	. . . . . . . . 9 |- ( y ( X X. X ) z <-> ( y e. X /\ z e. X ) )
25	23, 24	sylib 199	. . . . . . . 8 |- ( ( D e. (PsMet ` X ) /\ y (~Met ` D ) z ) -> ( y e. X /\ z e. X ) )
26	21, 25	syldan 472	. . . . . . 7 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> ( y e. X /\ z e. X ) )
27	26	simpld 460	. . . . . 6 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> y e. X )
28		simprl 762	. . . . . . . 8 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> x (~Met ` D ) y )
29	28, 9	syldan 472	. . . . . . 7 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> ( x e. X /\ y e. X ) )
30	29	simpld 460	. . . . . 6 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> x e. X )
31	26	simprd 464	. . . . . 6 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> z e. X )
32		psmettri2 21262	. . . . . 6 |- ( ( 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 1266	. . . . 5 |- ( ( 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 472	. . . . . . . 8 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> ( x D y ) = ( y D x ) )
35	29, 13	syldan 472	. . . . . . . . 9 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> ( x (~Met ` D ) y <-> ( x D y ) = 0 ) )
36	28, 35	mpbid 213	. . . . . . . 8 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> ( x D y ) = 0 )
37	34, 36	eqtr3d 2463	. . . . . . 7 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> ( y D x ) = 0 )
38		metidv 28575	. . . . . . . . 9 |- ( ( D e. (PsMet ` X ) /\ ( y e. X /\ z e. X ) ) -> ( y (~Met ` D ) z <-> ( y D z ) = 0 ) )
39	26, 38	syldan 472	. . . . . . . 8 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> ( y (~Met ` D ) z <-> ( y D z ) = 0 ) )
40	21, 39	mpbid 213	. . . . . . 7 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> ( y D z ) = 0 )
41	37, 40	oveq12d 6314	. . . . . 6 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> ( ( y D x ) +e ( y D z ) ) = ( 0 +e 0 ) )
42		0xr 9676	. . . . . . 7 |- 0 e. RR*
43		xaddid1 11521	. . . . . . 7 |- ( 0 e. RR* -> ( 0 +e 0 ) = 0 )
44	42, 43	ax-mp 5	. . . . . 6 |- ( 0 +e 0 ) = 0
45	41, 44	syl6eq 2477	. . . . 5 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> ( ( y D x ) +e ( y D z ) ) = 0 )
46	33, 45	breqtrd 4441	. . . 4 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> ( x D z ) <_ 0 )
47		psmetge0 21265	. . . . 5 |- ( ( D e. (PsMet ` X ) /\ x e. X /\ z e. X ) -> 0 <_ ( x D z ) )
48	20, 30, 31, 47	syl3anc 1264	. . . 4 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> 0 <_ ( x D z ) )
49		psmetcl 21260	. . . . . 6 |- ( ( D e. (PsMet ` X ) /\ x e. X /\ z e. X ) -> ( x D z ) e. RR* )
50	20, 30, 31, 49	syl3anc 1264	. . . . 5 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> ( x D z ) e. RR* )
51		xrletri3 11440	. . . . 5 |- ( ( ( 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 666	. . . 4 |- ( ( 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 930	. . 3 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> ( x D z ) = 0 )
54		metidv 28575	. . . 4 |- ( ( D e. (PsMet ` X ) /\ ( x e. X /\ z e. X ) ) -> ( x (~Met ` D ) z <-> ( x D z ) = 0 ) )
55	20, 30, 31, 54	syl12anc 1262	. . 3 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> ( x (~Met ` D ) z <-> ( x D z ) = 0 ) )
56	53, 55	mpbird 235	. 2 |- ( ( D e. (PsMet ` X ) /\ ( x (~Met ` D ) y /\ y (~Met ` D ) z ) ) -> x (~Met ` D ) z )
57		psmet0 21261	. . . 4 |- ( ( D e. (PsMet ` X ) /\ x e. X ) -> ( x D x ) = 0 )
58		metidv 28575	. . . . 5 |- ( ( D e. (PsMet ` X ) /\ ( x e. X /\ x e. X ) ) -> ( x (~Met ` D ) x <-> ( x D x ) = 0 ) )
59	58	anabsan2 829	. . . 4 |- ( ( D e. (PsMet ` X ) /\ x e. X ) -> ( x (~Met ` D ) x <-> ( x D x ) = 0 ) )
60	57, 59	mpbird 235	. . 3 |- ( ( D e. (PsMet ` X ) /\ x e. X ) -> x (~Met ` D ) x )
61	1	ssbrd 4458	. . . . . 6 |- ( D e. (PsMet ` X ) -> ( x (~Met ` D ) x -> x ( X X. X ) x ) )
62	61	imp 430	. . . . 5 |- ( ( D e. (PsMet ` X ) /\ x (~Met ` D ) x ) -> x ( X X. X ) x )
63		brxp 4876	. . . . 5 |- ( x ( X X. X ) x <-> ( x e. X /\ x e. X ) )
64	62, 63	sylib 199	. . . 4 |- ( ( D e. (PsMet ` X ) /\ x (~Met ` D ) x ) -> ( x e. X /\ x e. X ) )
65	64	simpld 460	. . 3 |- ( ( D e. (PsMet ` X ) /\ x (~Met ` D ) x ) -> x e. X )
66	60, 65	impbida 840	. 2 |- ( D e. (PsMet ` X ) -> ( x e. X <-> x (~Met ` D ) x ) )
67	5, 19, 56, 66	iserd 7388	1 |- ( D e. (PsMet ` X ) -> (~Met ` D ) Er X )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1867   _Vcvv 3078   C_ wss 3433   class class class wbr 4417   X. cxp 4843   Rel wrel 4850   ` cfv 5592  (class class class)co 6296   Er wer 7359   0cc0 9528   RR*cxr 9663   <_ cle 9665   +ecxad 11396  PsMetcpsmet 18895  ~Metcmetid 28569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-cnex 9584  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604  ax-pre-mulgt0 9605

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4476  df-mpt 4477  df-id 4760  df-po 4766  df-so 4767  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-1st 6798  df-2nd 6799  df-er 7362  df-map 7473  df-en 7569  df-dom 7570  df-sdom 7571  df-pnf 9666  df-mnf 9667  df-xr 9668  df-ltxr 9669  df-le 9670  df-sub 9851  df-neg 9852  df-div 10259  df-2 10657  df-rp 11292  df-xneg 11398  df-xadd 11399  df-xmul 11400  df-psmet 18903  df-metid 28571

This theorem is referenced by:  pstmxmet  28580