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 { 1 , 2 } )
ehl2eudisval0.d 
|- D = ( dist ` E )
ehl2eudisval0.0 
|- .0. = ( { 1 , 2 } X. { 0 } )
Assertion ehl2eudisval0 
|- ( F e. X -> ( F D .0. ) = ( sqrt ` ( ( ( F ` 1 ) ^ 2 ) + ( ( F ` 2 ) ^ 2 ) ) ) )

Proof

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