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 35213
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 ↦ (𝑥 ∈ (ℝ ↑m 𝑖), 𝑦 ∈ (ℝ ↑m 𝑖) ↦ (√‘Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2))))
Distinct variable group:   𝑥,𝑖,𝑦,𝑘

Detailed syntax breakdown of Definition df-rrn
StepHypRef Expression
1 crrn 35212 . 2 class n
2 vi . . 3 setvar 𝑖
3 cfn 8505 . . 3 class Fin
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
6 cr 10534 . . . . 5 class
72cv 1537 . . . . 5 class 𝑖
8 cmap 8402 . . . . 5 class m
96, 7, 8co 7149 . . . 4 class (ℝ ↑m 𝑖)
10 vk . . . . . . . . . 10 setvar 𝑘
1110cv 1537 . . . . . . . . 9 class 𝑘
124cv 1537 . . . . . . . . 9 class 𝑥
1311, 12cfv 6343 . . . . . . . 8 class (𝑥𝑘)
145cv 1537 . . . . . . . . 9 class 𝑦
1511, 14cfv 6343 . . . . . . . 8 class (𝑦𝑘)
16 cmin 10868 . . . . . . . 8 class
1713, 15, 16co 7149 . . . . . . 7 class ((𝑥𝑘) − (𝑦𝑘))
18 c2 11689 . . . . . . 7 class 2
19 cexp 13434 . . . . . . 7 class
2017, 18, 19co 7149 . . . . . 6 class (((𝑥𝑘) − (𝑦𝑘))↑2)
217, 20, 10csu 15042 . . . . 5 class Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2)
22 csqrt 14592 . . . . 5 class
2321, 22cfv 6343 . . . 4 class (√‘Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2))
244, 5, 9, 9, 23cmpo 7151 . . 3 class (𝑥 ∈ (ℝ ↑m 𝑖), 𝑦 ∈ (ℝ ↑m 𝑖) ↦ (√‘Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2)))
252, 3, 24cmpt 5132 . 2 class (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑m 𝑖), 𝑦 ∈ (ℝ ↑m 𝑖) ↦ (√‘Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2))))
261, 25wceq 1538 1 wff n = (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑m 𝑖), 𝑦 ∈ (ℝ ↑m 𝑖) ↦ (√‘Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2))))
Colors of variables: wff setvar class
This definition is referenced by:  rrnval  35214
  Copyright terms: Public domain W3C validator