Theorem rrndsmet

Description: D is a metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	rrndsmet.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	rrndsmet.2	⊢ 𝐷 = ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) , 𝑔 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) )
Assertion	rrndsmet	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrndsmet.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		rrndsmet.2	⊢ 𝐷 = ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) , 𝑔 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) )
3	2	a1i	⊢ ( 𝜑 → 𝐷 = ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) , 𝑔 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
4		eqid	⊢ ( ℝ^ ‘ 𝑋 ) = ( ℝ^ ‘ 𝑋 )
5		eqid	⊢ ( ℝ ↑m 𝑋 ) = ( ℝ ↑m 𝑋 )
6	4 5	rrxdsfi	⊢ ( 𝑋 ∈ Fin → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) = ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) , 𝑔 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
7	1 6	syl	⊢ ( 𝜑 → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) = ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) , 𝑔 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
8	3 7	eqtr4d	⊢ ( 𝜑 → 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) )
9		eqid	⊢ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) = ( dist ‘ ( ℝ^ ‘ 𝑋 ) )
10	9	rrxmetfi	⊢ ( 𝑋 ∈ Fin → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ ( Met ‘ ( ℝ ↑m 𝑋 ) ) )
11	1 10	syl	⊢ ( 𝜑 → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ ( Met ‘ ( ℝ ↑m 𝑋 ) ) )
12	8 11	eqeltrd	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝑋 ) ) )