Metamath Proof Explorer

Theorem rrxdsfi

Description: The distance over generalized Euclidean spaces. Finite dimensional case. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses rrxdsfi.h ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
rrxdsfi.b ⊢ 𝐵 = ( ℝ ↑m 𝐼 )
Assertion rrxdsfi ( 𝐼 ∈ Fin → ( dist ‘ 𝐻 ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 rrxdsfi.h ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
2 rrxdsfi.b ⊢ 𝐵 = ( ℝ ↑m 𝐼 )
3 id ⊢ ( 𝐼 ∈ Fin → 𝐼 ∈ Fin )
4 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
5 3 1 4 rrxbasefi ⊢ ( 𝐼 ∈ Fin → ( Base ‘ 𝐻 ) = ( ℝ ↑m 𝐼 ) )
6 2 5 eqtr4id ⊢ ( 𝐼 ∈ Fin → 𝐵 = ( Base ‘ 𝐻 ) )
7 6 adantr ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝐻 ) )
8 df-refld ⊢ ℝfld = ( ℂfld ↾s ℝ )
9 8 oveq1i ⊢ ( ℝfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( ( ℂfld ↾s ℝ ) Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) )
10 simp1 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → 𝐼 ∈ Fin )
11 simpr ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ) → 𝑓 ∈ 𝐵 )
12 11 2 eleqtrdi ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ) → 𝑓 ∈ ( ℝ ↑m 𝐼 ) )
13 12 3adant3 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → 𝑓 ∈ ( ℝ ↑m 𝐼 ) )
14 elmapi ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) → 𝑓 : 𝐼 ⟶ ℝ )
15 13 14 syl ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → 𝑓 : 𝐼 ⟶ ℝ )
16 15 ffvelrnda ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ )
17 simpr ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ 𝐵 )
18 17 2 eleqtrdi ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ ( ℝ ↑m 𝐼 ) )
19 18 3adant2 ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ ( ℝ ↑m 𝐼 ) )
20 elmapi ⊢ ( 𝑔 ∈ ( ℝ ↑m 𝐼 ) → 𝑔 : 𝐼 ⟶ ℝ )
21 19 20 syl ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → 𝑔 : 𝐼 ⟶ ℝ )
22 21 ffvelrnda ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑘 ) ∈ ℝ )
23 16 22 resubcld ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ∈ ℝ )
24 23 resqcld ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ )
25 10 24 regsumfsum ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → ( ( ℂfld ↾s ℝ ) Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) = Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) )
26 9 25 eqtr2id ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) = ( ℝfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
27 26 fveq2d ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ ( ℝfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) )
28 27 3expb ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ ( ℝfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) )
29 6 7 28 mpoeq123dva ⊢ ( 𝐼 ∈ Fin → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( 𝑓 ∈ ( Base ‘ 𝐻 ) , 𝑔 ∈ ( Base ‘ 𝐻 ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) ) )
30 1 4 rrxds ⊢ ( 𝐼 ∈ Fin → ( 𝑓 ∈ ( Base ‘ 𝐻 ) , 𝑔 ∈ ( Base ‘ 𝐻 ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) ) = ( dist ‘ 𝐻 ) )
31 29 30 eqtr2d ⊢ ( 𝐼 ∈ Fin → ( dist ‘ 𝐻 ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )