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 = ( 𝑖 ∈ Fin ↦ ( 𝑥 ∈ ( ℝ ↑m 𝑖 ) , 𝑦 ∈ ( ℝ ↑m 𝑖 ) ↦ ( √ ‘ Σ 𝑘𝑖 ( ( ( 𝑥𝑘 ) − ( 𝑦𝑘 ) ) ↑ 2 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crrn n
1 vi 𝑖
2 cfn Fin
3 vx 𝑥
4 cr
5 cmap m
6 1 cv 𝑖
7 4 6 5 co ( ℝ ↑m 𝑖 )
8 vy 𝑦
9 csqrt
10 vk 𝑘
11 3 cv 𝑥
12 10 cv 𝑘
13 12 11 cfv ( 𝑥𝑘 )
14 cmin
15 8 cv 𝑦
16 12 15 cfv ( 𝑦𝑘 )
17 13 16 14 co ( ( 𝑥𝑘 ) − ( 𝑦𝑘 ) )
18 cexp
19 c2 2
20 17 19 18 co ( ( ( 𝑥𝑘 ) − ( 𝑦𝑘 ) ) ↑ 2 )
21 6 20 10 csu Σ 𝑘𝑖 ( ( ( 𝑥𝑘 ) − ( 𝑦𝑘 ) ) ↑ 2 )
22 21 9 cfv ( √ ‘ Σ 𝑘𝑖 ( ( ( 𝑥𝑘 ) − ( 𝑦𝑘 ) ) ↑ 2 ) )
23 3 8 7 7 22 cmpo ( 𝑥 ∈ ( ℝ ↑m 𝑖 ) , 𝑦 ∈ ( ℝ ↑m 𝑖 ) ↦ ( √ ‘ Σ 𝑘𝑖 ( ( ( 𝑥𝑘 ) − ( 𝑦𝑘 ) ) ↑ 2 ) ) )
24 1 2 23 cmpt ( 𝑖 ∈ Fin ↦ ( 𝑥 ∈ ( ℝ ↑m 𝑖 ) , 𝑦 ∈ ( ℝ ↑m 𝑖 ) ↦ ( √ ‘ Σ 𝑘𝑖 ( ( ( 𝑥𝑘 ) − ( 𝑦𝑘 ) ) ↑ 2 ) ) ) )
25 0 24 wceq n = ( 𝑖 ∈ Fin ↦ ( 𝑥 ∈ ( ℝ ↑m 𝑖 ) , 𝑦 ∈ ( ℝ ↑m 𝑖 ) ↦ ( √ ‘ Σ 𝑘𝑖 ( ( ( 𝑥𝑘 ) − ( 𝑦𝑘 ) ) ↑ 2 ) ) ) )