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