Theorem dscmet 7918

Description: The discrete metric on any set X. Definition 1.1-8 of [Kreyszig] p. 8. (Contributed by FL, 12-Oct-2006.)

Hypotheses

Ref	Expression
dscmet.1	|- X e. V
dscmet.2	|- D = {<.<.x, y>., z>. | ((x e. X /\ y e. X) /\ z = if(x = y, 0, 1))}

Assertion

Ref	Expression
dscmet	|- D e. Met

Distinct variable group:   x,X,y,z

Proof of Theorem dscmet

Step	Hyp	Ref	Expression
1		dscmet.1	. 2 |- X e. V
2		dscmet.2	. . 3 |- D = {<.<.x, y>., z>. | ((x e. X /\ y e. X) /\ z = if(x = y, 0, 1))}
3		0re 5440	. . . . 5 |- 0 e. RR
4		1re 5435	. . . . 5 |- 1 e. RR
5	3, 4	keepel 2399	. . . 4 |- if(x = y, 0, 1) e. RR
6	5	a1i 8	. . 3 |- ((x e. X /\ y e. X) -> if(x = y, 0, 1) e. RR)
7	2, 6	foprab 4120	. 2 |- D:(X X. X)-->RR
8	3, 4	keepel 2399	. . . . . 6 |- if(w = v, 0, 1) e. RR
9	8	elisseti 1818	. . . . 5 |- if(w = v, 0, 1) e. V
10		eqeq1 1481	. . . . . 6 |- (x = w -> (x = y <-> w = y))
11	10	ifbid 2372	. . . . 5 |- (x = w -> if(x = y, 0, 1) = if(w = y, 0, 1))
12		eqeq2 1484	. . . . . 6 |- (y = v -> (w = y <-> w = v))
13	12	ifbid 2372	. . . . 5 |- (y = v -> if(w = y, 0, 1) = if(w = v, 0, 1))
14	9, 11, 13, 2	oprabval2 4028	. . . 4 |- ((w e. X /\ v e. X) -> (wDv) = if(w = v, 0, 1))
15	14	eqeq1d 1483	. . 3 |- ((w e. X /\ v e. X) -> ((wDv) = 0 <-> if(w = v, 0, 1) = 0))
16		eqif 2377	. . . . . 6 |- (0 = if(w = v, 0, 1) <-> ((w = v /\ 0 = 0) \/ (-. w = v /\ 0 = 1)))
17		pm3.26 319	. . . . . . 7 |- ((w = v /\ 0 = 0) -> w = v)
18		ax1ne0 5280	. . . . . . . . . . . 12 |- 1 =/= 0
19		necom 1636	. . . . . . . . . . . 12 |- (1 =/= 0 <-> 0 =/= 1)
20	18, 19	mpbi 189	. . . . . . . . . . 11 |- 0 =/= 1
21		df-ne 1587	. . . . . . . . . . 11 |- (0 =/= 1 <-> -. 0 = 1)
22	20, 21	mpbi 189	. . . . . . . . . 10 |- -. 0 = 1
23	22	pm2.21i 77	. . . . . . . . 9 |- (0 = 1 -> (w = v \/ w = v))
24	23	orcanai 690	. . . . . . . 8 |- ((0 = 1 /\ -. w = v) -> w = v)
25	24	ancoms 436	. . . . . . 7 |- ((-. w = v /\ 0 = 1) -> w = v)
26	17, 25	jaoi 341	. . . . . 6 |- (((w = v /\ 0 = 0) \/ (-. w = v /\ 0 = 1)) -> w = v)
27	16, 26	sylbi 199	. . . . 5 |- (0 = if(w = v, 0, 1) -> w = v)
28	27	eqcoms 1478	. . . 4 |- (if(w = v, 0, 1) = 0 -> w = v)
29		iftrue 2366	. . . 4 |- (w = v -> if(w = v, 0, 1) = 0)
30	28, 29	impbi 157	. . 3 |- (if(w = v, 0, 1) = 0 <-> w = v)
31	15, 30	syl6bb 536	. 2 |- ((w e. X /\ v e. X) -> ((wDv) = 0 <-> w = v))
32		equtr 1131	. . . . . . . . 9 |- (u = w -> (w = v -> u = v))
33	32	imdistani 443	. . . . . . . 8 |- ((u = w /\ w = v) -> (u = w /\ u = v))
34		iftrue 2366	. . . . . . . . . 10 |- (u = w -> if(u = w, 0, 1) = 0)
35		iftrue 2366	. . . . . . . . . 10 |- (u = v -> if(u = v, 0, 1) = 0)
36	34, 35	opreqan12d 3979	. . . . . . . . 9 |- ((u = w /\ u = v) -> (if(u = w, 0, 1) + if(u = v, 0, 1)) = (0 + 0))
37		0nn0 6113	. . . . . . . . . 10 |- 0 e. NN0
38	3, 37	nn0addge1 6132	. . . . . . . . 9 |- 0 <_ (0 + 0)
39	36, 38	syl5breqr 2651	. . . . . . . 8 |- ((u = w /\ u = v) -> 0 <_ (if(u = w, 0, 1) + if(u = v, 0, 1)))
40	33, 39	syl 10	. . . . . . 7 |- ((u = w /\ w = v) -> 0 <_ (if(u = w, 0, 1) + if(u = v, 0, 1)))
41		equequ2 1135	. . . . . . . . . . 11 |- (w = v -> (u = w <-> u = v))
42	41	negbid 611	. . . . . . . . . 10 |- (w = v -> (-. u = w <-> -. u = v))
43	42	biimpcd 155	. . . . . . . . 9 |- (-. u = w -> (w = v -> -. u = v))
44	43	imdistani 443	. . . . . . . 8 |- ((-. u = w /\ w = v) -> (-. u = w /\ -. u = v))
45		iffalse 2367	. . . . . . . . . 10 |- (-. u = w -> if(u = w, 0, 1) = 1)
46		iffalse 2367	. . . . . . . . . 10 |- (-. u = v -> if(u = v, 0, 1) = 1)
47	45, 46	opreqan12d 3979	. . . . . . . . 9 |- ((-. u = w /\ -. u = v) -> (if(u = w, 0, 1) + if(u = v, 0, 1)) = (1 + 1))
48		lt01 5680	. . . . . . . . . . 11 |- 0 < 1
49	3, 4, 48	ltlei 5581	. . . . . . . . . 10 |- 0 <_ 1
50	4, 4	addge0 5599	. . . . . . . . . 10 |- ((0 <_ 1 /\ 0 <_ 1) -> 0 <_ (1 + 1))
51	49, 49, 50	mp2an 697	. . . . . . . . 9 |- 0 <_ (1 + 1)
52	47, 51	syl5breqr 2651	. . . . . . . 8 |- ((-. u = w /\ -. u = v) -> 0 <_ (if(u = w, 0, 1) + if(u = v, 0, 1)))
53	44, 52	syl 10	. . . . . . 7 |- ((-. u = w /\ w = v) -> 0 <_ (if(u = w, 0, 1) + if(u = v, 0, 1)))
54	40, 53	pm2.61ian 476	. . . . . 6 |- (w = v -> 0 <_ (if(u = w, 0, 1) + if(u = v, 0, 1)))
55	29, 54	eqbrtrd 2635	. . . . 5 |- (w = v -> if(w = v, 0, 1) <_ (if(u = w, 0, 1) + if(u = v, 0, 1)))
56		iffalse 2367	. . . . . 6 |- (-. w = v -> if(w = v, 0, 1) = 1)
57		neeq1 1590	. . . . . . . . . . . 12 |- (u = w -> (u =/= v <-> w =/= v))
58	57	biimprd 154	. . . . . . . . . . 11 |- (u = w -> (w =/= v -> u =/= v))
59		df-ne 1587	. . . . . . . . . . 11 |- (w =/= v <-> -. w = v)
60		df-ne 1587	. . . . . . . . . . 11 |- (u =/= v <-> -. u = v)
61	58, 59, 60	3imtr3g 552	. . . . . . . . . 10 |- (u = w -> (-. w = v -> -. u = v))
62	61	imdistani 443	. . . . . . . . 9 |- ((u = w /\ -. w = v) -> (u = w /\ -. u = v))
63	34, 46	opreqan12d 3979	. . . . . . . . . . 11 |- ((u = w /\ -. u = v) -> (if(u = w, 0, 1) + if(u = v, 0, 1)) = (0 + 1))
64		ax1cn 5269	. . . . . . . . . . . 12 |- 1 e. CC
65	64	addid2 5331	. . . . . . . . . . 11 |- (0 + 1) = 1
66	63, 65	syl6eq 1523	. . . . . . . . . 10 |- ((u = w /\ -. u = v) -> (if(u = w, 0, 1) + if(u = v, 0, 1)) = 1)
67	4	leid 5610	. . . . . . . . . 10 |- 1 <_ 1
68	66, 67	syl5breqr 2651	. . . . . . . . 9 |- ((u = w /\ -. u = v) -> 1 <_ (if(u = w, 0, 1) + if(u = v, 0, 1)))
69	62, 68	syl 10	. . . . . . . 8 |- ((u = w /\ -. w = v) -> 1 <_ (if(u = w, 0, 1) + if(u = v, 0, 1)))
70	69	ex 373	. . . . . . 7 |- (u = w -> (-. w = v -> 1 <_ (if(u = w, 0, 1) + if(u = v, 0, 1))))
71	45, 35	opreqan12d 3979	. . . . . . . . . . 11 |- ((-. u = w /\ u = v) -> (if(u = w, 0, 1) + if(u = v, 0, 1)) = (1 + 0))
72	64	addid1 5330	. . . . . . . . . . 11 |- (1 + 0) = 1
73	71, 72	syl6eq 1523	. . . . . . . . . 10 |- ((-. u = w /\ u = v) -> (if(u = w, 0, 1) + if(u = v, 0, 1)) = 1)
74	73, 67	syl5breqr 2651	. . . . . . . . 9 |- ((-. u = w /\ u = v) -> 1 <_ (if(u = w, 0, 1) + if(u = v, 0, 1)))
75		df-2 5970	. . . . . . . . . . 11 |- 2 = (1 + 1)
76	47, 75	syl6eqr 1525	. . . . . . . . . 10 |- ((-. u = w /\ -. u = v) -> (if(u = w, 0, 1) + if(u = v, 0, 1)) = 2)
77		2re 5979	. . . . . . . . . . 11 |- 2 e. RR
78		1lt2 6028	. . . . . . . . . . 11 |- 1 < 2
79	4, 77, 78	ltlei 5581	. . . . . . . . . 10 |- 1 <_ 2
80	76, 79	syl5breqr 2651	. . . . . . . . 9 |- ((-. u = w /\ -. u = v) -> 1 <_ (if(u = w, 0, 1) + if(u = v, 0, 1)))
81	74, 80	pm2.61dan 477	. . . . . . . 8 |- (-. u = w -> 1 <_ (if(u = w, 0, 1) + if(u = v, 0, 1)))
82	81	a1d 12	. . . . . . 7 |- (-. u = w -> (-. w = v -> 1 <_ (if(u = w, 0, 1) + if(u = v, 0, 1))))
83	70, 82	pm2.61i 126	. . . . . 6 |- (-. w = v -> 1 <_ (if(u = w, 0, 1) + if(u = v, 0, 1)))
84	56, 83	eqbrtrd 2635	. . . . 5 |- (-. w = v -> if(w = v, 0, 1) <_ (if(u = w, 0, 1) + if(u = v, 0, 1)))
85	55, 84	pm2.61i 126	. . . 4 |- if(w = v, 0, 1) <_ (if(u = w, 0, 1) + if(u = v, 0, 1))
86	85	a1i 8	. . 3 |- ((w e. X /\ v e. X /\ u e. X) -> if(w