Definition df-rrn 32795

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

Step	Hyp	Ref	Expression
1		crrn 32794	. 2 class ℝn
2		vi	. . 3 setvar 𝑖
3		cfn 7841	. . 3 class Fin
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6		cr 9814	. . . . 5 class ℝ
7	2	cv 1474	. . . . 5 class 𝑖
8		cmap 7744	. . . . 5 class ↑𝑚
9	6, 7, 8	co 6549	. . . 4 class (ℝ ↑𝑚 𝑖)
10		vk	. . . . . . . . . 10 setvar 𝑘
11	10	cv 1474	. . . . . . . . 9 class 𝑘
12	4	cv 1474	. . . . . . . . 9 class 𝑥
13	11, 12	cfv 5804	. . . . . . . 8 class (𝑥‘𝑘)
14	5	cv 1474	. . . . . . . . 9 class 𝑦
15	11, 14	cfv 5804	. . . . . . . 8 class (𝑦‘𝑘)
16		cmin 10145	. . . . . . . 8 class −
17	13, 15, 16	co 6549	. . . . . . 7 class ((𝑥‘𝑘) − (𝑦‘𝑘))
18		c2 10947	. . . . . . 7 class 2
19		cexp 12722	. . . . . . 7 class ↑
20	17, 18, 19	co 6549	. . . . . 6 class (((𝑥‘𝑘) − (𝑦‘𝑘))↑2)
21	7, 20, 10	csu 14264	. . . . 5 class Σ𝑘 ∈ 𝑖 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2)
22		csqrt 13821	. . . . 5 class √
23	21, 22	cfv 5804	. . . 4 class (√‘Σ𝑘 ∈ 𝑖 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
24	4, 5, 9, 9, 23	cmpt2 6551	. . 3 class (𝑥 ∈ (ℝ ↑𝑚 𝑖), 𝑦 ∈ (ℝ ↑𝑚 𝑖) ↦ (√‘Σ𝑘 ∈ 𝑖 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
25	2, 3, 24	cmpt 4643	. 2 class (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑𝑚 𝑖), 𝑦 ∈ (ℝ ↑𝑚 𝑖) ↦ (√‘Σ𝑘 ∈ 𝑖 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))))
26	1, 25	wceq 1475	1 wff ℝn = (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑𝑚 𝑖), 𝑦 ∈ (ℝ ↑𝑚 𝑖) ↦ (√‘Σ𝑘 ∈ 𝑖 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))))

This definition is referenced by:  rrnval  32796