Metamath Proof Explorer

Theorem ehl2eudisval0

Description: The Euclidean distance of a point to the origin in a real Euclidean space of dimension 2. (Contributed by AV, 26-Feb-2023)

Ref Expression
Hypotheses ehl2eudisval0.e 
|- E = ( EEhil ` 2 )
ehl2eudisval0.x 
|- X = ( RR ^m ( 0 ..^ 2 ) )
ehl2eudisval0.d 
|- D = ( dist ` E )
ehl2eudisval0.0 
|- .0. = <" 0 0 ">
Assertion ehl2eudisval0 
|- ( F e. X -> ( F D .0. ) = ( sqrt ` ( ( ( F ` 0 ) ^ 2 ) + ( ( F ` 1 ) ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 ehl2eudisval0.e 
 |-  E = ( EEhil ` 2 )
2 ehl2eudisval0.x 
 |-  X = ( RR ^m ( 0 ..^ 2 ) )
3 ehl2eudisval0.d 
 |-  D = ( dist ` E )
4 ehl2eudisval0.0 
 |-  .0. = <" 0 0 ">
5 ovex 
 |-  ( 0 ..^ 2 ) e. _V
6 c0ex 
 |-  0 e. _V
7 1ex 
 |-  1 e. _V
8 xpprsng 
 |-  ( ( 0 e. _V /\ 1 e. _V /\ 0 e. _V ) -> ( { 0 , 1 } X. { 0 } ) = { <. 0 , 0 >. , <. 1 , 0 >. } )
9 6 7 6 8 mp3an 
 |-  ( { 0 , 1 } X. { 0 } ) = { <. 0 , 0 >. , <. 1 , 0 >. }
10 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
11 10 xpeq1i 
 |-  ( ( 0 ..^ 2 ) X. { 0 } ) = ( { 0 , 1 } X. { 0 } )
12 s2prop 
 |-  ( ( 0 e. _V /\ 0 e. _V ) -> <" 0 0 "> = { <. 0 , 0 >. , <. 1 , 0 >. } )
13 6 6 12 mp2an 
 |-  <" 0 0 "> = { <. 0 , 0 >. , <. 1 , 0 >. }
14 9 11 13 3eqtr4ri 
 |-  <" 0 0 "> = ( ( 0 ..^ 2 ) X. { 0 } )
15 4 14 eqtri 
 |-  .0. = ( ( 0 ..^ 2 ) X. { 0 } )
16 15 2 rrx0el 
 |-  ( ( 0 ..^ 2 ) e. _V -> .0. e. X )
17 5 16 mp1i 
 |-  ( F e. X -> .0. e. X )
18 1 2 3 ehl2eudisval 
 |-  ( ( F e. X /\ .0. e. X ) -> ( F D .0. ) = ( sqrt ` ( ( ( ( F ` 0 ) - ( .0. ` 0 ) ) ^ 2 ) + ( ( ( F ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) ) ) )
19 17 18 mpdan 
 |-  ( F e. X -> ( F D .0. ) = ( sqrt ` ( ( ( ( F ` 0 ) - ( .0. ` 0 ) ) ^ 2 ) + ( ( ( F ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) ) ) )
20 4 13 eqtri 
 |-  .0. = { <. 0 , 0 >. , <. 1 , 0 >. }
21 20 fveq1i 
 |-  ( .0. ` 0 ) = ( { <. 0 , 0 >. , <. 1 , 0 >. } ` 0 )
22 0ne1 
 |-  0 =/= 1
23 6 6 fvpr1 
 |-  ( 0 =/= 1 -> ( { <. 0 , 0 >. , <. 1 , 0 >. } ` 0 ) = 0 )
24 22 23 ax-mp 
 |-  ( { <. 0 , 0 >. , <. 1 , 0 >. } ` 0 ) = 0
25 21 24 eqtri 
 |-  ( .0. ` 0 ) = 0
26 25 a1i 
 |-  ( F e. X -> ( .0. ` 0 ) = 0 )
27 26 oveq2d 
 |-  ( F e. X -> ( ( F ` 0 ) - ( .0. ` 0 ) ) = ( ( F ` 0 ) - 0 ) )
28 eqid 
 |-  ( 0 ..^ 2 ) = ( 0 ..^ 2 )
29 28 2 rrx2pxel 
 |-  ( F e. X -> ( F ` 0 ) e. RR )
30 29 recnd 
 |-  ( F e. X -> ( F ` 0 ) e. CC )
31 30 subid1d 
 |-  ( F e. X -> ( ( F ` 0 ) - 0 ) = ( F ` 0 ) )
32 27 31 eqtrd 
 |-  ( F e. X -> ( ( F ` 0 ) - ( .0. ` 0 ) ) = ( F ` 0 ) )
33 32 oveq1d 
 |-  ( F e. X -> ( ( ( F ` 0 ) - ( .0. ` 0 ) ) ^ 2 ) = ( ( F ` 0 ) ^ 2 ) )
34 20 fveq1i 
 |-  ( .0. ` 1 ) = ( { <. 0 , 0 >. , <. 1 , 0 >. } ` 1 )
35 7 6 fvpr2 
 |-  ( 0 =/= 1 -> ( { <. 0 , 0 >. , <. 1 , 0 >. } ` 1 ) = 0 )
36 22 35 mp1i 
 |-  ( F e. X -> ( { <. 0 , 0 >. , <. 1 , 0 >. } ` 1 ) = 0 )
37 34 36 eqtrid 
 |-  ( F e. X -> ( .0. ` 1 ) = 0 )
38 37 oveq2d 
 |-  ( F e. X -> ( ( F ` 1 ) - ( .0. ` 1 ) ) = ( ( F ` 1 ) - 0 ) )
39 28 2 rrx2pyel 
 |-  ( F e. X -> ( F ` 1 ) e. RR )
40 39 recnd 
 |-  ( F e. X -> ( F ` 1 ) e. CC )
41 40 subid1d 
 |-  ( F e. X -> ( ( F ` 1 ) - 0 ) = ( F ` 1 ) )
42 38 41 eqtrd 
 |-  ( F e. X -> ( ( F ` 1 ) - ( .0. ` 1 ) ) = ( F ` 1 ) )
43 42 oveq1d 
 |-  ( F e. X -> ( ( ( F ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) = ( ( F ` 1 ) ^ 2 ) )
44 33 43 oveq12d 
 |-  ( F e. X -> ( ( ( ( F ` 0 ) - ( .0. ` 0 ) ) ^ 2 ) + ( ( ( F ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) ) = ( ( ( F ` 0 ) ^ 2 ) + ( ( F ` 1 ) ^ 2 ) ) )
45 44 fveq2d 
 |-  ( F e. X -> ( sqrt ` ( ( ( ( F ` 0 ) - ( .0. ` 0 ) ) ^ 2 ) + ( ( ( F ` 1 ) - ( .0. ` 1 ) ) ^ 2 ) ) ) = ( sqrt ` ( ( ( F ` 0 ) ^ 2 ) + ( ( F ` 1 ) ^ 2 ) ) ) )
46 19 45 eqtrd 
 |-  ( F e. X -> ( F D .0. ) = ( sqrt ` ( ( ( F ` 0 ) ^ 2 ) + ( ( F ` 1 ) ^ 2 ) ) ) )