This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) ) )