Theorem rrndsmet

Description: D is a metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	rrndsmet.1	$$⊢\phi \to X\in \mathrm{Fin}$$
	rrndsmet.2	$$⊢D=\left(f\in \left({ℝ}^X\right),g\in \left({ℝ}^X\right)⟼\sqrt{\sum _{k\in X}{\left(f\left(k\right)-g\left(k\right)\right)}^2}\right)$$
Assertion	rrndsmet	$$⊢\phi \to D\in \mathrm{Met}\left({ℝ}^X\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrndsmet.1	$$⊢\phi \to X\in \mathrm{Fin}$$
2		rrndsmet.2	$$⊢D=\left(f\in \left({ℝ}^X\right),g\in \left({ℝ}^X\right)⟼\sqrt{\sum _{k\in X}{\left(f\left(k\right)-g\left(k\right)\right)}^2}\right)$$
3	2	a1i	$$⊢\phi \to D=\left(f\in \left({ℝ}^X\right),g\in \left({ℝ}^X\right)⟼\sqrt{\sum _{k\in X}{\left(f\left(k\right)-g\left(k\right)\right)}^2}\right)$$
4		eqid
5		eqid	$$⊢{ℝ}^X={ℝ}^X$$
6	4 5	rrxdsfi
7	1 6	syl
8	3 7	eqtr4d
9		eqid
10	9	rrxmetfi
11	1 10	syl
12	8 11	eqeltrd	$$⊢\phi \to D\in \mathrm{Met}\left({ℝ}^X\right)$$