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

Metamath Proof Explorer

Theorem ehleudis

Description: The Euclidean distance function in a real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023)

Ref Expression
Hypotheses ehleudis.i ⊢ 𝐼 = ( 1 ... 𝑁 )
ehleudis.e ⊢ 𝐸 = ( 𝔼hil ‘ 𝑁 )
ehleudis.x ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
ehleudis.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
Assertion ehleudis ( 𝑁 ∈ ℕ0 → 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 ehleudis.i ⊢ 𝐼 = ( 1 ... 𝑁 )
2 ehleudis.e ⊢ 𝐸 = ( 𝔼hil ‘ 𝑁 )
3 ehleudis.x ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
4 ehleudis.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
5 2 ehlval ⊢ ( 𝑁 ∈ ℕ0 → 𝐸 = ( ℝ^ ‘ ( 1 ... 𝑁 ) ) )
6 5 fveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( dist ‘ 𝐸 ) = ( dist ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) )
7 4 6 eqtrid ⊢ ( 𝑁 ∈ ℕ0 → 𝐷 = ( dist ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) )
8 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
9 1 8 eqeltri ⊢ 𝐼 ∈ Fin
10 1 eqcomi ⊢ ( 1 ... 𝑁 ) = 𝐼
11 10 fveq2i ⊢ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) = ( ℝ^ ‘ 𝐼 )
12 11 fveq2i ⊢ ( dist ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
13 eqid ⊢ ( ℝ^ ‘ 𝐼 ) = ( ℝ^ ‘ 𝐼 )
14 13 3 rrxdsfi ⊢ ( 𝐼 ∈ Fin → ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
15 12 14 eqtrid ⊢ ( 𝐼 ∈ Fin → ( dist ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
16 9 15 mp1i ⊢ ( 𝑁 ∈ ℕ0 → ( dist ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
17 7 16 eqtrd ⊢ ( 𝑁 ∈ ℕ0 → 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )