Definition df-rrn 38760

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

Step	Hyp	Ref	Expression
1		crrn 38759	. 2 class ℝn
2		vi	. . 3 setvar 𝑖
3		cfn 8973	. . 3 class Fin
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6		cr 11199	. . . . 5 class ℝ
7	2	cv 1569	. . . . 5 class 𝑖
8		cmap 8847	. . . . 5 class ↑m
9	6, 7, 8	co 7420	. . . 4 class (ℝ ↑m 𝑖)
10		vk	. . . . . . . . . 10 setvar 𝑘
11	10	cv 1569	. . . . . . . . 9 class 𝑘
12	4	cv 1569	. . . . . . . . 9 class 𝑥
13	11, 12	cfv 6538	. . . . . . . 8 class (𝑥‘𝑘)
14	5	cv 1569	. . . . . . . . 9 class 𝑦
15	11, 14	cfv 6538	. . . . . . . 8 class (𝑦‘𝑘)
16		cmin 11541	. . . . . . . 8 class −
17	13, 15, 16	co 7420	. . . . . . 7 class ((𝑥‘𝑘) − (𝑦‘𝑘))
18		c2 12397	. . . . . . 7 class 2
19		cexp 14204	. . . . . . 7 class ↑
20	17, 18, 19	co 7420	. . . . . 6 class (((𝑥‘𝑘) − (𝑦‘𝑘))↑2)
21	7, 20, 10	csu 15853	. . . . 5 class Σ𝑘 ∈ 𝑖 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2)
22		csqrt 15400	. . . . 5 class √
23	21, 22	cfv 6538	. . . 4 class (√‘Σ𝑘 ∈ 𝑖 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
24	4, 5, 9, 9, 23	cmpo 7422	. . 3 class (𝑥 ∈ (ℝ ↑m 𝑖), 𝑦 ∈ (ℝ ↑m 𝑖) ↦ (√‘Σ𝑘 ∈ 𝑖 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
25	2, 3, 24	cmpt 5186	. 2 class (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑m 𝑖), 𝑦 ∈ (ℝ ↑m 𝑖) ↦ (√‘Σ𝑘 ∈ 𝑖 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))))
26	1, 25	wceq 1570	1 wff ℝn = (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑m 𝑖), 𝑦 ∈ (ℝ ↑m 𝑖) ↦ (√‘Σ𝑘 ∈ 𝑖 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))))

This definition is used by:  rrnval  38761