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 = ( EEhil ` 1 )
ehl1eudis.x 
|- X = ( RR ^m { 1 } )
ehl1eudis.d 
|- D = ( dist ` E )
Assertion ehl1eudisval 
|- ( ( F e. X /\ G e. X ) -> ( F D G ) = ( abs ` ( ( F ` 1 ) - ( G ` 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 ehl1eudis.e 
 |-  E = ( EEhil ` 1 )
2 ehl1eudis.x 
 |-  X = ( RR ^m { 1 } )
3 ehl1eudis.d 
 |-  D = ( dist ` E )
4 fveq1 
 |-  ( x = F -> ( x ` 1 ) = ( F ` 1 ) )
5 4 fvoveq1d 
 |-  ( x = F -> ( abs ` ( ( x ` 1 ) - ( y ` 1 ) ) ) = ( abs ` ( ( 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 -> ( abs ` ( ( F ` 1 ) - ( y ` 1 ) ) ) = ( abs ` ( ( F ` 1 ) - ( G ` 1 ) ) ) )
9 1 2 3 ehl1eudis 
 |-  D = ( x e. X , y e. X |-> ( abs ` ( ( x ` 1 ) - ( y ` 1 ) ) ) )
10 fvex 
 |-  ( abs ` ( ( F ` 1 ) - ( G ` 1 ) ) ) e. _V
11 5 8 9 10 ovmpo 
 |-  ( ( F e. X /\ G e. X ) -> ( F D G ) = ( abs ` ( ( F ` 1 ) - ( G ` 1 ) ) ) )