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 ) ) ) )