This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rrxmetfi

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

Ref Expression
Hypothesis rrxmetfi.1 ⊢ D = dist ⁡ I
Assertion rrxmetfi ⊢ I ∈ Fin → D ∈ Met ⁡ ℝ I

Proof

Step Hyp Ref Expression
1 rrxmetfi.1 ⊢ D = dist ⁡ I
2 eqid ⊢ h ∈ ℝ I | finSupp 0 ⁡ h = h ∈ ℝ I | finSupp 0 ⁡ h
3 2 1 rrxmet ⊢ I ∈ Fin → D ∈ Met ⁡ h ∈ ℝ I | finSupp 0 ⁡ h
4 eqid ⊢ I = I
5 eqid ⊢ Base I = Base I
6 4 5 rrxbase ⊢ I ∈ Fin → Base I = h ∈ ℝ I | finSupp 0 ⁡ h
7 id ⊢ I ∈ Fin → I ∈ Fin
8 7 4 5 rrxbasefi ⊢ I ∈ Fin → Base I = ℝ I
9 6 8 eqtr3d ⊢ I ∈ Fin → h ∈ ℝ I | finSupp 0 ⁡ h = ℝ I
10 9 fveq2d ⊢ I ∈ Fin → Met ⁡ h ∈ ℝ I | finSupp 0 ⁡ h = Met ⁡ ℝ I
11 3 10 eleqtrd ⊢ I ∈ Fin → D ∈ Met ⁡ ℝ I