Metamath Proof Explorer

Theorem rrnmet

Description: Euclidean space is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 5-Jun-2014)

Ref Expression
Hypothesis rrnval.1 
|- X = ( RR ^m I )
Assertion rrnmet 
|- ( I e. Fin -> ( Rn ` I ) e. ( Met ` X ) )

Proof

Step Hyp Ref Expression
1 rrnval.1 
 |-  X = ( RR ^m I )
2 simpl 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> I e. Fin )
3 simprl 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> x e. X )
4 3 1 eleqtrdi 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> x e. ( RR ^m I ) )
5 elmapi 
 |-  ( x e. ( RR ^m I ) -> x : I --> RR )
6 4 5 syl 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> x : I --> RR )
7 6 ffvelrnda 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( x ` k ) e. RR )
8 simprr 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> y e. X )
9 8 1 eleqtrdi 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> y e. ( RR ^m I ) )
10 elmapi 
 |-  ( y e. ( RR ^m I ) -> y : I --> RR )
11 9 10 syl 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> y : I --> RR )
12 11 ffvelrnda 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( y ` k ) e. RR )
13 7 12 resubcld 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( ( x ` k ) - ( y ` k ) ) e. RR )
14 13 resqcld 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) e. RR )
15 2 14 fsumrecl 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) e. RR )
16 13 sqge0d 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> 0 <_ ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) )
17 2 14 16 fsumge0 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> 0 <_ sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) )
18 15 17 resqrtcld 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) e. RR )
19 18 ralrimivva 
 |-  ( I e. Fin -> A. x e. X A. y e. X ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) e. RR )
20 eqid 
 |-  ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) = ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
21 20 fmpo 
 |-  ( A. x e. X A. y e. X ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) e. RR <-> ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) : ( X X. X ) --> RR )
22 19 21 sylib 
 |-  ( I e. Fin -> ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) : ( X X. X ) --> RR )
23 1 rrnval 
 |-  ( I e. Fin -> ( Rn ` I ) = ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
24 23 feq1d 
 |-  ( I e. Fin -> ( ( Rn ` I ) : ( X X. X ) --> RR <-> ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) : ( X X. X ) --> RR ) )
25 22 24 mpbird 
 |-  ( I e. Fin -> ( Rn ` I ) : ( X X. X ) --> RR )
26 sqrt00 
 |-  ( ( sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) e. RR /\ 0 <_ sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) -> ( ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = 0 <-> sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 ) )
27 15 17 26 syl2anc 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = 0 <-> sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 ) )
28 2 14 16 fsum00 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 <-> A. k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 ) )
29 27 28 bitrd 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = 0 <-> A. k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 ) )
30 13 recnd 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( ( x ` k ) - ( y ` k ) ) e. CC )
31 sqeq0 
 |-  ( ( ( x ` k ) - ( y ` k ) ) e. CC -> ( ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 <-> ( ( x ` k ) - ( y ` k ) ) = 0 ) )
32 30 31 syl 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 <-> ( ( x ` k ) - ( y ` k ) ) = 0 ) )
33 7 recnd 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( x ` k ) e. CC )
34 12 recnd 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( y ` k ) e. CC )
35 33 34 subeq0ad 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( ( ( x ` k ) - ( y ` k ) ) = 0 <-> ( x ` k ) = ( y ` k ) ) )
36 32 35 bitrd 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 <-> ( x ` k ) = ( y ` k ) ) )
37 36 ralbidva 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( A. k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 <-> A. k e. I ( x ` k ) = ( y ` k ) ) )
38 29 37 bitrd 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = 0 <-> A. k e. I ( x ` k ) = ( y ` k ) ) )
39 1 rrnmval 
 |-  ( ( I e. Fin /\ x e. X /\ y e. X ) -> ( x ( Rn ` I ) y ) = ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
40 39 3expb 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( x ( Rn ` I ) y ) = ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
41 40 eqeq1d 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( ( x ( Rn ` I ) y ) = 0 <-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = 0 ) )
42 6 ffnd 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> x Fn I )
43 11 ffnd 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> y Fn I )
44 eqfnfv 
 |-  ( ( x Fn I /\ y Fn I ) -> ( x = y <-> A. k e. I ( x ` k ) = ( y ` k ) ) )
45 42 43 44 syl2anc 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( x = y <-> A. k e. I ( x ` k ) = ( y ` k ) ) )
46 38 41 45 3bitr4d 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( ( x ( Rn ` I ) y ) = 0 <-> x = y ) )
47 simpll 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> I e. Fin )
48 7 adantlr 
 |-  ( ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( x ` k ) e. RR )
49 simpr 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> z e. X )
50 49 1 eleqtrdi 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> z e. ( RR ^m I ) )
51 elmapi 
 |-  ( z e. ( RR ^m I ) -> z : I --> RR )
52 50 51 syl 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> z : I --> RR )
53 52 ffvelrnda 
 |-  ( ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( z ` k ) e. RR )
54 48 53 resubcld 
 |-  ( ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( ( x ` k ) - ( z ` k ) ) e. RR )
55 12 adantlr 
 |-  ( ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( y ` k ) e. RR )
56 53 55 resubcld 
 |-  ( ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( ( z ` k ) - ( y ` k ) ) e. RR )
57 47 54 56 trirn 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( sqrt ` sum_ k e. I ( ( ( ( x ` k ) - ( z ` k ) ) + ( ( z ` k ) - ( y ` k ) ) ) ^ 2 ) ) <_ ( ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( z ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
58 33 adantlr 
 |-  ( ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( x ` k ) e. CC )
59 53 recnd 
 |-  ( ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( z ` k ) e. CC )
60 34 adantlr 
 |-  ( ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( y ` k ) e. CC )
61 58 59 60 npncand 
 |-  ( ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( ( ( x ` k ) - ( z ` k ) ) + ( ( z ` k ) - ( y ` k ) ) ) = ( ( x ` k ) - ( y ` k ) ) )
62 61 oveq1d 
 |-  ( ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( ( ( ( x ` k ) - ( z ` k ) ) + ( ( z ` k ) - ( y ` k ) ) ) ^ 2 ) = ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) )
63 62 sumeq2dv 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> sum_ k e. I ( ( ( ( x ` k ) - ( z ` k ) ) + ( ( z ` k ) - ( y ` k ) ) ) ^ 2 ) = sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) )
64 63 fveq2d 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( sqrt ` sum_ k e. I ( ( ( ( x ` k ) - ( z ` k ) ) + ( ( z ` k ) - ( y ` k ) ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
65 sqsubswap 
 |-  ( ( ( x ` k ) e. CC /\ ( z ` k ) e. CC ) -> ( ( ( x ` k ) - ( z ` k ) ) ^ 2 ) = ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) )
66 58 59 65 syl2anc 
 |-  ( ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( ( ( x ` k ) - ( z ` k ) ) ^ 2 ) = ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) )
67 66 sumeq2dv 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> sum_ k e. I ( ( ( x ` k ) - ( z ` k ) ) ^ 2 ) = sum_ k e. I ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) )
68 67 fveq2d 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( z ` k ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) )
69 68 oveq1d 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( z ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) = ( ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
70 57 64 69 3brtr3d 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) <_ ( ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
71 40 adantr 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( x ( Rn ` I ) y ) = ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
72 1 rrnmval 
 |-  ( ( I e. Fin /\ z e. X /\ x e. X ) -> ( z ( Rn ` I ) x ) = ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) )
73 72 3adant3r 
 |-  ( ( I e. Fin /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( z ( Rn ` I ) x ) = ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) )
74 1 rrnmval 
 |-  ( ( I e. Fin /\ z e. X /\ y e. X ) -> ( z ( Rn ` I ) y ) = ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) )
75 74 3adant3l 
 |-  ( ( I e. Fin /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( z ( Rn ` I ) y ) = ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) )
76 73 75 oveq12d 
 |-  ( ( I e. Fin /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( ( z ( Rn ` I ) x ) + ( z ( Rn ` I ) y ) ) = ( ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
77 76 3expa 
 |-  ( ( ( I e. Fin /\ z e. X ) /\ ( x e. X /\ y e. X ) ) -> ( ( z ( Rn ` I ) x ) + ( z ( Rn ` I ) y ) ) = ( ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
78 77 an32s 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( ( z ( Rn ` I ) x ) + ( z ( Rn ` I ) y ) ) = ( ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. I ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
79 70 71 78 3brtr4d 
 |-  ( ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( x ( Rn ` I ) y ) <_ ( ( z ( Rn ` I ) x ) + ( z ( Rn ` I ) y ) ) )
80 79 ralrimiva 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> A. z e. X ( x ( Rn ` I ) y ) <_ ( ( z ( Rn ` I ) x ) + ( z ( Rn ` I ) y ) ) )
81 46 80 jca 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( ( ( x ( Rn ` I ) y ) = 0 <-> x = y ) /\ A. z e. X ( x ( Rn ` I ) y ) <_ ( ( z ( Rn ` I ) x ) + ( z ( Rn ` I ) y ) ) ) )
82 81 ralrimivva 
 |-  ( I e. Fin -> A. x e. X A. y e. X ( ( ( x ( Rn ` I ) y ) = 0 <-> x = y ) /\ A. z e. X ( x ( Rn ` I ) y ) <_ ( ( z ( Rn ` I ) x ) + ( z ( Rn ` I ) y ) ) ) )
83 ovex 
 |-  ( RR ^m I ) e. _V
84 1 83 eqeltri 
 |-  X e. _V
85 ismet 
 |-  ( X e. _V -> ( ( Rn ` I ) e. ( Met ` X ) <-> ( ( Rn ` I ) : ( X X. X ) --> RR /\ A. x e. X A. y e. X ( ( ( x ( Rn ` I ) y ) = 0 <-> x = y ) /\ A. z e. X ( x ( Rn ` I ) y ) <_ ( ( z ( Rn ` I ) x ) + ( z ( Rn ` I ) y ) ) ) ) ) )
86 84 85 ax-mp 
 |-  ( ( Rn ` I ) e. ( Met ` X ) <-> ( ( Rn ` I ) : ( X X. X ) --> RR /\ A. x e. X A. y e. X ( ( ( x ( Rn ` I ) y ) = 0 <-> x = y ) /\ A. z e. X ( x ( Rn ` I ) y ) <_ ( ( z ( Rn ` I ) x ) + ( z ( Rn ` I ) y ) ) ) ) )
87 25 82 86 sylanbrc 
 |-  ( I e. Fin -> ( Rn ` I ) e. ( Met ` X ) )