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