df-rrn

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)

		Ref	Expression
	Assertion	df-rrn	$⊢ ℝ^{n} = (i \in Fin ⟼ (x \in (ℝ^{i}), y \in (ℝ^{i}) ⟼ \sqrt{\sum_{k \in i} {(x (k) - y (k))}^{2}}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrn	$class ℝ^{n}$
1		vi	$setvar i$
2		cfn	$class Fin$
3		vx	$setvar x$
4		cr	$class ℝ$
5		cmap	$class ↑_{𝑚}$
6	1	cv	$setvar i$
7	4 6 5	co	$class (ℝ^{i})$
8		vy	$setvar y$
9		csqrt	$class \sqrt$
10		vk	$setvar k$
11	3	cv	$setvar x$
12	10	cv	$setvar k$
13	12 11	cfv	$class x (k)$
14		cmin	$class -$
15	8	cv	$setvar y$
16	12 15	cfv	$class y (k)$
17	13 16 14	co	$class (x (k) - y (k))$
18		cexp	$class^$
19		c2	$class 2$
20	17 19 18	co	$class {(x (k) - y (k))}^{2}$
21	6 20 10	csu	$class \sum_{k \in i} {(x (k) - y (k))}^{2}$
22	21 9	cfv	$class \sqrt{\sum_{k \in i} {(x (k) - y (k))}^{2}}$
23	3 8 7 7 22	cmpo	$class (x \in (ℝ^{i}), y \in (ℝ^{i}) ⟼ \sqrt{\sum_{k \in i} {(x (k) - y (k))}^{2}})$
24	1 2 23	cmpt	$class (i \in Fin ⟼ (x \in (ℝ^{i}), y \in (ℝ^{i}) ⟼ \sqrt{\sum_{k \in i} {(x (k) - y (k))}^{2}}))$
25	0 24	wceq	$wff ℝ^{n} = (i \in Fin ⟼ (x \in (ℝ^{i}), y \in (ℝ^{i}) ⟼ \sqrt{\sum_{k \in i} {(x (k) - y (k))}^{2}}))$

Metamath Proof Explorer

Definition df-rrn

Detailed syntax breakdown