Metamath Proof Explorer

Definition df-rrn

Description: Define n-dimensional Euclidean space as a metric space with the standard Euclidean norm given by the quadratic mean. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion 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 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crrn 
 |-  Rn
1 vi 
 |-  i
2 cfn 
 |-  Fin
3 vx 
 |-  x
4 cr 
 |-  RR
5 cmap 
 |-  ^m
6 1 cv 
 |-  i
7 4 6 5 co 
 |-  ( RR ^m i )
8 vy 
 |-  y
9 csqrt 
 |-  sqrt
10 vk 
 |-  k
11 3 cv 
 |-  x
12 10 cv 
 |-  k
13 12 11 cfv 
 |-  ( x ` k )
14 cmin 
 |-  -
15 8 cv 
 |-  y
16 12 15 cfv 
 |-  ( y ` k )
17 13 16 14 co 
 |-  ( ( x ` k ) - ( y ` k ) )
18 cexp 
 |-  ^
19 c2 
 |-  2
20 17 19 18 co 
 |-  ( ( ( x ` k ) - ( y ` k ) ) ^ 2 )
21 6 20 10 csu 
 |-  sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 )
22 21 9 cfv 
 |-  ( sqrt ` sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) )
23 3 8 7 7 22 cmpo 
 |-  ( x e. ( RR ^m i ) , y e. ( RR ^m i ) |-> ( sqrt ` sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
24 1 2 23 cmpt 
 |-  ( i e. Fin |-> ( x e. ( RR ^m i ) , y e. ( RR ^m i ) |-> ( sqrt ` sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
25 0 24 wceq 
 |-  Rn = ( i e. Fin |-> ( x e. ( RR ^m i ) , y e. ( RR ^m i ) |-> ( sqrt ` sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) )