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 ⊢X=h∈ℝI|finSupp0⁡h
rrxmval.d ⊢D=dist⁡msup
Assertion rrxmfval ⊢I∈V→D=f∈X,g∈X⟼∑k∈supp0⁡f∪supp0⁡gf⁡k−g⁡k2

Proof

Step Hyp Ref Expression
1 rrxmval.1 ⊢X=h∈ℝI|finSupp0⁡h
2 rrxmval.d ⊢D=dist⁡msup
3 eqid ⊢f∈Basemsup,g∈Basemsup⟼∑ℝfldx∈If⁡x−g⁡x2=f∈Basemsup,g∈Basemsup⟼∑ℝfldx∈If⁡x−g⁡x2
4 fvex ⊢∑ℝfldx∈If⁡x−g⁡x2∈V
5 3 4 fnmpoi ⊢f∈Basemsup,g∈Basemsup⟼∑ℝfldx∈If⁡x−g⁡x2FnBasemsup×Basemsup
6 eqid ⊢msup=msup
7 eqid ⊢Basemsup=Basemsup
8 6 7 rrxds ⊢I∈V→f∈Basemsup,g∈Basemsup⟼∑ℝfldx∈If⁡x−g⁡x2=dist⁡msup
9 2 8 eqtr4id ⊢I∈V→D=f∈Basemsup,g∈Basemsup⟼∑ℝfldx∈If⁡x−g⁡x2
10 6 7 rrxbase ⊢I∈V→Basemsup=h∈ℝI|finSupp0⁡h
11 1 10 eqtr4id ⊢I∈V→X=Basemsup
12 11 sqxpeqd ⊢I∈V→X×X=Basemsup×Basemsup
13 9 12 fneq12d ⊢I∈V→DFnX×X↔f∈Basemsup,g∈Basemsup⟼∑ℝfldx∈If⁡x−g⁡x2FnBasemsup×Basemsup
14 5 13 mpbiri ⊢I∈V→DFnX×X
15 fnov ⊢DFnX×X↔D=f∈X,g∈X⟼fDg
16 14 15 sylib ⊢I∈V→D=f∈X,g∈X⟼fDg
17 1 2 rrxmval ⊢I∈V∧f∈X∧g∈X→fDg=∑k∈supp0⁡f∪supp0⁡gf⁡k−g⁡k2
18 17 mpoeq3dva ⊢I∈V→f∈X,g∈X⟼fDg=f∈X,g∈X⟼∑k∈supp0⁡f∪supp0⁡gf⁡k−g⁡k2
19 16 18 eqtrd ⊢I∈V→D=f∈X,g∈X⟼∑k∈supp0⁡f∪supp0⁡gf⁡k−g⁡k2