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 ⊢ 𝐸 = ( 𝔼hil ‘ 2 )
ehl2eudisval0.x ⊢ 𝑋 = ( ℝ ↑m ( 0 ..^ 2 ) )
ehl2eudisval0.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
ehl2eudisval0.0 ⊢ 0 = ( ( 0 ..^ 2 ) × { 0 } )
Assertion ehl2eudisval0 ( 𝐹 ∈ 𝑋 → ( 𝐹 𝐷 0 ) = ( √ ‘ ( ( ( 𝐹 ‘ 0 ) ↑ 2 ) + ( ( 𝐹 ‘ 1 ) ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 ehl2eudisval0.e ⊢ 𝐸 = ( 𝔼hil ‘ 2 )
2 ehl2eudisval0.x ⊢ 𝑋 = ( ℝ ↑m ( 0 ..^ 2 ) )
3 ehl2eudisval0.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
4 ehl2eudisval0.0 ⊢ 0 = ( ( 0 ..^ 2 ) × { 0 } )
5 ovex ⊢ ( 0 ..^ 2 ) ∈ V
6 4 2 rrx0el ⊢ ( ( 0 ..^ 2 ) ∈ V → 0 ∈ 𝑋 )
7 5 6 mp1i ⊢ ( 𝐹 ∈ 𝑋 → 0 ∈ 𝑋 )
8 1 2 3 ehl2eudisval ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 0 ∈ 𝑋 ) → ( 𝐹 𝐷 0 ) = ( √ ‘ ( ( ( ( 𝐹 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) ) )
9 7 8 mpdan ⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 𝐷 0 ) = ( √ ‘ ( ( ( ( 𝐹 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) ) )
10 fzo0to2pr ⊢ ( 0 ..^ 2 ) = { 0 , 1 }
11 10 xpeq1i ⊢ ( ( 0 ..^ 2 ) × { 0 } ) = ( { 0 , 1 } × { 0 } )
12 c0ex ⊢ 0 ∈ V
13 1ex ⊢ 1 ∈ V
14 xpprsng ⊢ ( ( 0 ∈ V ∧ 1 ∈ V ∧ 0 ∈ V ) → ( { 0 , 1 } × { 0 } ) = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } )
15 12 13 12 14 mp3an ⊢ ( { 0 , 1 } × { 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 ⊢ ( 𝐹 ∈ 𝑋 → ( 0 ‘ 0 ) = 0 )
23 22 oveq2d ⊢ ( 𝐹 ∈ 𝑋 → ( ( 𝐹 ‘ 0 ) − ( 0 ‘ 0 ) ) = ( ( 𝐹 ‘ 0 ) − 0 ) )
24 eqid ⊢ ( 0 ..^ 2 ) = ( 0 ..^ 2 )
25 24 2 rrx2pxel ⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 ‘ 0 ) ∈ ℝ )
26 25 recnd ⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 ‘ 0 ) ∈ ℂ )
27 26 subid1d ⊢ ( 𝐹 ∈ 𝑋 → ( ( 𝐹 ‘ 0 ) − 0 ) = ( 𝐹 ‘ 0 ) )
28 23 27 eqtrd ⊢ ( 𝐹 ∈ 𝑋 → ( ( 𝐹 ‘ 0 ) − ( 0 ‘ 0 ) ) = ( 𝐹 ‘ 0 ) )
29 28 oveq1d ⊢ ( 𝐹 ∈ 𝑋 → ( ( ( 𝐹 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) = ( ( 𝐹 ‘ 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 ⊢ ( 𝐹 ∈ 𝑋 → ( { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ‘ 1 ) = 0 )
33 30 32 eqtrid ⊢ ( 𝐹 ∈ 𝑋 → ( 0 ‘ 1 ) = 0 )
34 33 oveq2d ⊢ ( 𝐹 ∈ 𝑋 → ( ( 𝐹 ‘ 1 ) − ( 0 ‘ 1 ) ) = ( ( 𝐹 ‘ 1 ) − 0 ) )
35 24 2 rrx2pyel ⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 ‘ 1 ) ∈ ℝ )
36 35 recnd ⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 ‘ 1 ) ∈ ℂ )
37 36 subid1d ⊢ ( 𝐹 ∈ 𝑋 → ( ( 𝐹 ‘ 1 ) − 0 ) = ( 𝐹 ‘ 1 ) )
38 34 37 eqtrd ⊢ ( 𝐹 ∈ 𝑋 → ( ( 𝐹 ‘ 1 ) − ( 0 ‘ 1 ) ) = ( 𝐹 ‘ 1 ) )
39 38 oveq1d ⊢ ( 𝐹 ∈ 𝑋 → ( ( ( 𝐹 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) = ( ( 𝐹 ‘ 1 ) ↑ 2 ) )
40 29 39 oveq12d ⊢ ( 𝐹 ∈ 𝑋 → ( ( ( ( 𝐹 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( ( ( 𝐹 ‘ 0 ) ↑ 2 ) + ( ( 𝐹 ‘ 1 ) ↑ 2 ) ) )
41 40 fveq2d ⊢ ( 𝐹 ∈ 𝑋 → ( √ ‘ ( ( ( ( 𝐹 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) ) = ( √ ‘ ( ( ( 𝐹 ‘ 0 ) ↑ 2 ) + ( ( 𝐹 ‘ 1 ) ↑ 2 ) ) ) )
42 9 41 eqtrd ⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 𝐷 0 ) = ( √ ‘ ( ( ( 𝐹 ‘ 0 ) ↑ 2 ) + ( ( 𝐹 ‘ 1 ) ↑ 2 ) ) ) )