Metamath Proof Explorer

Theorem rrxmet

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

Ref Expression
Hypotheses rrxmval.1 
|- X = { h e. ( RR ^m I ) | h finSupp 0 }
rrxmval.d 
|- D = ( dist ` ( RR^ ` I ) )
Assertion rrxmet 
|- ( I e. V -> D e. ( Met ` X ) )

Proof

Step Hyp Ref Expression
1 rrxmval.1 
 |-  X = { h e. ( RR ^m I ) | h finSupp 0 }
2 rrxmval.d 
 |-  D = ( dist ` ( RR^ ` I ) )
3 simprl 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> x e. X )
4 1 3 rrxfsupp 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( x supp 0 ) e. Fin )
5 simprr 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> y e. X )
6 1 5 rrxfsupp 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( y supp 0 ) e. Fin )
7 unfi 
 |-  ( ( ( x supp 0 ) e. Fin /\ ( y supp 0 ) e. Fin ) -> ( ( x supp 0 ) u. ( y supp 0 ) ) e. Fin )
8 4 6 7 syl2anc 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( ( x supp 0 ) u. ( y supp 0 ) ) e. Fin )
9 1 3 rrxsuppss 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( x supp 0 ) C_ I )
10 1 5 rrxsuppss 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( y supp 0 ) C_ I )
11 9 10 unssd 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( ( x supp 0 ) u. ( y supp 0 ) ) C_ I )
12 11 sselda 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ) -> k e. I )
13 1 3 rrxf 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> x : I --> RR )
14 13 ffvelcdmda 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( x ` k ) e. RR )
15 1 5 rrxf 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> y : I --> RR )
16 15 ffvelcdmda 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( y ` k ) e. RR )
17 14 16 resubcld 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( ( x ` k ) - ( y ` k ) ) e. RR )
18 17 resqcld 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) e. RR )
19 12 18 syldan 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ) -> ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) e. RR )
20 8 19 fsumrecl 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) e. RR )
21 17 sqge0d 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> 0 <_ ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) )
22 12 21 syldan 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ) -> 0 <_ ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) )
23 8 19 22 fsumge0 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> 0 <_ sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) )
24 20 23 resqrtcld 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) e. RR )
25 24 ralrimivva 
 |-  ( I e. V -> A. x e. X A. y e. X ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) e. RR )
26 eqid 
 |-  ( x e. X , y e. X |-> ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) = ( x e. X , y e. X |-> ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
27 26 fmpo 
 |-  ( A. x e. X A. y e. X ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) e. RR <-> ( x e. X , y e. X |-> ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) : ( X X. X ) --> RR )
28 25 27 sylib 
 |-  ( I e. V -> ( x e. X , y e. X |-> ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) : ( X X. X ) --> RR )
29 1 2 rrxmfval 
 |-  ( I e. V -> D = ( x e. X , y e. X |-> ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
30 29 feq1d 
 |-  ( I e. V -> ( D : ( X X. X ) --> RR <-> ( x e. X , y e. X |-> ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) : ( X X. X ) --> RR ) )
31 28 30 mpbird 
 |-  ( I e. V -> D : ( X X. X ) --> RR )
32 sqrt00 
 |-  ( ( sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) e. RR /\ 0 <_ sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) -> ( ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = 0 <-> sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 ) )
33 20 23 32 syl2anc 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = 0 <-> sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 ) )
34 8 19 22 fsum00 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 <-> A. k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 ) )
35 17 recnd 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( ( x ` k ) - ( y ` k ) ) e. CC )
36 sqeq0 
 |-  ( ( ( x ` k ) - ( y ` k ) ) e. CC -> ( ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 <-> ( ( x ` k ) - ( y ` k ) ) = 0 ) )
37 35 36 syl 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 <-> ( ( x ` k ) - ( y ` k ) ) = 0 ) )
38 14 recnd 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( x ` k ) e. CC )
39 16 recnd 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( y ` k ) e. CC )
40 38 39 subeq0ad 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( ( ( x ` k ) - ( y ` k ) ) = 0 <-> ( x ` k ) = ( y ` k ) ) )
41 37 40 bitrd 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. I ) -> ( ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 <-> ( x ` k ) = ( y ` k ) ) )
42 12 41 syldan 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ) -> ( ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 <-> ( x ` k ) = ( y ` k ) ) )
43 42 ralbidva 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( A. k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = 0 <-> A. k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( x ` k ) = ( y ` k ) ) )
44 33 34 43 3bitrd 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = 0 <-> A. k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( x ` k ) = ( y ` k ) ) )
45 1 2 rrxmval 
 |-  ( ( I e. V /\ x e. X /\ y e. X ) -> ( x D y ) = ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
46 45 3expb 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( x D y ) = ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
47 46 eqeq1d 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) = 0 <-> ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = 0 ) )
48 13 ffnd 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> x Fn I )
49 15 ffnd 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> y Fn I )
50 eqfnfv 
 |-  ( ( x Fn I /\ y Fn I ) -> ( x = y <-> A. k e. I ( x ` k ) = ( y ` k ) ) )
51 48 49 50 syl2anc 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( x = y <-> A. k e. I ( x ` k ) = ( y ` k ) ) )
52 ssun1 
 |-  ( x supp 0 ) C_ ( ( x supp 0 ) u. ( y supp 0 ) )
53 52 a1i 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( x supp 0 ) C_ ( ( x supp 0 ) u. ( y supp 0 ) ) )
54 simpl 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> I e. V )
55 0red 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> 0 e. RR )
56 13 53 54 55 suppssr 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. ( I \ ( ( x supp 0 ) u. ( y supp 0 ) ) ) ) -> ( x ` k ) = 0 )
57 ssun2 
 |-  ( y supp 0 ) C_ ( ( x supp 0 ) u. ( y supp 0 ) )
58 57 a1i 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( y supp 0 ) C_ ( ( x supp 0 ) u. ( y supp 0 ) ) )
59 15 58 54 55 suppssr 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. ( I \ ( ( x supp 0 ) u. ( y supp 0 ) ) ) ) -> ( y ` k ) = 0 )
60 56 59 eqtr4d 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ k e. ( I \ ( ( x supp 0 ) u. ( y supp 0 ) ) ) ) -> ( x ` k ) = ( y ` k ) )
61 60 ralrimiva 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> A. k e. ( I \ ( ( x supp 0 ) u. ( y supp 0 ) ) ) ( x ` k ) = ( y ` k ) )
62 11 61 raldifeq 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( A. k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( x ` k ) = ( y ` k ) <-> A. k e. I ( x ` k ) = ( y ` k ) ) )
63 51 62 bitr4d 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( x = y <-> A. k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( x ` k ) = ( y ` k ) ) )
64 44 47 63 3bitr4d 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) = 0 <-> x = y ) )
65 8 3adant2 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( ( x supp 0 ) u. ( y supp 0 ) ) e. Fin )
66 simp2 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> z e. X )
67 1 66 rrxfsupp 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( z supp 0 ) e. Fin )
68 unfi 
 |-  ( ( ( ( x supp 0 ) u. ( y supp 0 ) ) e. Fin /\ ( z supp 0 ) e. Fin ) -> ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) e. Fin )
69 65 67 68 syl2anc 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) e. Fin )
70 69 3expa 
 |-  ( ( ( I e. V /\ z e. X ) /\ ( x e. X /\ y e. X ) ) -> ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) e. Fin )
71 70 an32s 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) e. Fin )
72 11 adantr 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( ( x supp 0 ) u. ( y supp 0 ) ) C_ I )
73 simpr 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> z e. X )
74 1 73 rrxsuppss 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( z supp 0 ) C_ I )
75 72 74 unssd 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) C_ I )
76 75 sselda 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ) -> k e. I )
77 14 adantlr 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( x ` k ) e. RR )
78 1 73 rrxf 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> z : I --> RR )
79 78 ffvelcdmda 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( z ` k ) e. RR )
80 77 79 resubcld 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( ( x ` k ) - ( z ` k ) ) e. RR )
81 76 80 syldan 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ) -> ( ( x ` k ) - ( z ` k ) ) e. RR )
82 16 adantlr 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( y ` k ) e. RR )
83 79 82 resubcld 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( ( z ` k ) - ( y ` k ) ) e. RR )
84 76 83 syldan 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ) -> ( ( z ` k ) - ( y ` k ) ) e. RR )
85 71 81 84 trirn 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( ( x ` k ) - ( z ` k ) ) + ( ( z ` k ) - ( y ` k ) ) ) ^ 2 ) ) <_ ( ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( x ` k ) - ( z ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
86 38 adantlr 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( x ` k ) e. CC )
87 79 recnd 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( z ` k ) e. CC )
88 39 adantlr 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( y ` k ) e. CC )
89 86 87 88 npncand 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( ( ( x ` k ) - ( z ` k ) ) + ( ( z ` k ) - ( y ` k ) ) ) = ( ( x ` k ) - ( y ` k ) ) )
90 89 oveq1d 
 |-  ( ( ( ( I e. V /\ ( 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 ) )
91 76 90 syldan 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ) -> ( ( ( ( x ` k ) - ( z ` k ) ) + ( ( z ` k ) - ( y ` k ) ) ) ^ 2 ) = ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) )
92 91 sumeq2dv 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( ( x ` k ) - ( z ` k ) ) + ( ( z ` k ) - ( y ` k ) ) ) ^ 2 ) = sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) )
93 92 fveq2d 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( ( x ` k ) - ( z ` k ) ) + ( ( z ` k ) - ( y ` k ) ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
94 sqsubswap 
 |-  ( ( ( x ` k ) e. CC /\ ( z ` k ) e. CC ) -> ( ( ( x ` k ) - ( z ` k ) ) ^ 2 ) = ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) )
95 86 87 94 syl2anc 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. I ) -> ( ( ( x ` k ) - ( z ` k ) ) ^ 2 ) = ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) )
96 76 95 syldan 
 |-  ( ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) /\ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ) -> ( ( ( x ` k ) - ( z ` k ) ) ^ 2 ) = ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) )
97 96 sumeq2dv 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( x ` k ) - ( z ` k ) ) ^ 2 ) = sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) )
98 97 fveq2d 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( x ` k ) - ( z ` k ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) )
99 98 oveq1d 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( x ` k ) - ( z ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) = ( ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
100 85 93 99 3brtr3d 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) <_ ( ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
101 46 adantr 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( x D y ) = ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
102 simp1 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> I e. V )
103 3 3adant2 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> x e. X )
104 5 3adant2 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> y e. X )
105 1 103 rrxsuppss 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( x supp 0 ) C_ I )
106 1 104 rrxsuppss 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( y supp 0 ) C_ I )
107 105 106 unssd 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( ( x supp 0 ) u. ( y supp 0 ) ) C_ I )
108 1 66 rrxsuppss 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( z supp 0 ) C_ I )
109 107 108 unssd 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) C_ I )
110 ssun1 
 |-  ( ( x supp 0 ) u. ( y supp 0 ) ) C_ ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) )
111 110 a1i 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( ( x supp 0 ) u. ( y supp 0 ) ) C_ ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) )
112 1 2 102 103 104 109 69 111 rrxmetlem 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) )
113 112 fveq2d 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
114 113 3expa 
 |-  ( ( ( I e. V /\ z e. X ) /\ ( x e. X /\ y e. X ) ) -> ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
115 114 an32s 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( sqrt ` sum_ k e. ( ( x supp 0 ) u. ( y supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
116 101 115 eqtrd 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( x D y ) = ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
117 1 2 rrxmval 
 |-  ( ( I e. V /\ z e. X /\ x e. X ) -> ( z D x ) = ( sqrt ` sum_ k e. ( ( z supp 0 ) u. ( x supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) )
118 117 3adant3r 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( z D x ) = ( sqrt ` sum_ k e. ( ( z supp 0 ) u. ( x supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) )
119 1 2 rrxmval 
 |-  ( ( I e. V /\ z e. X /\ y e. X ) -> ( z D y ) = ( sqrt ` sum_ k e. ( ( z supp 0 ) u. ( y supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) )
120 119 3adant3l 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( z D y ) = ( sqrt ` sum_ k e. ( ( z supp 0 ) u. ( y supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) )
121 118 120 oveq12d 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( ( z D x ) + ( z D y ) ) = ( ( sqrt ` sum_ k e. ( ( z supp 0 ) u. ( x supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. ( ( z supp 0 ) u. ( y supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
122 ssun2 
 |-  ( z supp 0 ) C_ ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) )
123 122 a1i 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( z supp 0 ) C_ ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) )
124 52 110 sstri 
 |-  ( x supp 0 ) C_ ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) )
125 124 a1i 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( x supp 0 ) C_ ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) )
126 123 125 unssd 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( ( z supp 0 ) u. ( x supp 0 ) ) C_ ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) )
127 1 2 102 66 103 109 69 126 rrxmetlem 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> sum_ k e. ( ( z supp 0 ) u. ( x supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) = sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) )
128 127 fveq2d 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( sqrt ` sum_ k e. ( ( z supp 0 ) u. ( x supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) )
129 57 110 sstri 
 |-  ( y supp 0 ) C_ ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) )
130 129 a1i 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( y supp 0 ) C_ ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) )
131 123 130 unssd 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( ( z supp 0 ) u. ( y supp 0 ) ) C_ ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) )
132 1 2 102 66 104 109 69 131 rrxmetlem 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> sum_ k e. ( ( z supp 0 ) u. ( y supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) = sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) )
133 132 fveq2d 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( sqrt ` sum_ k e. ( ( z supp 0 ) u. ( y supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) )
134 128 133 oveq12d 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( ( sqrt ` sum_ k e. ( ( z supp 0 ) u. ( x supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. ( ( z supp 0 ) u. ( y supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) = ( ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
135 121 134 eqtrd 
 |-  ( ( I e. V /\ z e. X /\ ( x e. X /\ y e. X ) ) -> ( ( z D x ) + ( z D y ) ) = ( ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
136 135 3expa 
 |-  ( ( ( I e. V /\ z e. X ) /\ ( x e. X /\ y e. X ) ) -> ( ( z D x ) + ( z D y ) ) = ( ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
137 136 an32s 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( ( z D x ) + ( z D y ) ) = ( ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( x ` k ) ) ^ 2 ) ) + ( sqrt ` sum_ k e. ( ( ( x supp 0 ) u. ( y supp 0 ) ) u. ( z supp 0 ) ) ( ( ( z ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
138 100 116 137 3brtr4d 
 |-  ( ( ( I e. V /\ ( x e. X /\ y e. X ) ) /\ z e. X ) -> ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )
139 138 ralrimiva 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> A. z e. X ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )
140 64 139 jca 
 |-  ( ( I e. V /\ ( x e. X /\ y e. X ) ) -> ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) + ( z D y ) ) ) )
141 140 ralrimivva 
 |-  ( I e. V -> A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) + ( z D y ) ) ) )
142 ovex 
 |-  ( RR ^m I ) e. _V
143 1 142 rabex2 
 |-  X e. _V
144 ismet 
 |-  ( X e. _V -> ( D e. ( Met ` X ) <-> ( D : ( X X. X ) --> RR /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) + ( z D y ) ) ) ) ) )
145 143 144 ax-mp 
 |-  ( D e. ( Met ` X ) <-> ( D : ( X X. X ) --> RR /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) + ( z D y ) ) ) ) )
146 31 141 145 sylanbrc 
 |-  ( I e. V -> D e. ( Met ` X ) )