This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rrxmfval

Description: The value of the Euclidean metric. Compare with rrnval . (Contributed by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Hypotheses rrxmval.1 ⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
rrxmval.d ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
Assertion rrxmfval ( 𝐼 ∈ 𝑉 → 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ ( ( 𝑓 supp 0 ) ∪ ( 𝑔 supp 0 ) ) ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 rrxmval.1 ⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 rrxmval.d ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
3 eqid ⊢ ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) = ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) )
4 fvex ⊢ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ∈ V
5 3 4 fnmpoi ⊢ ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) Fn ( ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) × ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) )
6 eqid ⊢ ( ℝ^ ‘ 𝐼 ) = ( ℝ^ ‘ 𝐼 )
7 eqid ⊢ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( Base ‘ ( ℝ^ ‘ 𝐼 ) )
8 6 7 rrxds ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) = ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) )
9 2 8 eqtr4id ⊢ ( 𝐼 ∈ 𝑉 → 𝐷 = ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) )
10 6 7 rrxbase ⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
11 1 10 eqtr4id ⊢ ( 𝐼 ∈ 𝑉 → 𝑋 = ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) )
12 11 sqxpeqd ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑋 × 𝑋 ) = ( ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) × ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) )
13 9 12 fneq12d ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐷 Fn ( 𝑋 × 𝑋 ) ↔ ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) Fn ( ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) × ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) ) )
14 5 13 mpbiri ⊢ ( 𝐼 ∈ 𝑉 → 𝐷 Fn ( 𝑋 × 𝑋 ) )
15 fnov ⊢ ( 𝐷 Fn ( 𝑋 × 𝑋 ) ↔ 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( 𝑓 𝐷 𝑔 ) ) )
16 14 15 sylib ⊢ ( 𝐼 ∈ 𝑉 → 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( 𝑓 𝐷 𝑔 ) ) )
17 1 2 rrxmval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( 𝑓 𝐷 𝑔 ) = ( √ ‘ Σ 𝑘 ∈ ( ( 𝑓 supp 0 ) ∪ ( 𝑔 supp 0 ) ) ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) )
18 17 mpoeq3dva ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( 𝑓 𝐷 𝑔 ) ) = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ ( ( 𝑓 supp 0 ) ∪ ( 𝑔 supp 0 ) ) ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
19 16 18 eqtrd ⊢ ( 𝐼 ∈ 𝑉 → 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ ( ( 𝑓 supp 0 ) ∪ ( 𝑔 supp 0 ) ) ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )