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 
|- D = ( dist ` ( RR^ ` I ) )
Assertion rrxmetfi 
|- ( I e. Fin -> D e. ( Met ` ( RR ^m I ) ) )

Proof

Step Hyp Ref Expression
1 rrxmetfi.1 
 |-  D = ( dist ` ( RR^ ` I ) )
2 eqid 
 |-  { h e. ( RR ^m I ) | h finSupp 0 } = { h e. ( RR ^m I ) | h finSupp 0 }
3 2 1 rrxmet 
 |-  ( I e. Fin -> D e. ( Met ` { h e. ( RR ^m I ) | h finSupp 0 } ) )
4 eqid 
 |-  ( RR^ ` I ) = ( RR^ ` I )
5 eqid 
 |-  ( Base ` ( RR^ ` I ) ) = ( Base ` ( RR^ ` I ) )
6 4 5 rrxbase 
 |-  ( I e. Fin -> ( Base ` ( RR^ ` I ) ) = { h e. ( RR ^m I ) | h finSupp 0 } )
7 id 
 |-  ( I e. Fin -> I e. Fin )
8 7 4 5 rrxbasefi 
 |-  ( I e. Fin -> ( Base ` ( RR^ ` I ) ) = ( RR ^m I ) )
9 6 8 eqtr3d 
 |-  ( I e. Fin -> { h e. ( RR ^m I ) | h finSupp 0 } = ( RR ^m I ) )
10 9 fveq2d 
 |-  ( I e. Fin -> ( Met ` { h e. ( RR ^m I ) | h finSupp 0 } ) = ( Met ` ( RR ^m I ) ) )
11 3 10 eleqtrd 
 |-  ( I e. Fin -> D e. ( Met ` ( RR ^m I ) ) )