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	syl5eq	⊢ ( 𝑁 ∈ ℕ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 ) ) )