Metamath Proof Explorer

Theorem ehl1eudis

Description: The Euclidean distance function in a real Euclidean space of dimension 1. (Contributed by AV, 16-Jan-2023)

Ref Expression
Hypotheses ehl1eudis.e ⊢ E = 𝔼 hil ⁡ 1
ehl1eudis.x ⊢ X = ℝ 1
ehl1eudis.d ⊢ D = dist ⁡ E
Assertion ehl1eudis ⊢ D = f ∈ X , g ∈ X ⟼ f ⁡ 1 − g ⁡ 1

Proof

Step Hyp Ref Expression
1 ehl1eudis.e ⊢ E = 𝔼 hil ⁡ 1
2 ehl1eudis.x ⊢ X = ℝ 1
3 ehl1eudis.d ⊢ D = dist ⁡ E
4 1nn0 ⊢ 1 ∈ ℕ 0
5 1z ⊢ 1 ∈ ℤ
6 fzsn ⊢ 1 ∈ ℤ → 1 … 1 = 1
7 5 6 ax-mp ⊢ 1 … 1 = 1
8 7 eqcomi ⊢ 1 = 1 … 1
9 8 1 2 3 ehleudis ⊢ 1 ∈ ℕ 0 → D = f ∈ X , g ∈ X ⟼ ∑ k ∈ 1 f ⁡ k − g ⁡ k 2
10 4 9 ax-mp ⊢ D = f ∈ X , g ∈ X ⟼ ∑ k ∈ 1 f ⁡ k − g ⁡ k 2
11 2 eleq2i ⊢ f ∈ X ↔ f ∈ ℝ 1
12 reex ⊢ ℝ ∈ V
13 snex ⊢ 1 ∈ V
14 12 13 elmap ⊢ f ∈ ℝ 1 ↔ f : 1 ⟶ ℝ
15 11 14 bitri ⊢ f ∈ X ↔ f : 1 ⟶ ℝ
16 id ⊢ f : 1 ⟶ ℝ → f : 1 ⟶ ℝ
17 1ex ⊢ 1 ∈ V
18 17 snid ⊢ 1 ∈ 1
19 18 a1i ⊢ f : 1 ⟶ ℝ → 1 ∈ 1
20 16 19 ffvelcdmd ⊢ f : 1 ⟶ ℝ → f ⁡ 1 ∈ ℝ
21 15 20 sylbi ⊢ f ∈ X → f ⁡ 1 ∈ ℝ
22 21 adantr ⊢ f ∈ X ∧ g ∈ X → f ⁡ 1 ∈ ℝ
23 2 eleq2i ⊢ g ∈ X ↔ g ∈ ℝ 1
24 12 13 elmap ⊢ g ∈ ℝ 1 ↔ g : 1 ⟶ ℝ
25 23 24 bitri ⊢ g ∈ X ↔ g : 1 ⟶ ℝ
26 id ⊢ g : 1 ⟶ ℝ → g : 1 ⟶ ℝ
27 18 a1i ⊢ g : 1 ⟶ ℝ → 1 ∈ 1
28 26 27 ffvelcdmd ⊢ g : 1 ⟶ ℝ → g ⁡ 1 ∈ ℝ
29 25 28 sylbi ⊢ g ∈ X → g ⁡ 1 ∈ ℝ
30 29 adantl ⊢ f ∈ X ∧ g ∈ X → g ⁡ 1 ∈ ℝ
31 22 30 resubcld ⊢ f ∈ X ∧ g ∈ X → f ⁡ 1 − g ⁡ 1 ∈ ℝ
32 31 resqcld ⊢ f ∈ X ∧ g ∈ X → f ⁡ 1 − g ⁡ 1 2 ∈ ℝ
33 32 recnd ⊢ f ∈ X ∧ g ∈ X → f ⁡ 1 − g ⁡ 1 2 ∈ ℂ
34 fveq2 ⊢ k = 1 → f ⁡ k = f ⁡ 1
35 fveq2 ⊢ k = 1 → g ⁡ k = g ⁡ 1
36 34 35 oveq12d ⊢ k = 1 → f ⁡ k − g ⁡ k = f ⁡ 1 − g ⁡ 1
37 36 oveq1d ⊢ k = 1 → f ⁡ k − g ⁡ k 2 = f ⁡ 1 − g ⁡ 1 2
38 37 sumsn ⊢ 1 ∈ ℤ ∧ f ⁡ 1 − g ⁡ 1 2 ∈ ℂ → ∑ k ∈ 1 f ⁡ k − g ⁡ k 2 = f ⁡ 1 − g ⁡ 1 2
39 5 33 38 sylancr ⊢ f ∈ X ∧ g ∈ X → ∑ k ∈ 1 f ⁡ k − g ⁡ k 2 = f ⁡ 1 − g ⁡ 1 2
40 39 fveq2d ⊢ f ∈ X ∧ g ∈ X → ∑ k ∈ 1 f ⁡ k − g ⁡ k 2 = f ⁡ 1 − g ⁡ 1 2
41 31 absred ⊢ f ∈ X ∧ g ∈ X → f ⁡ 1 − g ⁡ 1 = f ⁡ 1 − g ⁡ 1 2
42 40 41 eqtr4d ⊢ f ∈ X ∧ g ∈ X → ∑ k ∈ 1 f ⁡ k − g ⁡ k 2 = f ⁡ 1 − g ⁡ 1
43 42 mpoeq3ia ⊢ f ∈ X , g ∈ X ⟼ ∑ k ∈ 1 f ⁡ k − g ⁡ k 2 = f ∈ X , g ∈ X ⟼ f ⁡ 1 − g ⁡ 1
44 10 43 eqtri ⊢ D = f ∈ X , g ∈ X ⟼ f ⁡ 1 − g ⁡ 1