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 36694
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 36693 . 2 class n
2 vi . . 3 setvar 𝑖
3 cfn 8939 . . 3 class Fin
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
6 cr 11109 . . . . 5 class
72cv 1541 . . . . 5 class 𝑖
8 cmap 8820 . . . . 5 class m
96, 7, 8co 7409 . . . 4 class (ℝ ↑m 𝑖)
10 vk . . . . . . . . . 10 setvar 𝑘
1110cv 1541 . . . . . . . . 9 class 𝑘
124cv 1541 . . . . . . . . 9 class 𝑥
1311, 12cfv 6544 . . . . . . . 8 class (𝑥𝑘)
145cv 1541 . . . . . . . . 9 class 𝑦
1511, 14cfv 6544 . . . . . . . 8 class (𝑦𝑘)
16 cmin 11444 . . . . . . . 8 class
1713, 15, 16co 7409 . . . . . . 7 class ((𝑥𝑘) − (𝑦𝑘))
18 c2 12267 . . . . . . 7 class 2
19 cexp 14027 . . . . . . 7 class
2017, 18, 19co 7409 . . . . . 6 class (((𝑥𝑘) − (𝑦𝑘))↑2)
217, 20, 10csu 15632 . . . . 5 class Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2)
22 csqrt 15180 . . . . 5 class
2321, 22cfv 6544 . . . 4 class (√‘Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2))
244, 5, 9, 9, 23cmpo 7411 . . 3 class (𝑥 ∈ (ℝ ↑m 𝑖), 𝑦 ∈ (ℝ ↑m 𝑖) ↦ (√‘Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2)))
252, 3, 24cmpt 5232 . 2 class (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑m 𝑖), 𝑦 ∈ (ℝ ↑m 𝑖) ↦ (√‘Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2))))
261, 25wceq 1542 1 wff n = (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑m 𝑖), 𝑦 ∈ (ℝ ↑m 𝑖) ↦ (√‘Σ𝑘𝑖 (((𝑥𝑘) − (𝑦𝑘))↑2))))
Colors of variables: wff setvar class
This definition is referenced by:  rrnval  36695
  Copyright terms: Public domain W3C validator