Metamath Proof Explorer

Theorem rrxdsfival

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

Ref Expression
Hypotheses rrxdsfival.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
rrxdsfival.d ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
Assertion rrxdsfival ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 rrxdsfival.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
2 rrxdsfival.d ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
3 eqid ⊢ ( ℝ^ ‘ 𝐼 ) = ( ℝ^ ‘ 𝐼 )
4 3 1 rrxdsfi ⊢ ( 𝐼 ∈ Fin → ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
5 2 4 syl5eq ⊢ ( 𝐼 ∈ Fin → 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
6 5 oveqd ⊢ ( 𝐼 ∈ Fin → ( 𝐹 𝐷 𝐺 ) = ( 𝐹 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) 𝐺 ) )
7 6 3ad2ant1 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) = ( 𝐹 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) 𝐺 ) )
8 eqidd ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
9 fveq1 ⊢ ( 𝑥 = 𝐹 → ( 𝑥 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
10 fveq1 ⊢ ( 𝑦 = 𝐺 → ( 𝑦 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
11 9 10 oveqan12d ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) )
12 11 oveq1d ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
13 12 sumeq2sdv ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) → Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
14 13 fveq2d ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
15 14 adantl ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
16 simp2 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐹 ∈ 𝑋 )
17 simp3 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐺 ∈ 𝑋 )
18 fvexd ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ V )
19 8 15 16 17 18 ovmpod ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
20 7 19 eqtrd ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )