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