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 = ( EEhil ` 1 )
ehl1eudis.x 
|- X = ( RR ^m { 0 } )
ehl1eudis.d 
|- D = ( dist ` E )
Assertion ehl1eudis 
|- D = ( f e. X , g e. X |-> ( abs ` ( ( f ` 0 ) - ( g ` 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 ehl1eudis.e 
 |-  E = ( EEhil ` 1 )
2 ehl1eudis.x 
 |-  X = ( RR ^m { 0 } )
3 ehl1eudis.d 
 |-  D = ( dist ` E )
4 1nn0 
 |-  1 e. NN0
5 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
6 5 eqcomi 
 |-  { 0 } = ( 0 ..^ 1 )
7 6 1 2 3 ehleudis 
 |-  ( 1 e. NN0 -> D = ( f e. X , g e. X |-> ( sqrt ` sum_ k e. { 0 } ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
8 4 7 ax-mp 
 |-  D = ( f e. X , g e. X |-> ( sqrt ` sum_ k e. { 0 } ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )
9 0z 
 |-  0 e. ZZ
10 2 eleq2i 
 |-  ( f e. X <-> f e. ( RR ^m { 0 } ) )
11 reex 
 |-  RR e. _V
12 snex 
 |-  { 0 } e. _V
13 11 12 elmap 
 |-  ( f e. ( RR ^m { 0 } ) <-> f : { 0 } --> RR )
14 10 13 bitri 
 |-  ( f e. X <-> f : { 0 } --> RR )
15 id 
 |-  ( f : { 0 } --> RR -> f : { 0 } --> RR )
16 c0ex 
 |-  0 e. _V
17 16 snid 
 |-  0 e. { 0 }
18 17 a1i 
 |-  ( f : { 0 } --> RR -> 0 e. { 0 } )
19 15 18 ffvelcdmd 
 |-  ( f : { 0 } --> RR -> ( f ` 0 ) e. RR )
20 14 19 sylbi 
 |-  ( f e. X -> ( f ` 0 ) e. RR )
21 20 adantr 
 |-  ( ( f e. X /\ g e. X ) -> ( f ` 0 ) e. RR )
22 2 eleq2i 
 |-  ( g e. X <-> g e. ( RR ^m { 0 } ) )
23 11 12 elmap 
 |-  ( g e. ( RR ^m { 0 } ) <-> g : { 0 } --> RR )
24 22 23 bitri 
 |-  ( g e. X <-> g : { 0 } --> RR )
25 id 
 |-  ( g : { 0 } --> RR -> g : { 0 } --> RR )
26 17 a1i 
 |-  ( g : { 0 } --> RR -> 0 e. { 0 } )
27 25 26 ffvelcdmd 
 |-  ( g : { 0 } --> RR -> ( g ` 0 ) e. RR )
28 24 27 sylbi 
 |-  ( g e. X -> ( g ` 0 ) e. RR )
29 28 adantl 
 |-  ( ( f e. X /\ g e. X ) -> ( g ` 0 ) e. RR )
30 21 29 resubcld 
 |-  ( ( f e. X /\ g e. X ) -> ( ( f ` 0 ) - ( g ` 0 ) ) e. RR )
31 30 resqcld 
 |-  ( ( f e. X /\ g e. X ) -> ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) e. RR )
32 31 recnd 
 |-  ( ( f e. X /\ g e. X ) -> ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) e. CC )
33 fveq2 
 |-  ( k = 0 -> ( f ` k ) = ( f ` 0 ) )
34 fveq2 
 |-  ( k = 0 -> ( g ` k ) = ( g ` 0 ) )
35 33 34 oveq12d 
 |-  ( k = 0 -> ( ( f ` k ) - ( g ` k ) ) = ( ( f ` 0 ) - ( g ` 0 ) ) )
36 35 oveq1d 
 |-  ( k = 0 -> ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) = ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) )
37 36 sumsn 
 |-  ( ( 0 e. ZZ /\ ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) e. CC ) -> sum_ k e. { 0 } ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) = ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) )
38 9 32 37 sylancr 
 |-  ( ( f e. X /\ g e. X ) -> sum_ k e. { 0 } ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) = ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) )
39 38 fveq2d 
 |-  ( ( f e. X /\ g e. X ) -> ( sqrt ` sum_ k e. { 0 } ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) = ( sqrt ` ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) ) )
40 30 absred 
 |-  ( ( f e. X /\ g e. X ) -> ( abs ` ( ( f ` 0 ) - ( g ` 0 ) ) ) = ( sqrt ` ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) ) )
41 39 40 eqtr4d 
 |-  ( ( f e. X /\ g e. X ) -> ( sqrt ` sum_ k e. { 0 } ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) = ( abs ` ( ( f ` 0 ) - ( g ` 0 ) ) ) )
42 41 mpoeq3ia 
 |-  ( f e. X , g e. X |-> ( sqrt ` sum_ k e. { 0 } ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) = ( f e. X , g e. X |-> ( abs ` ( ( f ` 0 ) - ( g ` 0 ) ) ) )
43 8 42 eqtri 
 |-  D = ( f e. X , g e. X |-> ( abs ` ( ( f ` 0 ) - ( g ` 0 ) ) ) )