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

Definition df-rrn 26653
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 26652 . 2  class  Rn
2 vi . . 3  set  i
3 cfn 6879 . . 3  class  Fin
4 vx . . . 4  set  x
5 vy . . . 4  set  y
6 cr 8752 . . . . 5  class  RR
72cv 1631 . . . . 5  class  i
8 cmap 6788 . . . . 5  class  ^m
96, 7, 8co 5874 . . . 4  class  ( RR 
^m  i )
10 vk . . . . . . . . . 10  set  k
1110cv 1631 . . . . . . . . 9  class  k
124cv 1631 . . . . . . . . 9  class  x
1311, 12cfv 5271 . . . . . . . 8  class  ( x `
 k )
145cv 1631 . . . . . . . . 9  class  y
1511, 14cfv 5271 . . . . . . . 8  class  ( y `
 k )
16 cmin 9053 . . . . . . . 8  class  -
1713, 15, 16co 5874 . . . . . . 7  class  ( ( x `  k )  -  ( y `  k ) )
18 c2 9811 . . . . . . 7  class  2
19 cexp 11120 . . . . . . 7  class  ^
2017, 18, 19co 5874 . . . . . 6  class  ( ( ( x `  k
)  -  ( y `
 k ) ) ^ 2 )
217, 20, 10csu 12174 . . . . 5  class  sum_ k  e.  i  ( (
( x `  k
)  -  ( y `
 k ) ) ^ 2 )
22 csqr 11734 . . . . 5  class  sqr
2321, 22cfv 5271 . . . 4  class  ( sqr `  sum_ k  e.  i  ( ( ( x `
 k )  -  ( y `  k
) ) ^ 2 ) )
244, 5, 9, 9, 23cmpt2 5876 . . 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 4093 . 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 1632 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  26654
  Copyright terms: Public domain W3C validator