Metamath Proof Explorer

Definition 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 ∈ Fin ⟼ x ∈ ℝ i , y ∈ ℝ i ⟼ ∑ k ∈ 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 √
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 ∑ k ∈ i x ⁡ k − y ⁡ k 2
22 21 9 cfv class ∑ k ∈ i x ⁡ k − y ⁡ k 2
23 3 8 7 7 22 cmpo class x ∈ ℝ i , y ∈ ℝ i ⟼ ∑ k ∈ i x ⁡ k − y ⁡ k 2
24 1 2 23 cmpt class i ∈ Fin ⟼ x ∈ ℝ i , y ∈ ℝ i ⟼ ∑ k ∈ i x ⁡ k − y ⁡ k 2
25 0 24 wceq wff ℝ n = i ∈ Fin ⟼ x ∈ ℝ i , y ∈ ℝ i ⟼ ∑ k ∈ i x ⁡ k − y ⁡ k 2