Metamath Proof Explorer

Theorem ehleudis

Description: The Euclidean distance function in a real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023)

Ref Expression
Hypotheses ehleudis.i 
|- I = ( 1 ... N )
ehleudis.e 
|- E = ( EEhil ` N )
ehleudis.x 
|- X = ( RR ^m I )
ehleudis.d 
|- D = ( dist ` E )
Assertion ehleudis 
|- ( N e. NN0 -> D = ( f e. X , g e. X |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 ehleudis.i 
 |-  I = ( 1 ... N )
2 ehleudis.e 
 |-  E = ( EEhil ` N )
3 ehleudis.x 
 |-  X = ( RR ^m I )
4 ehleudis.d 
 |-  D = ( dist ` E )
5 2 ehlval 
 |-  ( N e. NN0 -> E = ( RR^ ` ( 1 ... N ) ) )
6 5 fveq2d 
 |-  ( N e. NN0 -> ( dist ` E ) = ( dist ` ( RR^ ` ( 1 ... N ) ) ) )
7 4 6 syl5eq 
 |-  ( N e. NN0 -> D = ( dist ` ( RR^ ` ( 1 ... N ) ) ) )
8 fzfi 
 |-  ( 1 ... N ) e. Fin
9 1 8 eqeltri 
 |-  I e. Fin
10 1 eqcomi 
 |-  ( 1 ... N ) = I
11 10 fveq2i 
 |-  ( RR^ ` ( 1 ... N ) ) = ( RR^ ` I )
12 11 fveq2i 
 |-  ( dist ` ( RR^ ` ( 1 ... N ) ) ) = ( dist ` ( RR^ ` I ) )
13 eqid 
 |-  ( RR^ ` I ) = ( RR^ ` I )
14 13 3 rrxdsfi 
 |-  ( I e. Fin -> ( dist ` ( RR^ ` I ) ) = ( f e. X , g e. X |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
15 12 14 syl5eq 
 |-  ( I e. Fin -> ( dist ` ( RR^ ` ( 1 ... N ) ) ) = ( f e. X , g e. X |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
16 9 15 mp1i 
 |-  ( N e. NN0 -> ( dist ` ( RR^ ` ( 1 ... N ) ) ) = ( f e. X , g e. X |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
17 7 16 eqtrd 
 |-  ( N e. NN0 -> D = ( f e. X , g e. X |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )