Metamath Proof Explorer

Theorem ehl2eudis

Description: 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 ( 0 ..^ 2 ) )
ehl2eudis.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
Assertion ehl2eudis 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ ( ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 ehl2eudis.e ⊢ 𝐸 = ( 𝔼hil ‘ 2 )
2 ehl2eudis.x ⊢ 𝑋 = ( ℝ ↑m ( 0 ..^ 2 ) )
3 ehl2eudis.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
4 2nn0 ⊢ 2 ∈ ℕ0
5 fzo0to2pr ⊢ ( 0 ..^ 2 ) = { 0 , 1 }
6 5 eqcomi ⊢ { 0 , 1 } = ( 0 ..^ 2 )
7 6 oveq2i ⊢ ( ℝ ↑m { 0 , 1 } ) = ( ℝ ↑m ( 0 ..^ 2 ) )
8 2 7 eqtr4i ⊢ 𝑋 = ( ℝ ↑m { 0 , 1 } )
9 6 1 8 3 ehleudis ⊢ ( 2 ∈ ℕ0 → 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ { 0 , 1 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
10 4 9 ax-mp ⊢ 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ { 0 , 1 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) )
11 fveq2 ⊢ ( 𝑘 = 0 → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 0 ) )
12 fveq2 ⊢ ( 𝑘 = 0 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 0 ) )
13 11 12 oveq12d ⊢ ( 𝑘 = 0 → ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) = ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) )
14 13 oveq1d ⊢ ( 𝑘 = 0 → ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) )
15 fveq2 ⊢ ( 𝑘 = 1 → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 1 ) )
16 fveq2 ⊢ ( 𝑘 = 1 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 1 ) )
17 15 16 oveq12d ⊢ ( 𝑘 = 1 → ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) = ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) )
18 17 oveq1d ⊢ ( 𝑘 = 1 → ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) )
19 8 eleq2i ⊢ ( 𝑓 ∈ 𝑋 ↔ 𝑓 ∈ ( ℝ ↑m { 0 , 1 } ) )
20 reex ⊢ ℝ ∈ V
21 prex ⊢ { 0 , 1 } ∈ V
22 20 21 elmap ⊢ ( 𝑓 ∈ ( ℝ ↑m { 0 , 1 } ) ↔ 𝑓 : { 0 , 1 } ⟶ ℝ )
23 19 22 bitri ⊢ ( 𝑓 ∈ 𝑋 ↔ 𝑓 : { 0 , 1 } ⟶ ℝ )
24 id ⊢ ( 𝑓 : { 0 , 1 } ⟶ ℝ → 𝑓 : { 0 , 1 } ⟶ ℝ )
25 0elpr01 ⊢ 0 ∈ { 0 , 1 }
26 25 a1i ⊢ ( 𝑓 : { 0 , 1 } ⟶ ℝ → 0 ∈ { 0 , 1 } )
27 24 26 ffvelcdmd ⊢ ( 𝑓 : { 0 , 1 } ⟶ ℝ → ( 𝑓 ‘ 0 ) ∈ ℝ )
28 23 27 sylbi ⊢ ( 𝑓 ∈ 𝑋 → ( 𝑓 ‘ 0 ) ∈ ℝ )
29 28 adantr ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( 𝑓 ‘ 0 ) ∈ ℝ )
30 8 eleq2i ⊢ ( 𝑔 ∈ 𝑋 ↔ 𝑔 ∈ ( ℝ ↑m { 0 , 1 } ) )
31 20 21 elmap ⊢ ( 𝑔 ∈ ( ℝ ↑m { 0 , 1 } ) ↔ 𝑔 : { 0 , 1 } ⟶ ℝ )
32 30 31 bitri ⊢ ( 𝑔 ∈ 𝑋 ↔ 𝑔 : { 0 , 1 } ⟶ ℝ )
33 id ⊢ ( 𝑔 : { 0 , 1 } ⟶ ℝ → 𝑔 : { 0 , 1 } ⟶ ℝ )
34 25 a1i ⊢ ( 𝑔 : { 0 , 1 } ⟶ ℝ → 0 ∈ { 0 , 1 } )
35 33 34 ffvelcdmd ⊢ ( 𝑔 : { 0 , 1 } ⟶ ℝ → ( 𝑔 ‘ 0 ) ∈ ℝ )
36 32 35 sylbi ⊢ ( 𝑔 ∈ 𝑋 → ( 𝑔 ‘ 0 ) ∈ ℝ )
37 36 adantl ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( 𝑔 ‘ 0 ) ∈ ℝ )
38 29 37 resubcld ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ∈ ℝ )
39 38 resqcld ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) ∈ ℝ )
40 39 recnd ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) ∈ ℂ )
41 1elpr01 ⊢ 1 ∈ { 0 , 1 }
42 41 a1i ⊢ ( 𝑓 : { 0 , 1 } ⟶ ℝ → 1 ∈ { 0 , 1 } )
43 24 42 ffvelcdmd ⊢ ( 𝑓 : { 0 , 1 } ⟶ ℝ → ( 𝑓 ‘ 1 ) ∈ ℝ )
44 23 43 sylbi ⊢ ( 𝑓 ∈ 𝑋 → ( 𝑓 ‘ 1 ) ∈ ℝ )
45 44 adantr ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( 𝑓 ‘ 1 ) ∈ ℝ )
46 41 a1i ⊢ ( 𝑔 : { 0 , 1 } ⟶ ℝ → 1 ∈ { 0 , 1 } )
47 33 46 ffvelcdmd ⊢ ( 𝑔 : { 0 , 1 } ⟶ ℝ → ( 𝑔 ‘ 1 ) ∈ ℝ )
48 32 47 sylbi ⊢ ( 𝑔 ∈ 𝑋 → ( 𝑔 ‘ 1 ) ∈ ℝ )
49 48 adantl ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( 𝑔 ‘ 1 ) ∈ ℝ )
50 45 49 resubcld ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ∈ ℝ )
51 50 resqcld ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) ∈ ℝ )
52 51 recnd ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) ∈ ℂ )
53 40 52 jca ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) ∈ ℂ ∧ ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) ∈ ℂ ) )
54 c0ex ⊢ 0 ∈ V
55 1ex ⊢ 1 ∈ V
56 54 55 pm3.2i ⊢ ( 0 ∈ V ∧ 1 ∈ V )
57 56 a1i ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( 0 ∈ V ∧ 1 ∈ V ) )
58 0ne1 ⊢ 0 ≠ 1
59 58 a1i ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → 0 ≠ 1 )
60 14 18 53 57 59 sumpr ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → Σ 𝑘 ∈ { 0 , 1 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) ) )
61 60 fveq2d ⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ { 0 , 1 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ ( ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) ) ) )
62 61 mpoeq3ia ⊢ ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ { 0 , 1 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ ( ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) ) ) )
63 10 62 eqtri ⊢ 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ ( ( ( ( 𝑓 ‘ 0 ) − ( 𝑔 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) ) ) )