Metamath Proof Explorer

Theorem rrxmfval

Description: The value of the Euclidean metric. Compare with rrnval . (Contributed by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Hypotheses rrxmval.1 ⊢ X = h ∈ ℝ I | finSupp 0 ⁡ h
rrxmval.d ⊢ D = dist ⁡ I
Assertion rrxmfval ⊢ I ∈ V → D = f ∈ X , g ∈ X ⟼ ∑ k ∈ supp 0 ⁡ f ∪ supp 0 ⁡ g f ⁡ k − g ⁡ k 2

Proof

Step Hyp Ref Expression
1 rrxmval.1 ⊢ X = h ∈ ℝ I | finSupp 0 ⁡ h
2 rrxmval.d ⊢ D = dist ⁡ I
3 eqid ⊢ f ∈ Base I , g ∈ Base I ⟼ ∑ ℝ fld x ∈ I f ⁡ x − g ⁡ x 2 = f ∈ Base I , g ∈ Base I ⟼ ∑ ℝ fld x ∈ I f ⁡ x − g ⁡ x 2
4 fvex ⊢ ∑ ℝ fld x ∈ I f ⁡ x − g ⁡ x 2 ∈ V
5 3 4 fnmpoi ⊢ f ∈ Base I , g ∈ Base I ⟼ ∑ ℝ fld x ∈ I f ⁡ x − g ⁡ x 2 Fn Base I × Base I
6 eqid ⊢ I = I
7 eqid ⊢ Base I = Base I
8 6 7 rrxds ⊢ I ∈ V → f ∈ Base I , g ∈ Base I ⟼ ∑ ℝ fld x ∈ I f ⁡ x − g ⁡ x 2 = dist ⁡ I
9 2 8 eqtr4id ⊢ I ∈ V → D = f ∈ Base I , g ∈ Base I ⟼ ∑ ℝ fld x ∈ I f ⁡ x − g ⁡ x 2
10 6 7 rrxbase ⊢ I ∈ V → Base I = h ∈ ℝ I | finSupp 0 ⁡ h
11 1 10 eqtr4id ⊢ I ∈ V → X = Base I
12 11 sqxpeqd ⊢ I ∈ V → X × X = Base I × Base I
13 9 12 fneq12d ⊢ I ∈ V → D Fn X × X ↔ f ∈ Base I , g ∈ Base I ⟼ ∑ ℝ fld x ∈ I f ⁡ x − g ⁡ x 2 Fn Base I × Base I
14 5 13 mpbiri ⊢ I ∈ V → D Fn X × X
15 fnov ⊢ D Fn X × X ↔ D = f ∈ X , g ∈ X ⟼ f D g
16 14 15 sylib ⊢ I ∈ V → D = f ∈ X , g ∈ X ⟼ f D g
17 1 2 rrxmval ⊢ I ∈ V ∧ f ∈ X ∧ g ∈ X → f D g = ∑ k ∈ supp 0 ⁡ f ∪ supp 0 ⁡ g f ⁡ k − g ⁡ k 2
18 17 mpoeq3dva ⊢ I ∈ V → f ∈ X , g ∈ X ⟼ f D g = f ∈ X , g ∈ X ⟼ ∑ k ∈ supp 0 ⁡ f ∪ supp 0 ⁡ g f ⁡ k − g ⁡ k 2
19 16 18 eqtrd ⊢ I ∈ V → D = f ∈ X , g ∈ X ⟼ ∑ k ∈ supp 0 ⁡ f ∪ supp 0 ⁡ g f ⁡ k − g ⁡ k 2