Theorem rrndsxmet

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

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

Proof

Step	Hyp	Ref	Expression
1		rrndsxmet.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		rrndsxmet.2	⊢ 𝐷 = ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) , 𝑔 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) )
3	1 2	rrndsmet	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝑋 ) ) )
4		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝑋 ) ) → 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑m 𝑋 ) ) )
5	3 4	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑m 𝑋 ) ) )