Metamath Proof Explorer

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 
|- ( ph -> X e. Fin )
rrndsmet.2 
|- D = ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )
Assertion rrndsmet 
|- ( ph -> D e. ( Met ` ( RR ^m X ) ) )

Proof

Step Hyp Ref Expression
1 rrndsmet.1 
 |-  ( ph -> X e. Fin )
2 rrndsmet.2 
 |-  D = ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )
3 2 a1i 
 |-  ( ph -> D = ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
4 eqid 
 |-  ( RR^ ` X ) = ( RR^ ` X )
5 eqid 
 |-  ( RR ^m X ) = ( RR ^m X )
6 4 5 rrxdsfi 
 |-  ( X e. Fin -> ( dist ` ( RR^ ` X ) ) = ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
7 1 6 syl 
 |-  ( ph -> ( dist ` ( RR^ ` X ) ) = ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
8 3 7 eqtr4d 
 |-  ( ph -> D = ( dist ` ( RR^ ` X ) ) )
9 eqid 
 |-  ( dist ` ( RR^ ` X ) ) = ( dist ` ( RR^ ` X ) )
10 9 rrxmetfi 
 |-  ( X e. Fin -> ( dist ` ( RR^ ` X ) ) e. ( Met ` ( RR ^m X ) ) )
11 1 10 syl 
 |-  ( ph -> ( dist ` ( RR^ ` X ) ) e. ( Met ` ( RR ^m X ) ) )
12 8 11 eqeltrd 
 |-  ( ph -> D e. ( Met ` ( RR ^m X ) ) )