Theorem rrxmetfi

Description: Euclidean space is a metric space. Finite dimensional version. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypothesis	rrxmetfi.1	⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
Assertion	rrxmetfi	⊢ ( 𝐼 ∈ Fin → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝐼 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrxmetfi.1	⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
2		eqid	⊢ { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
3	2 1	rrxmet	⊢ ( 𝐼 ∈ Fin → 𝐷 ∈ ( Met ‘ { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) )
4		eqid	⊢ ( ℝ^ ‘ 𝐼 ) = ( ℝ^ ‘ 𝐼 )
5		eqid	⊢ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( Base ‘ ( ℝ^ ‘ 𝐼 ) )
6	4 5	rrxbase	⊢ ( 𝐼 ∈ Fin → ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
7		id	⊢ ( 𝐼 ∈ Fin → 𝐼 ∈ Fin )
8	7 4 5	rrxbasefi	⊢ ( 𝐼 ∈ Fin → ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( ℝ ↑m 𝐼 ) )
9	6 8	eqtr3d	⊢ ( 𝐼 ∈ Fin → { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } = ( ℝ ↑m 𝐼 ) )
10	9	fveq2d	⊢ ( 𝐼 ∈ Fin → ( Met ‘ { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) = ( Met ‘ ( ℝ ↑m 𝐼 ) ) )
11	3 10	eleqtrd	⊢ ( 𝐼 ∈ Fin → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝐼 ) ) )