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

Definition df-rrn 32578
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 n = (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑𝑚 𝑖), 𝑦 ∈ (ℝ ↑𝑚 𝑖) ↦ (√‘Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2))))
Distinct variable group:   𝑥,𝑖,𝑦,𝑘

Detailed syntax breakdown of Definition df-rrn
StepHypRef Expression
1 crrn 32577 . 2 class n
2 vi . . 3 setvar 𝑖
3 cfn 7818 . . 3 class Fin
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
6 cr 9791 . . . . 5 class
72cv 1473 . . . . 5 class 𝑖
8 cmap 7721 . . . . 5 class 𝑚
96, 7, 8co 6526 . . . 4 class (ℝ ↑𝑚 𝑖)
10 vk . . . . . . . . . 10 setvar 𝑘
1110cv 1473 . . . . . . . . 9 class 𝑘
124cv 1473 . . . . . . . . 9 class 𝑥
1311, 12cfv 5789 . . . . . . . 8 class (𝑥𝑘)
145cv 1473 . . . . . . . . 9 class 𝑦
1511, 14cfv 5789 . . . . . . . 8 class (𝑦𝑘)
16 cmin 10117 . . . . . . . 8 class
1713, 15, 16co 6526 . . . . . . 7 class ((𝑥𝑘) − (𝑦𝑘))
18 c2 10919 . . . . . . 7 class 2
19 cexp 12679 . . . . . . 7 class
2017, 18, 19co 6526 . . . . . 6 class (((𝑥𝑘) − (𝑦𝑘))↑2)
217, 20, 10csu 14212 . . . . 5 class Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2)
22 csqrt 13769 . . . . 5 class
2321, 22cfv 5789 . . . 4 class (√‘Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2))
244, 5, 9, 9, 23cmpt2 6528 . . 3 class (𝑥 ∈ (ℝ ↑𝑚 𝑖), 𝑦 ∈ (ℝ ↑𝑚 𝑖) ↦ (√‘Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2)))
252, 3, 24cmpt 4637 . 2 class (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑𝑚 𝑖), 𝑦 ∈ (ℝ ↑𝑚 𝑖) ↦ (√‘Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2))))
261, 25wceq 1474 1 wff n = (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑𝑚 𝑖), 𝑦 ∈ (ℝ ↑𝑚 𝑖) ↦ (√‘Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2))))
Colors of variables: wff setvar class
This definition is referenced by:  rrnval  32579
  Copyright terms: Public domain W3C validator