Metamath Proof Explorer

Theorem ehl2eudis

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

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

Proof

Step Hyp Ref Expression
1 ehl2eudis.e ⊢ E = 𝔼 hil ⁡ 2
2 ehl2eudis.x ⊢ X = ℝ 0 ..^ 2
3 ehl2eudis.d ⊢ D = dist ⁡ E
4 2nn0 ⊢ 2 ∈ ℕ 0
5 fzo0to2pr ⊢ 0 ..^ 2 = 0 1
6 5 eqcomi ⊢ 0 1 = 0 ..^ 2
7 6 oveq2i ⊢ ℝ 0 1 = ℝ 0 ..^ 2
8 2 7 eqtr4i ⊢ X = ℝ 0 1
9 6 1 8 3 ehleudis ⊢ 2 ∈ ℕ 0 → D = f ∈ X , g ∈ X ⟼ ∑ k ∈ 0 1 f ⁡ k − g ⁡ k 2
10 4 9 ax-mp ⊢ D = f ∈ X , g ∈ X ⟼ ∑ k ∈ 0 1 f ⁡ k − g ⁡ k 2
11 fveq2 ⊢ k = 0 → f ⁡ k = f ⁡ 0
12 fveq2 ⊢ k = 0 → g ⁡ k = g ⁡ 0
13 11 12 oveq12d ⊢ k = 0 → f ⁡ k − g ⁡ k = f ⁡ 0 − g ⁡ 0
14 13 oveq1d ⊢ k = 0 → f ⁡ k − g ⁡ k 2 = f ⁡ 0 − g ⁡ 0 2
15 fveq2 ⊢ k = 1 → f ⁡ k = f ⁡ 1
16 fveq2 ⊢ k = 1 → g ⁡ k = g ⁡ 1
17 15 16 oveq12d ⊢ k = 1 → f ⁡ k − g ⁡ k = f ⁡ 1 − g ⁡ 1
18 17 oveq1d ⊢ k = 1 → f ⁡ k − g ⁡ k 2 = f ⁡ 1 − g ⁡ 1 2
19 8 eleq2i ⊢ f ∈ X ↔ f ∈ ℝ 0 1
20 reex ⊢ ℝ ∈ V
21 prex ⊢ 0 1 ∈ V
22 20 21 elmap ⊢ f ∈ ℝ 0 1 ↔ f : 0 1 ⟶ ℝ
23 19 22 bitri ⊢ f ∈ X ↔ f : 0 1 ⟶ ℝ
24 id ⊢ f : 0 1 ⟶ ℝ → f : 0 1 ⟶ ℝ
25 0elpr01 ⊢ 0 ∈ 0 1
26 25 a1i ⊢ f : 0 1 ⟶ ℝ → 0 ∈ 0 1
27 24 26 ffvelcdmd ⊢ f : 0 1 ⟶ ℝ → f ⁡ 0 ∈ ℝ
28 23 27 sylbi ⊢ f ∈ X → f ⁡ 0 ∈ ℝ
29 28 adantr ⊢ f ∈ X ∧ g ∈ X → f ⁡ 0 ∈ ℝ
30 8 eleq2i ⊢ g ∈ X ↔ g ∈ ℝ 0 1
31 20 21 elmap ⊢ g ∈ ℝ 0 1 ↔ g : 0 1 ⟶ ℝ
32 30 31 bitri ⊢ g ∈ X ↔ g : 0 1 ⟶ ℝ
33 id ⊢ g : 0 1 ⟶ ℝ → g : 0 1 ⟶ ℝ
34 25 a1i ⊢ g : 0 1 ⟶ ℝ → 0 ∈ 0 1
35 33 34 ffvelcdmd ⊢ g : 0 1 ⟶ ℝ → g ⁡ 0 ∈ ℝ
36 32 35 sylbi ⊢ g ∈ X → g ⁡ 0 ∈ ℝ
37 36 adantl ⊢ f ∈ X ∧ g ∈ X → g ⁡ 0 ∈ ℝ
38 29 37 resubcld ⊢ f ∈ X ∧ g ∈ X → f ⁡ 0 − g ⁡ 0 ∈ ℝ
39 38 resqcld ⊢ f ∈ X ∧ g ∈ X → f ⁡ 0 − g ⁡ 0 2 ∈ ℝ
40 39 recnd ⊢ f ∈ X ∧ g ∈ X → f ⁡ 0 − g ⁡ 0 2 ∈ ℂ
41 1elpr01 ⊢ 1 ∈ 0 1
42 41 a1i ⊢ f : 0 1 ⟶ ℝ → 1 ∈ 0 1
43 24 42 ffvelcdmd ⊢ f : 0 1 ⟶ ℝ → f ⁡ 1 ∈ ℝ
44 23 43 sylbi ⊢ f ∈ X → f ⁡ 1 ∈ ℝ
45 44 adantr ⊢ f ∈ X ∧ g ∈ X → f ⁡ 1 ∈ ℝ
46 41 a1i ⊢ g : 0 1 ⟶ ℝ → 1 ∈ 0 1
47 33 46 ffvelcdmd ⊢ g : 0 1 ⟶ ℝ → g ⁡ 1 ∈ ℝ
48 32 47 sylbi ⊢ g ∈ X → g ⁡ 1 ∈ ℝ
49 48 adantl ⊢ f ∈ X ∧ g ∈ X → g ⁡ 1 ∈ ℝ
50 45 49 resubcld ⊢ f ∈ X ∧ g ∈ X → f ⁡ 1 − g ⁡ 1 ∈ ℝ
51 50 resqcld ⊢ f ∈ X ∧ g ∈ X → f ⁡ 1 − g ⁡ 1 2 ∈ ℝ
52 51 recnd ⊢ f ∈ X ∧ g ∈ X → f ⁡ 1 − g ⁡ 1 2 ∈ ℂ
53 40 52 jca ⊢ f ∈ X ∧ g ∈ X → f ⁡ 0 − g ⁡ 0 2 ∈ ℂ ∧ f ⁡ 1 − g ⁡ 1 2 ∈ ℂ
54 c0ex ⊢ 0 ∈ V
55 1ex ⊢ 1 ∈ V
56 54 55 pm3.2i ⊢ 0 ∈ V ∧ 1 ∈ V
57 56 a1i ⊢ f ∈ X ∧ g ∈ X → 0 ∈ V ∧ 1 ∈ V
58 0ne1 ⊢ 0 ≠ 1
59 58 a1i ⊢ f ∈ X ∧ g ∈ X → 0 ≠ 1
60 14 18 53 57 59 sumpr ⊢ f ∈ X ∧ g ∈ X → ∑ k ∈ 0 1 f ⁡ k − g ⁡ k 2 = f ⁡ 0 − g ⁡ 0 2 + f ⁡ 1 − g ⁡ 1 2
61 60 fveq2d ⊢ f ∈ X ∧ g ∈ X → ∑ k ∈ 0 1 f ⁡ k − g ⁡ k 2 = f ⁡ 0 − g ⁡ 0 2 + f ⁡ 1 − g ⁡ 1 2
62 61 mpoeq3ia ⊢ f ∈ X , g ∈ X ⟼ ∑ k ∈ 0 1 f ⁡ k − g ⁡ k 2 = f ∈ X , g ∈ X ⟼ f ⁡ 0 − g ⁡ 0 2 + f ⁡ 1 − g ⁡ 1 2
63 10 62 eqtri ⊢ D = f ∈ X , g ∈ X ⟼ f ⁡ 0 − g ⁡ 0 2 + f ⁡ 1 − g ⁡ 1 2