Metamath Proof Explorer

Theorem dscmet

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

Ref Expression
Hypothesis dscmet.1 
|- D = ( x e. X , y e. X |-> if ( x = y , 0 , 1 ) )
Assertion dscmet 
|- ( X e. V -> D e. ( Met ` X ) )

Proof

Step Hyp Ref Expression
1 dscmet.1 
 |-  D = ( x e. X , y e. X |-> if ( x = y , 0 , 1 ) )
2 0re 
 |-  0 e. RR
3 1re 
 |-  1 e. RR
4 2 3 ifcli 
 |-  if ( x = y , 0 , 1 ) e. RR
5 4 rgen2w 
 |-  A. x e. X A. y e. X if ( x = y , 0 , 1 ) e. RR
6 1 fmpo 
 |-  ( A. x e. X A. y e. X if ( x = y , 0 , 1 ) e. RR <-> D : ( X X. X ) --> RR )
7 5 6 mpbi 
 |-  D : ( X X. X ) --> RR
8 equequ1 
 |-  ( x = w -> ( x = y <-> w = y ) )
9 8 ifbid 
 |-  ( x = w -> if ( x = y , 0 , 1 ) = if ( w = y , 0 , 1 ) )
10 equequ2 
 |-  ( y = v -> ( w = y <-> w = v ) )
11 10 ifbid 
 |-  ( y = v -> if ( w = y , 0 , 1 ) = if ( w = v , 0 , 1 ) )
12 0nn0 
 |-  0 e. NN0
13 1nn0 
 |-  1 e. NN0
14 12 13 ifcli 
 |-  if ( w = v , 0 , 1 ) e. NN0
15 14 elexi 
 |-  if ( w = v , 0 , 1 ) e. _V
16 9 11 1 15 ovmpo 
 |-  ( ( w e. X /\ v e. X ) -> ( w D v ) = if ( w = v , 0 , 1 ) )
17 16 eqeq1d 
 |-  ( ( w e. X /\ v e. X ) -> ( ( w D v ) = 0 <-> if ( w = v , 0 , 1 ) = 0 ) )
18 iffalse 
 |-  ( -. w = v -> if ( w = v , 0 , 1 ) = 1 )
19 ax-1ne0 
 |-  1 =/= 0
20 19 a1i 
 |-  ( -. w = v -> 1 =/= 0 )
21 18 20 eqnetrd 
 |-  ( -. w = v -> if ( w = v , 0 , 1 ) =/= 0 )
22 21 neneqd 
 |-  ( -. w = v -> -. if ( w = v , 0 , 1 ) = 0 )
23 22 con4i 
 |-  ( if ( w = v , 0 , 1 ) = 0 -> w = v )
24 iftrue 
 |-  ( w = v -> if ( w = v , 0 , 1 ) = 0 )
25 23 24 impbii 
 |-  ( if ( w = v , 0 , 1 ) = 0 <-> w = v )
26 17 25 bitrdi 
 |-  ( ( w e. X /\ v e. X ) -> ( ( w D v ) = 0 <-> w = v ) )
27 12 13 ifcli 
 |-  if ( u = w , 0 , 1 ) e. NN0
28 12 13 ifcli 
 |-  if ( u = v , 0 , 1 ) e. NN0
29 27 28 nn0addcli 
 |-  ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) e. NN0
30 elnn0 
 |-  ( ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) e. NN0 <-> ( ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) e. NN \/ ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) = 0 ) )
31 29 30 mpbi 
 |-  ( ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) e. NN \/ ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) = 0 )
32 breq1 
 |-  ( 0 = if ( w = v , 0 , 1 ) -> ( 0 <_ 1 <-> if ( w = v , 0 , 1 ) <_ 1 ) )
33 breq1 
 |-  ( 1 = if ( w = v , 0 , 1 ) -> ( 1 <_ 1 <-> if ( w = v , 0 , 1 ) <_ 1 ) )
34 0le1 
 |-  0 <_ 1
35 3 leidi 
 |-  1 <_ 1
36 32 33 34 35 keephyp 
 |-  if ( w = v , 0 , 1 ) <_ 1
37 nnge1 
 |-  ( ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) e. NN -> 1 <_ ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) )
38 14 nn0rei 
 |-  if ( w = v , 0 , 1 ) e. RR
39 29 nn0rei 
 |-  ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) e. RR
40 38 3 39 letri 
 |-  ( ( if ( w = v , 0 , 1 ) <_ 1 /\ 1 <_ ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) ) -> if ( w = v , 0 , 1 ) <_ ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) )
41 36 37 40 sylancr 
 |-  ( ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) e. NN -> if ( w = v , 0 , 1 ) <_ ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) )
42 27 nn0ge0i 
 |-  0 <_ if ( u = w , 0 , 1 )
43 28 nn0ge0i 
 |-  0 <_ if ( u = v , 0 , 1 )
44 27 nn0rei 
 |-  if ( u = w , 0 , 1 ) e. RR
45 28 nn0rei 
 |-  if ( u = v , 0 , 1 ) e. RR
46 44 45 add20i 
 |-  ( ( 0 <_ if ( u = w , 0 , 1 ) /\ 0 <_ if ( u = v , 0 , 1 ) ) -> ( ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) = 0 <-> ( if ( u = w , 0 , 1 ) = 0 /\ if ( u = v , 0 , 1 ) = 0 ) ) )
47 42 43 46 mp2an 
 |-  ( ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) = 0 <-> ( if ( u = w , 0 , 1 ) = 0 /\ if ( u = v , 0 , 1 ) = 0 ) )
48 equequ2 
 |-  ( v = w -> ( u = v <-> u = w ) )
49 48 ifbid 
 |-  ( v = w -> if ( u = v , 0 , 1 ) = if ( u = w , 0 , 1 ) )
50 49 eqeq1d 
 |-  ( v = w -> ( if ( u = v , 0 , 1 ) = 0 <-> if ( u = w , 0 , 1 ) = 0 ) )
51 50 48 bibi12d 
 |-  ( v = w -> ( ( if ( u = v , 0 , 1 ) = 0 <-> u = v ) <-> ( if ( u = w , 0 , 1 ) = 0 <-> u = w ) ) )
52 equequ1 
 |-  ( w = u -> ( w = v <-> u = v ) )
53 52 ifbid 
 |-  ( w = u -> if ( w = v , 0 , 1 ) = if ( u = v , 0 , 1 ) )
54 53 eqeq1d 
 |-  ( w = u -> ( if ( w = v , 0 , 1 ) = 0 <-> if ( u = v , 0 , 1 ) = 0 ) )
55 54 52 bibi12d 
 |-  ( w = u -> ( ( if ( w = v , 0 , 1 ) = 0 <-> w = v ) <-> ( if ( u = v , 0 , 1 ) = 0 <-> u = v ) ) )
56 55 25 chvarvv 
 |-  ( if ( u = v , 0 , 1 ) = 0 <-> u = v )
57 51 56 chvarvv 
 |-  ( if ( u = w , 0 , 1 ) = 0 <-> u = w )
58 eqtr2 
 |-  ( ( u = w /\ u = v ) -> w = v )
59 57 56 58 syl2anb 
 |-  ( ( if ( u = w , 0 , 1 ) = 0 /\ if ( u = v , 0 , 1 ) = 0 ) -> w = v )
60 59 iftrued 
 |-  ( ( if ( u = w , 0 , 1 ) = 0 /\ if ( u = v , 0 , 1 ) = 0 ) -> if ( w = v , 0 , 1 ) = 0 )
61 2 leidi 
 |-  0 <_ 0
62 60 61 eqbrtrdi 
 |-  ( ( if ( u = w , 0 , 1 ) = 0 /\ if ( u = v , 0 , 1 ) = 0 ) -> if ( w = v , 0 , 1 ) <_ 0 )
63 47 62 sylbi 
 |-  ( ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) = 0 -> if ( w = v , 0 , 1 ) <_ 0 )
64 id 
 |-  ( ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) = 0 -> ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) = 0 )
65 63 64 breqtrrd 
 |-  ( ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) = 0 -> if ( w = v , 0 , 1 ) <_ ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) )
66 41 65 jaoi 
 |-  ( ( ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) e. NN \/ ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) = 0 ) -> if ( w = v , 0 , 1 ) <_ ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) )
67 31 66 mp1i 
 |-  ( ( u e. X /\ ( w e. X /\ v e. X ) ) -> if ( w = v , 0 , 1 ) <_ ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) )
68 16 adantl 
 |-  ( ( u e. X /\ ( w e. X /\ v e. X ) ) -> ( w D v ) = if ( w = v , 0 , 1 ) )
69 eqeq12 
 |-  ( ( x = u /\ y = w ) -> ( x = y <-> u = w ) )
70 69 ifbid 
 |-  ( ( x = u /\ y = w ) -> if ( x = y , 0 , 1 ) = if ( u = w , 0 , 1 ) )
71 27 elexi 
 |-  if ( u = w , 0 , 1 ) e. _V
72 70 1 71 ovmpoa 
 |-  ( ( u e. X /\ w e. X ) -> ( u D w ) = if ( u = w , 0 , 1 ) )
73 72 adantrr 
 |-  ( ( u e. X /\ ( w e. X /\ v e. X ) ) -> ( u D w ) = if ( u = w , 0 , 1 ) )
74 eqeq12 
 |-  ( ( x = u /\ y = v ) -> ( x = y <-> u = v ) )
75 74 ifbid 
 |-  ( ( x = u /\ y = v ) -> if ( x = y , 0 , 1 ) = if ( u = v , 0 , 1 ) )
76 28 elexi 
 |-  if ( u = v , 0 , 1 ) e. _V
77 75 1 76 ovmpoa 
 |-  ( ( u e. X /\ v e. X ) -> ( u D v ) = if ( u = v , 0 , 1 ) )
78 77 adantrl 
 |-  ( ( u e. X /\ ( w e. X /\ v e. X ) ) -> ( u D v ) = if ( u = v , 0 , 1 ) )
79 73 78 oveq12d 
 |-  ( ( u e. X /\ ( w e. X /\ v e. X ) ) -> ( ( u D w ) + ( u D v ) ) = ( if ( u = w , 0 , 1 ) + if ( u = v , 0 , 1 ) ) )
80 67 68 79 3brtr4d 
 |-  ( ( u e. X /\ ( w e. X /\ v e. X ) ) -> ( w D v ) <_ ( ( u D w ) + ( u D v ) ) )
81 80 expcom 
 |-  ( ( w e. X /\ v e. X ) -> ( u e. X -> ( w D v ) <_ ( ( u D w ) + ( u D v ) ) ) )
82 81 ralrimiv 
 |-  ( ( w e. X /\ v e. X ) -> A. u e. X ( w D v ) <_ ( ( u D w ) + ( u D v ) ) )
83 26 82 jca 
 |-  ( ( w e. X /\ v e. X ) -> ( ( ( w D v ) = 0 <-> w = v ) /\ A. u e. X ( w D v ) <_ ( ( u D w ) + ( u D v ) ) ) )
84 83 rgen2 
 |-  A. w e. X A. v e. X ( ( ( w D v ) = 0 <-> w = v ) /\ A. u e. X ( w D v ) <_ ( ( u D w ) + ( u D v ) ) )
85 7 84 pm3.2i 
 |-  ( D : ( X X. X ) --> RR /\ A. w e. X A. v e. X ( ( ( w D v ) = 0 <-> w = v ) /\ A. u e. X ( w D v ) <_ ( ( u D w ) + ( u D v ) ) ) )
86 ismet 
 |-  ( X e. V -> ( D e. ( Met ` X ) <-> ( D : ( X X. X ) --> RR /\ A. w e. X A. v e. X ( ( ( w D v ) = 0 <-> w = v ) /\ A. u e. X ( w D v ) <_ ( ( u D w ) + ( u D v ) ) ) ) ) )
87 85 86 mpbiri 
 |-  ( X e. V -> D e. ( Met ` X ) )