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