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

Definition df-rrn 26550
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 26549 . 2  class  Rn
2 vi . . 3  set  i
3 cfn 6863 . . 3  class  Fin
4 vx . . . 4  set  x
5 vy . . . 4  set  y
6 cr 8736 . . . . 5  class  RR
72cv 1622 . . . . 5  class  i
8 cmap 6772 . . . . 5  class  ^m
96, 7, 8co 5858 . . . 4  class  ( RR 
^m  i )
10 vk . . . . . . . . . 10  set  k
1110cv 1622 . . . . . . . . 9  class  k
124cv 1622 . . . . . . . . 9  class  x
1311, 12cfv 5255 . . . . . . . 8  class  ( x `
 k )
145cv 1622 . . . . . . . . 9  class  y
1511, 14cfv 5255 . . . . . . . 8  class  ( y `
 k )
16 cmin 9037 . . . . . . . 8  class  -
1713, 15, 16co 5858 . . . . . . 7  class  ( ( x `  k )  -  ( y `  k ) )
18 c2 9795 . . . . . . 7  class  2
19 cexp 11104 . . . . . . 7  class  ^
2017, 18, 19co 5858 . . . . . 6  class  ( ( ( x `  k
)  -  ( y `
 k ) ) ^ 2 )
217, 20, 10csu 12158 . . . . 5  class  sum_ k  e.  i  ( (
( x `  k
)  -  ( y `
 k ) ) ^ 2 )
22 csqr 11718 . . . . 5  class  sqr
2321, 22cfv 5255 . . . 4  class  ( sqr `  sum_ k  e.  i  ( ( ( x `
 k )  -  ( y `  k
) ) ^ 2 ) )
244, 5, 9, 9, 23cmpt2 5860 . . 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 4077 . 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 1623 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  26551
  Copyright terms: Public domain W3C validator