Metamath Proof Explorer

Theorem ehl2eudisval

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

Ref Expression
Hypotheses ehl2eudis.e ⊢ 𝐸 = ( 𝔼hil ‘ 2 )
ehl2eudis.x ⊢ 𝑋 = ( ℝ ↑m { 1 , 2 } )
ehl2eudis.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
Assertion ehl2eudisval ( ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) = ( √ ‘ ( ( ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 2 ) − ( 𝐺 ‘ 2 ) ) ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 ehl2eudis.e ⊢ 𝐸 = ( 𝔼hil ‘ 2 )
2 ehl2eudis.x ⊢ 𝑋 = ( ℝ ↑m { 1 , 2 } )
3 ehl2eudis.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
4 1 2 3 ehl2eudis ⊢ 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ ( ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑓 ‘ 2 ) − ( 𝑔 ‘ 2 ) ) ↑ 2 ) ) ) )
5 4 oveqi ⊢ ( 𝐹 𝐷 𝐺 ) = ( 𝐹 ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ ( ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑓 ‘ 2 ) − ( 𝑔 ‘ 2 ) ) ↑ 2 ) ) ) ) 𝐺 )
6 eqidd ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ ( ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑓 ‘ 2 ) − ( 𝑔 ‘ 2 ) ) ↑ 2 ) ) ) ) = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ ( ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑓 ‘ 2 ) − ( 𝑔 ‘ 2 ) ) ↑ 2 ) ) ) ) )
7 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 1 ) )
8 fveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 1 ) = ( 𝐺 ‘ 1 ) )
9 7 8 oveqan12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) = ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) )
10 9 oveq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ↑ 2 ) )
11 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 2 ) = ( 𝐹 ‘ 2 ) )
12 fveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 2 ) = ( 𝐺 ‘ 2 ) )
13 11 12 oveqan12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ‘ 2 ) − ( 𝑔 ‘ 2 ) ) = ( ( 𝐹 ‘ 2 ) − ( 𝐺 ‘ 2 ) ) )
14 13 oveq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑓 ‘ 2 ) − ( 𝑔 ‘ 2 ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 2 ) − ( 𝐺 ‘ 2 ) ) ↑ 2 ) )
15 10 14 oveq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑓 ‘ 2 ) − ( 𝑔 ‘ 2 ) ) ↑ 2 ) ) = ( ( ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 2 ) − ( 𝐺 ‘ 2 ) ) ↑ 2 ) ) )
16 15 fveq2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( √ ‘ ( ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑓 ‘ 2 ) − ( 𝑔 ‘ 2 ) ) ↑ 2 ) ) ) = ( √ ‘ ( ( ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 2 ) − ( 𝐺 ‘ 2 ) ) ↑ 2 ) ) ) )
17 16 adantl ⊢ ( ( ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( √ ‘ ( ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑓 ‘ 2 ) − ( 𝑔 ‘ 2 ) ) ↑ 2 ) ) ) = ( √ ‘ ( ( ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 2 ) − ( 𝐺 ‘ 2 ) ) ↑ 2 ) ) ) )
18 simpl ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐹 ∈ 𝑋 )
19 simpr ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐺 ∈ 𝑋 )
20 fvexd ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( √ ‘ ( ( ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 2 ) − ( 𝐺 ‘ 2 ) ) ↑ 2 ) ) ) ∈ V )
21 6 17 18 19 20 ovmpod ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ ( ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑓 ‘ 2 ) − ( 𝑔 ‘ 2 ) ) ↑ 2 ) ) ) ) 𝐺 ) = ( √ ‘ ( ( ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 2 ) − ( 𝐺 ‘ 2 ) ) ↑ 2 ) ) ) )
22 5 21 syl5eq ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) = ( √ ‘ ( ( ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 2 ) − ( 𝐺 ‘ 2 ) ) ↑ 2 ) ) ) )