Metamath Proof Explorer

Theorem rrnval

Description: The n-dimensional Euclidean space. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypothesis rrnval.1 
|- X = ( RR ^m I )
Assertion rrnval 
|- ( I e. Fin -> ( Rn ` I ) = ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) )

Proof

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