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