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	syl5eq	⊢ ( 𝑁 ∈ ℕ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	syl5eq	⊢ ( 𝐼 ∈ Fin → ( dist ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
16	9 15	mp1i	⊢ ( 𝑁 ∈ ℕ0 → ( dist ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
17	7 16	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )