Theorem rrndsxmet

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

	Ref	Expression
Hypotheses	rrndsxmet.1	$$⊢\phi \to X\in \mathrm{Fin}$$
	rrndsxmet.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	rrndsxmet	$$⊢\phi \to D\in \mathrm{\infty Met}\left({ℝ}^X\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrndsxmet.1	$$⊢\phi \to X\in \mathrm{Fin}$$
2		rrndsxmet.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	1 2	rrndsmet	$$⊢\phi \to D\in \mathrm{Met}\left({ℝ}^X\right)$$
4		metxmet	$$⊢D\in \mathrm{Met}\left({ℝ}^X\right)\to D\in \mathrm{\infty Met}\left({ℝ}^X\right)$$
5	3 4	syl	$$⊢\phi \to D\in \mathrm{\infty Met}\left({ℝ}^X\right)$$