Step |
Hyp |
Ref |
Expression |
1 |
|
rrnval.1 |
|- X = ( RR ^m I ) |
2 |
|
oveq2 |
|- ( i = I -> ( RR ^m i ) = ( RR ^m I ) ) |
3 |
2 1
|
eqtr4di |
|- ( i = I -> ( RR ^m i ) = X ) |
4 |
|
sumeq1 |
|- ( i = I -> sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) |
5 |
4
|
fveq2d |
|- ( i = I -> ( sqrt ` sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) |
6 |
3 3 5
|
mpoeq123dv |
|- ( i = I -> ( x e. ( RR ^m i ) , y e. ( RR ^m i ) |-> ( 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 ) ) ) ) |
7 |
|
df-rrn |
|- Rn = ( i e. Fin |-> ( x e. ( RR ^m i ) , y e. ( RR ^m i ) |-> ( sqrt ` sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) ) |
8 |
|
fvrn0 |
|- ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) e. ( ran sqrt u. { (/) } ) |
9 |
8
|
rgen2w |
|- A. x e. X A. y e. X ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) e. ( ran sqrt u. { (/) } ) |
10 |
|
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 ) ) ) |
11 |
10
|
fmpo |
|- ( A. x e. X A. y e. X ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) e. ( ran sqrt u. { (/) } ) <-> ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) : ( X X. X ) --> ( ran sqrt u. { (/) } ) ) |
12 |
9 11
|
mpbi |
|- ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) : ( X X. X ) --> ( ran sqrt u. { (/) } ) |
13 |
|
ovex |
|- ( RR ^m I ) e. _V |
14 |
1 13
|
eqeltri |
|- X e. _V |
15 |
14 14
|
xpex |
|- ( X X. X ) e. _V |
16 |
|
cnex |
|- CC e. _V |
17 |
|
sqrtf |
|- sqrt : CC --> CC |
18 |
|
frn |
|- ( sqrt : CC --> CC -> ran sqrt C_ CC ) |
19 |
17 18
|
ax-mp |
|- ran sqrt C_ CC |
20 |
16 19
|
ssexi |
|- ran sqrt e. _V |
21 |
|
p0ex |
|- { (/) } e. _V |
22 |
20 21
|
unex |
|- ( ran sqrt u. { (/) } ) e. _V |
23 |
|
fex2 |
|- ( ( ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) : ( X X. X ) --> ( ran sqrt u. { (/) } ) /\ ( X X. X ) e. _V /\ ( ran sqrt u. { (/) } ) e. _V ) -> ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) e. _V ) |
24 |
12 15 22 23
|
mp3an |
|- ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) e. _V |
25 |
6 7 24
|
fvmpt |
|- ( I e. Fin -> ( Rn ` I ) = ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) ) |