This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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