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

Metamath Proof Explorer

Theorem rrnmval

Description: The value of the Euclidean metric. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypothesis rrnval.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
Assertion rrnmval ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 rrnval.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
2 1 rrnval ⊢ ( 𝐼 ∈ Fin → ( ℝn ‘ 𝐼 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
3 2 3ad2ant1 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ℝn ‘ 𝐼 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
4 fveq1 ⊢ ( 𝑥 = 𝐹 → ( 𝑥 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
5 fveq1 ⊢ ( 𝑦 = 𝐺 → ( 𝑦 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
6 4 5 oveqan12d ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) )
7 6 oveq1d ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
8 7 sumeq2sdv ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) → Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
9 8 fveq2d ⊢ ( ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
10 9 adantl ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑥 = 𝐹 ∧ 𝑦 = 𝐺 ) ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
11 simp2 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐹 ∈ 𝑋 )
12 simp3 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐺 ∈ 𝑋 )
13 fvexd ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ V )
14 3 10 11 12 13 ovmpod ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )