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

Metamath Proof Explorer

Theorem ehl1eudisval

Description: The value of 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 ehl1eudisval ⊢ F ∈ X ∧ G ∈ X → F D G = 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 fveq1 ⊢ x = F → x ⁡ 1 = F ⁡ 1
5 4 fvoveq1d ⊢ x = F → x ⁡ 1 − y ⁡ 1 = F ⁡ 1 − y ⁡ 1
6 fveq1 ⊢ y = G → y ⁡ 1 = G ⁡ 1
7 6 oveq2d ⊢ y = G → F ⁡ 1 − y ⁡ 1 = F ⁡ 1 − G ⁡ 1
8 7 fveq2d ⊢ y = G → F ⁡ 1 − y ⁡ 1 = F ⁡ 1 − G ⁡ 1
9 1 2 3 ehl1eudis ⊢ D = x ∈ X , y ∈ X ⟼ x ⁡ 1 − y ⁡ 1
10 fvex ⊢ F ⁡ 1 − G ⁡ 1 ∈ V
11 5 8 9 10 ovmpo ⊢ F ∈ X ∧ G ∈ X → F D G = F ⁡ 1 − G ⁡ 1