Metamath Proof Explorer

Theorem ehl1eudis

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

Ref Expression
Hypotheses ehl1eudis.e ⊢ 𝐸 = ( 𝔼hil ‘ 1 )
ehl1eudis.x ⊢ 𝑋 = ( ℝ ↑m { 0 } )
ehl1eudis.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
Assertion ehl1eudis 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( abs ‘ ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 ehl1eudis.e ⊢ 𝐸 = ( 𝔼hil ‘ 1 )
2 ehl1eudis.x ⊢ 𝑋 = ( ℝ ↑m { 0 } )
3 ehl1eudis.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
4 1nn0 ⊢ 1 ∈ ℕ0
5 fzo01 ⊢ ( 0 ..^ 1 ) = { 0 }
6 5 eqcomi ⊢ { 0 } = ( 0 ..^ 1 )
7 6 1 2 3 ehleudis ⊢ ( 1 ∈ ℕ0 → 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ { 0 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
8 4 7 ax-mp ⊢ 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ { 0 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) )
9 0z ⊢ 0 ∈ ℤ
10 2 eleq2i ⊢ ( 𝑓 ∈ 𝑋 ↔ 𝑓 ∈ ( ℝ ↑m { 0 } ) )
11 reex ⊢ ℝ ∈ V
12 snex ⊢ { 0 } ∈ V
13 11 12 elmap ⊢ ( 𝑓 ∈ ( ℝ ↑m { 0 } ) ↔ 𝑓 : { 0 } ⟶ ℝ )
14 10 13 bitri ⊢ ( 𝑓 ∈ 𝑋 ↔ 𝑓 : { 0 } ⟶ ℝ )
15 id ⊢ ( 𝑓 : { 0 } ⟶ ℝ → 𝑓 : { 0 } ⟶ ℝ )
16 c0ex ⊢ 0 ∈ V
17 16 snid ⊢ 0 ∈ { 0 }
18 17 a1i ⊢ ( 𝑓 : { 0 } ⟶ ℝ → 0 ∈ { 0 } )
19 15 18 ffvelcdmd ⊢ ( 𝑓 : { 0 } ⟶ ℝ → ( 𝑓 ‘ 0 ) ∈ ℝ )
20 14 19 sylbi ⊢ ( 𝑓 ∈ 𝑋 → ( 𝑓 ‘ 0 ) ∈ ℝ )
21 20 adantr ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( 𝑓 ‘ 0 ) ∈ ℝ )
22 2 eleq2i ⊢ ( 𝑔 ∈ 𝑋 ↔ 𝑔 ∈ ( ℝ ↑m { 0 } ) )
23 11 12 elmap ⊢ ( 𝑔 ∈ ( ℝ ↑m { 0 } ) ↔ 𝑔 : { 0 } ⟶ ℝ )
24 22 23 bitri ⊢ ( 𝑔 ∈ 𝑋 ↔ 𝑔 : { 0 } ⟶ ℝ )
25 id ⊢ ( 𝑔 : { 0 } ⟶ ℝ → 𝑔 : { 0 } ⟶ ℝ )
26 17 a1i ⊢ ( 𝑔 : { 0 } ⟶ ℝ → 0 ∈ { 0 } )
27 25 26 ffvelcdmd ⊢ ( 𝑔 : { 0 } ⟶ ℝ → ( 𝑔 ‘ 0 ) ∈ ℝ )
28 24 27 sylbi ⊢ ( 𝑔 ∈ 𝑋 → ( 𝑔 ‘ 0 ) ∈ ℝ )
29 28 adantl ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( 𝑔 ‘ 0 ) ∈ ℝ )
30 21 29 resubcld ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ∈ ℝ )
31 30 resqcld ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) ∈ ℝ )
32 31 recnd ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) ∈ ℂ )
33 fveq2 ⊢ ( 𝑘 = 0 → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 0 ) )
34 fveq2 ⊢ ( 𝑘 = 0 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 0 ) )
35 33 34 oveq12d ⊢ ( 𝑘 = 0 → ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) = ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) )
36 35 oveq1d ⊢ ( 𝑘 = 0 → ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) )
37 36 sumsn ⊢ ( ( 0 ∈ ℤ ∧ ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) ∈ ℂ ) → Σ 𝑘 ∈ { 0 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) )
38 9 32 37 sylancr ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → Σ 𝑘 ∈ { 0 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) )
39 38 fveq2d ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ { 0 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) ) )
40 30 absred ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ) = ( √ ‘ ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) ) )
41 39 40 eqtr4d ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ { 0 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) = ( abs ‘ ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ) )
42 41 mpoeq3ia ⊢ ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ { 0 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( abs ‘ ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ) )
43 8 42 eqtri ⊢ 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( abs ‘ ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ) )