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	$⊢ I = (1 \dots N)$
	ehleudis.e	$⊢ E = 𝔼_{hil} (N)$
	ehleudis.x	$⊢ X = ℝ^{I}$
	ehleudis.d	$⊢ D = dist (E)$
Assertion	ehleudisval	$⊢ (N \in ℕ_{0} \land F \in X \land G \in X) \to F D G = \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$

Step	Hyp	Ref	Expression
1		ehleudis.i	$⊢ I = (1 \dots N)$
2		ehleudis.e	$⊢ E = 𝔼_{hil} (N)$
3		ehleudis.x	$⊢ X = ℝ^{I}$
4		ehleudis.d	$⊢ D = dist (E)$
5	2	ehlval	$⊢ N \in ℕ_{0} \to E = (1 \dots N)$
6	5	fveq2d	$⊢ N \in ℕ_{0} \to dist (E) = dist ((1 \dots N))$
7	4 6	syl5eq	$⊢ N \in ℕ_{0} \to D = dist ((1 \dots N))$
8	7	oveqd	$⊢ N \in ℕ_{0} \to F D G = F dist ((1 \dots N)) G$
9	8	3ad2ant1	$⊢ (N \in ℕ_{0} \land F \in X \land G \in X) \to F D G = F dist ((1 \dots N)) G$
10		fzfi	$⊢ (1 \dots N) \in Fin$
11	1 10	eqeltri	$⊢ I \in Fin$
12	3	eleq2i	$⊢ F \in X \leftrightarrow F \in (ℝ^{I})$
13	12	biimpi	$⊢ F \in X \to F \in (ℝ^{I})$
14	13	3ad2ant2	$⊢ (N \in ℕ_{0} \land F \in X \land G \in X) \to F \in (ℝ^{I})$
15	3	eleq2i	$⊢ G \in X \leftrightarrow G \in (ℝ^{I})$
16	15	biimpi	$⊢ G \in X \to G \in (ℝ^{I})$
17	16	3ad2ant3	$⊢ (N \in ℕ_{0} \land F \in X \land G \in X) \to G \in (ℝ^{I})$
18		eqid	$⊢ ℝ^{I} = ℝ^{I}$
19	1	eqcomi	$⊢ (1 \dots N) = I$
20	19	fveq2i	$⊢ (1 \dots N) = I$
21	20	fveq2i	$⊢ dist ((1 \dots N)) = dist (I)$
22	18 21	rrxdsfival	$⊢ (I \in Fin \land F \in (ℝ^{I}) \land G \in (ℝ^{I})) \to F dist ((1 \dots N)) G = \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$
23	11 14 17 22	mp3an2i	$⊢ (N \in ℕ_{0} \land F \in X \land G \in X) \to F dist ((1 \dots N)) G = \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$
24	9 23	eqtrd	$⊢ (N \in ℕ_{0} \land F \in X \land G \in X) \to F D G = \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$

Metamath Proof Explorer