Metamath Proof Explorer

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 ⊢ φ → X ∈ Fin
rrndsmet.2 ⊢ D = f ∈ ℝ X , g ∈ ℝ X ⟼ ∑ k ∈ X f ⁡ k − g ⁡ k 2
Assertion rrndsmet ⊢ φ → D ∈ Met ⁡ ℝ X

Proof

Step Hyp Ref Expression
1 rrndsmet.1 ⊢ φ → X ∈ Fin
2 rrndsmet.2 ⊢ D = f ∈ ℝ X , g ∈ ℝ X ⟼ ∑ k ∈ X f ⁡ k − g ⁡ k 2
3 2 a1i ⊢ φ → D = f ∈ ℝ X , g ∈ ℝ X ⟼ ∑ k ∈ X f ⁡ k − g ⁡ k 2
4 eqid ⊢ X = X
5 eqid ⊢ ℝ X = ℝ X
6 4 5 rrxdsfi ⊢ X ∈ Fin → dist ⁡ X = f ∈ ℝ X , g ∈ ℝ X ⟼ ∑ k ∈ X f ⁡ k − g ⁡ k 2
7 1 6 syl ⊢ φ → dist ⁡ X = f ∈ ℝ X , g ∈ ℝ X ⟼ ∑ k ∈ X f ⁡ k − g ⁡ k 2
8 3 7 eqtr4d ⊢ φ → D = dist ⁡ X
9 eqid ⊢ dist ⁡ X = dist ⁡ X
10 9 rrxmetfi ⊢ X ∈ Fin → dist ⁡ X ∈ Met ⁡ ℝ X
11 1 10 syl ⊢ φ → dist ⁡ X ∈ Met ⁡ ℝ X
12 8 11 eqeltrd ⊢ φ → D ∈ Met ⁡ ℝ X