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

Metamath Proof Explorer

Theorem ehleudisval

Description: The value of 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 ehleudisval ( ( 𝑁 ∈ ℕ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 7 oveqd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐹 𝐷 𝐺 ) = ( 𝐹 ( dist ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) 𝐺 ) )
9 8 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) = ( 𝐹 ( dist ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) 𝐺 ) )
10 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
11 1 10 eqeltri ⊢ 𝐼 ∈ Fin
12 3 eleq2i ⊢ ( 𝐹 ∈ 𝑋 ↔ 𝐹 ∈ ( ℝ ↑m 𝐼 ) )
13 12 biimpi ⊢ ( 𝐹 ∈ 𝑋 → 𝐹 ∈ ( ℝ ↑m 𝐼 ) )
14 13 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐹 ∈ ( ℝ ↑m 𝐼 ) )
15 3 eleq2i ⊢ ( 𝐺 ∈ 𝑋 ↔ 𝐺 ∈ ( ℝ ↑m 𝐼 ) )
16 15 biimpi ⊢ ( 𝐺 ∈ 𝑋 → 𝐺 ∈ ( ℝ ↑m 𝐼 ) )
17 16 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐺 ∈ ( ℝ ↑m 𝐼 ) )
18 eqid ⊢ ( ℝ ↑m 𝐼 ) = ( ℝ ↑m 𝐼 )
19 1 eqcomi ⊢ ( 1 ... 𝑁 ) = 𝐼
20 19 fveq2i ⊢ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) = ( ℝ^ ‘ 𝐼 )
21 20 fveq2i ⊢ ( dist ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
22 18 21 rrxdsfival ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝐺 ∈ ( ℝ ↑m 𝐼 ) ) → ( 𝐹 ( dist ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
23 11 14 17 22 mp3an2i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 ( dist ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
24 9 23 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )