Theorem rrxmetfi

Description: Euclidean space is a metric space. Finite dimensional version. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypothesis	rrxmetfi.1
Assertion	rrxmetfi	$$⊢I\in \mathrm{Fin}\to D\in \mathrm{Met}\left({ℝ}^I\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrxmetfi.1
2		eqid	$$⊢\left\{h\in \left({ℝ}^I\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({ℝ}^I\right)|{finSupp}_0\left(h\right)\right\}$$
3	2 1	rrxmet	$$⊢I\in \mathrm{Fin}\to D\in \mathrm{Met}\left(\left\{h\in \left({ℝ}^I\right)|{finSupp}_0\left(h\right)\right\}\right)$$
4		eqid
5		eqid
6	4 5	rrxbase
7		id	$$⊢I\in \mathrm{Fin}\to I\in \mathrm{Fin}$$
8	7 4 5	rrxbasefi
9	6 8	eqtr3d	$$⊢I\in \mathrm{Fin}\to \left\{h\in \left({ℝ}^I\right)|{finSupp}_0\left(h\right)\right\}={ℝ}^I$$
10	9	fveq2d	$$⊢I\in \mathrm{Fin}\to \mathrm{Met}\left(\left\{h\in \left({ℝ}^I\right)|{finSupp}_0\left(h\right)\right\}\right)=\mathrm{Met}\left({ℝ}^I\right)$$
11	3 10	eleqtrd	$$⊢I\in \mathrm{Fin}\to D\in \mathrm{Met}\left({ℝ}^I\right)$$