Metamath Proof Explorer

Theorem ehl2eudis

Description: The Euclidean distance function in a real Euclidean space of dimension 2. (Contributed by AV, 16-Jan-2023)

Ref Expression
Hypotheses ehl2eudis.e 
|- E = ( EEhil ` 2 )
ehl2eudis.x 
|- X = ( RR ^m ( 0 ..^ 2 ) )
ehl2eudis.d 
|- D = ( dist ` E )
Assertion ehl2eudis 
|- D = ( f e. X , g e. X |-> ( sqrt ` ( ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) + ( ( ( f ` 1 ) - ( g ` 1 ) ) ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 ehl2eudis.e 
 |-  E = ( EEhil ` 2 )
2 ehl2eudis.x 
 |-  X = ( RR ^m ( 0 ..^ 2 ) )
3 ehl2eudis.d 
 |-  D = ( dist ` E )
4 2nn0 
 |-  2 e. NN0
5 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
6 5 eqcomi 
 |-  { 0 , 1 } = ( 0 ..^ 2 )
7 6 oveq2i 
 |-  ( RR ^m { 0 , 1 } ) = ( RR ^m ( 0 ..^ 2 ) )
8 2 7 eqtr4i 
 |-  X = ( RR ^m { 0 , 1 } )
9 6 1 8 3 ehleudis 
 |-  ( 2 e. NN0 -> D = ( f e. X , g e. X |-> ( sqrt ` sum_ k e. { 0 , 1 } ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
10 4 9 ax-mp 
 |-  D = ( f e. X , g e. X |-> ( sqrt ` sum_ k e. { 0 , 1 } ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )
11 fveq2 
 |-  ( k = 0 -> ( f ` k ) = ( f ` 0 ) )
12 fveq2 
 |-  ( k = 0 -> ( g ` k ) = ( g ` 0 ) )
13 11 12 oveq12d 
 |-  ( k = 0 -> ( ( f ` k ) - ( g ` k ) ) = ( ( f ` 0 ) - ( g ` 0 ) ) )
14 13 oveq1d 
 |-  ( k = 0 -> ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) = ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) )
15 fveq2 
 |-  ( k = 1 -> ( f ` k ) = ( f ` 1 ) )
16 fveq2 
 |-  ( k = 1 -> ( g ` k ) = ( g ` 1 ) )
17 15 16 oveq12d 
 |-  ( k = 1 -> ( ( f ` k ) - ( g ` k ) ) = ( ( f ` 1 ) - ( g ` 1 ) ) )
18 17 oveq1d 
 |-  ( k = 1 -> ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) = ( ( ( f ` 1 ) - ( g ` 1 ) ) ^ 2 ) )
19 8 eleq2i 
 |-  ( f e. X <-> f e. ( RR ^m { 0 , 1 } ) )
20 reex 
 |-  RR e. _V
21 prex 
 |-  { 0 , 1 } e. _V
22 20 21 elmap 
 |-  ( f e. ( RR ^m { 0 , 1 } ) <-> f : { 0 , 1 } --> RR )
23 19 22 bitri 
 |-  ( f e. X <-> f : { 0 , 1 } --> RR )
24 id 
 |-  ( f : { 0 , 1 } --> RR -> f : { 0 , 1 } --> RR )
25 0elpr01 
 |-  0 e. { 0 , 1 }
26 25 a1i 
 |-  ( f : { 0 , 1 } --> RR -> 0 e. { 0 , 1 } )
27 24 26 ffvelcdmd 
 |-  ( f : { 0 , 1 } --> RR -> ( f ` 0 ) e. RR )
28 23 27 sylbi 
 |-  ( f e. X -> ( f ` 0 ) e. RR )
29 28 adantr 
 |-  ( ( f e. X /\ g e. X ) -> ( f ` 0 ) e. RR )
30 8 eleq2i 
 |-  ( g e. X <-> g e. ( RR ^m { 0 , 1 } ) )
31 20 21 elmap 
 |-  ( g e. ( RR ^m { 0 , 1 } ) <-> g : { 0 , 1 } --> RR )
32 30 31 bitri 
 |-  ( g e. X <-> g : { 0 , 1 } --> RR )
33 id 
 |-  ( g : { 0 , 1 } --> RR -> g : { 0 , 1 } --> RR )
34 25 a1i 
 |-  ( g : { 0 , 1 } --> RR -> 0 e. { 0 , 1 } )
35 33 34 ffvelcdmd 
 |-  ( g : { 0 , 1 } --> RR -> ( g ` 0 ) e. RR )
36 32 35 sylbi 
 |-  ( g e. X -> ( g ` 0 ) e. RR )
37 36 adantl 
 |-  ( ( f e. X /\ g e. X ) -> ( g ` 0 ) e. RR )
38 29 37 resubcld 
 |-  ( ( f e. X /\ g e. X ) -> ( ( f ` 0 ) - ( g ` 0 ) ) e. RR )
39 38 resqcld 
 |-  ( ( f e. X /\ g e. X ) -> ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) e. RR )
40 39 recnd 
 |-  ( ( f e. X /\ g e. X ) -> ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) e. CC )
41 1elpr01 
 |-  1 e. { 0 , 1 }
42 41 a1i 
 |-  ( f : { 0 , 1 } --> RR -> 1 e. { 0 , 1 } )
43 24 42 ffvelcdmd 
 |-  ( f : { 0 , 1 } --> RR -> ( f ` 1 ) e. RR )
44 23 43 sylbi 
 |-  ( f e. X -> ( f ` 1 ) e. RR )
45 44 adantr 
 |-  ( ( f e. X /\ g e. X ) -> ( f ` 1 ) e. RR )
46 41 a1i 
 |-  ( g : { 0 , 1 } --> RR -> 1 e. { 0 , 1 } )
47 33 46 ffvelcdmd 
 |-  ( g : { 0 , 1 } --> RR -> ( g ` 1 ) e. RR )
48 32 47 sylbi 
 |-  ( g e. X -> ( g ` 1 ) e. RR )
49 48 adantl 
 |-  ( ( f e. X /\ g e. X ) -> ( g ` 1 ) e. RR )
50 45 49 resubcld 
 |-  ( ( f e. X /\ g e. X ) -> ( ( f ` 1 ) - ( g ` 1 ) ) e. RR )
51 50 resqcld 
 |-  ( ( f e. X /\ g e. X ) -> ( ( ( f ` 1 ) - ( g ` 1 ) ) ^ 2 ) e. RR )
52 51 recnd 
 |-  ( ( f e. X /\ g e. X ) -> ( ( ( f ` 1 ) - ( g ` 1 ) ) ^ 2 ) e. CC )
53 40 52 jca 
 |-  ( ( f e. X /\ g e. X ) -> ( ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) e. CC /\ ( ( ( f ` 1 ) - ( g ` 1 ) ) ^ 2 ) e. CC ) )
54 c0ex 
 |-  0 e. _V
55 1ex 
 |-  1 e. _V
56 54 55 pm3.2i 
 |-  ( 0 e. _V /\ 1 e. _V )
57 56 a1i 
 |-  ( ( f e. X /\ g e. X ) -> ( 0 e. _V /\ 1 e. _V ) )
58 0ne1 
 |-  0 =/= 1
59 58 a1i 
 |-  ( ( f e. X /\ g e. X ) -> 0 =/= 1 )
60 14 18 53 57 59 sumpr 
 |-  ( ( f e. X /\ g e. X ) -> sum_ k e. { 0 , 1 } ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) = ( ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) + ( ( ( f ` 1 ) - ( g ` 1 ) ) ^ 2 ) ) )
61 60 fveq2d 
 |-  ( ( f e. X /\ g e. X ) -> ( sqrt ` sum_ k e. { 0 , 1 } ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) = ( sqrt ` ( ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) + ( ( ( f ` 1 ) - ( g ` 1 ) ) ^ 2 ) ) ) )
62 61 mpoeq3ia 
 |-  ( f e. X , g e. X |-> ( sqrt ` sum_ k e. { 0 , 1 } ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) = ( f e. X , g e. X |-> ( sqrt ` ( ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) + ( ( ( f ` 1 ) - ( g ` 1 ) ) ^ 2 ) ) ) )
63 10 62 eqtri 
 |-  D = ( f e. X , g e. X |-> ( sqrt ` ( ( ( ( f ` 0 ) - ( g ` 0 ) ) ^ 2 ) + ( ( ( f ` 1 ) - ( g ` 1 ) ) ^ 2 ) ) ) )