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 { 1 } )
ehl1eudis.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
Assertion ehl1eudis 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( abs ‘ ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ) )

Proof

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