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