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 ) )