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 ⊢ 𝐸 = ( 𝔼hil ‘ 1 )
ehl1eudis.x ⊢ 𝑋 = ( ℝ ↑m { 1 } )
ehl1eudis.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
Assertion ehl1eudisval ( ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) = ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 ehl1eudis.e ⊢ 𝐸 = ( 𝔼hil ‘ 1 )
2 ehl1eudis.x ⊢ 𝑋 = ( ℝ ↑m { 1 } )
3 ehl1eudis.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
4 fveq1 ⊢ ( 𝑥 = 𝐹 → ( 𝑥 ‘ 1 ) = ( 𝐹 ‘ 1 ) )
5 4 fvoveq1d ⊢ ( 𝑥 = 𝐹 → ( abs ‘ ( ( 𝑥 ‘ 1 ) − ( 𝑦 ‘ 1 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝑦 ‘ 1 ) ) ) )
6 fveq1 ⊢ ( 𝑦 = 𝐺 → ( 𝑦 ‘ 1 ) = ( 𝐺 ‘ 1 ) )
7 6 oveq2d ⊢ ( 𝑦 = 𝐺 → ( ( 𝐹 ‘ 1 ) − ( 𝑦 ‘ 1 ) ) = ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) )
8 7 fveq2d ⊢ ( 𝑦 = 𝐺 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝑦 ‘ 1 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ) )
9 1 2 3 ehl1eudis ⊢ 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( abs ‘ ( ( 𝑥 ‘ 1 ) − ( 𝑦 ‘ 1 ) ) ) )
10 fvex ⊢ ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ) ∈ V
11 5 8 9 10 ovmpo ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) = ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ) )