Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rrn Unicode version

Definition df-rrn 26219
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.)
Assertion
Ref Expression
df-rrn  |-  Rn  =  ( i  e.  Fin  |->  ( x  e.  ( RR  ^m  i ) ,  y  e.  ( RR 
^m  i )  |->  ( sqr `  sum_ k  e.  i  ( (
( x `  k
)  -  ( y `
 k ) ) ^ 2 ) ) ) )
Distinct variable group:    x, i, y, k

Detailed syntax breakdown of Definition df-rrn
StepHypRef Expression
1 crrn 26218 . 2  class  Rn
2 vi . . 3  set  i
3 cfn 7038 . . 3  class  Fin
4 vx . . . 4  set  x
5 vy . . . 4  set  y
6 cr 8915 . . . . 5  class  RR
72cv 1648 . . . . 5  class  i
8 cmap 6947 . . . . 5  class  ^m
96, 7, 8co 6013 . . . 4  class  ( RR 
^m  i )
10 vk . . . . . . . . . 10  set  k
1110cv 1648 . . . . . . . . 9  class  k
124cv 1648 . . . . . . . . 9  class  x
1311, 12cfv 5387 . . . . . . . 8  class  ( x `
 k )
145cv 1648 . . . . . . . . 9  class  y
1511, 14cfv 5387 . . . . . . . 8  class  ( y `
 k )
16 cmin 9216 . . . . . . . 8  class  -
1713, 15, 16co 6013 . . . . . . 7  class  ( ( x `  k )  -  ( y `  k ) )
18 c2 9974 . . . . . . 7  class  2
19 cexp 11302 . . . . . . 7  class  ^
2017, 18, 19co 6013 . . . . . 6  class  ( ( ( x `  k
)  -  ( y `
 k ) ) ^ 2 )
217, 20, 10csu 12399 . . . . 5  class  sum_ k  e.  i  ( (
( x `  k
)  -  ( y `
 k ) ) ^ 2 )
22 csqr 11958 . . . . 5  class  sqr
2321, 22cfv 5387 . . . 4  class  ( sqr `  sum_ k  e.  i  ( ( ( x `
 k )  -  ( y `  k
) ) ^ 2 ) )
244, 5, 9, 9, 23cmpt2 6015 . . 3  class  ( x  e.  ( RR  ^m  i ) ,  y  e.  ( RR  ^m  i )  |->  ( sqr `  sum_ k  e.  i  ( ( ( x `
 k )  -  ( y `  k
) ) ^ 2 ) ) )
252, 3, 24cmpt 4200 . 2  class  ( i  e.  Fin  |->  ( x  e.  ( RR  ^m  i ) ,  y  e.  ( RR  ^m  i )  |->  ( sqr `  sum_ k  e.  i  ( ( ( x `
 k )  -  ( y `  k
) ) ^ 2 ) ) ) )
261, 25wceq 1649 1  wff  Rn  =  ( i  e.  Fin  |->  ( x  e.  ( RR  ^m  i ) ,  y  e.  ( RR 
^m  i )  |->  ( sqr `  sum_ k  e.  i  ( (
( x `  k
)  -  ( y `
 k ) ) ^ 2 ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  rrnval  26220
  Copyright terms: Public domain W3C validator