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