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	$⊢ I = (1 \dots N)$
	ehleudis.e	$⊢ E = 𝔼_{hil} (N)$
	ehleudis.x	$⊢ X = ℝ^{I}$
	ehleudis.d	$⊢ D = dist (E)$
Assertion	ehleudis	$⊢ N \in ℕ_{0} \to D = (f \in X, g \in X ⟼ \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		fzfi	$⊢ (1 \dots N) \in Fin$
9	1 8	eqeltri	$⊢ I \in Fin$
10	1	eqcomi	$⊢ (1 \dots N) = I$
11	10	fveq2i	$⊢ (1 \dots N) = I$
12	11	fveq2i	$⊢ dist ((1 \dots N)) = dist (I)$
13		eqid	$⊢ I = I$
14	13 3	rrxdsfi	$⊢ I \in Fin \to dist (I) = (f \in X, g \in X ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}})$
15	12 14	syl5eq	$⊢ I \in Fin \to dist ((1 \dots N)) = (f \in X, g \in X ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}})$
16	9 15	mp1i	$⊢ N \in ℕ_{0} \to dist ((1 \dots N)) = (f \in X, g \in X ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}})$
17	7 16	eqtrd	$⊢ N \in ℕ_{0} \to D = (f \in X, g \in X ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}})$

Metamath Proof Explorer