Metamath Proof Explorer

Theorem ehleudisval

Description: The value of 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 ehleudisval 
|- ( ( N e. NN0 /\ F e. X /\ G e. X ) -> ( F D G ) = ( 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 7 oveqd 
 |-  ( N e. NN0 -> ( F D G ) = ( F ( dist ` ( RR^ ` ( 1 ... N ) ) ) G ) )
9 8 3ad2ant1 
 |-  ( ( N e. NN0 /\ F e. X /\ G e. X ) -> ( F D G ) = ( F ( dist ` ( RR^ ` ( 1 ... N ) ) ) G ) )
10 fzfi 
 |-  ( 1 ... N ) e. Fin
11 1 10 eqeltri 
 |-  I e. Fin
12 3 eleq2i 
 |-  ( F e. X <-> F e. ( RR ^m I ) )
13 12 biimpi 
 |-  ( F e. X -> F e. ( RR ^m I ) )
14 13 3ad2ant2 
 |-  ( ( N e. NN0 /\ F e. X /\ G e. X ) -> F e. ( RR ^m I ) )
15 3 eleq2i 
 |-  ( G e. X <-> G e. ( RR ^m I ) )
16 15 biimpi 
 |-  ( G e. X -> G e. ( RR ^m I ) )
17 16 3ad2ant3 
 |-  ( ( N e. NN0 /\ F e. X /\ G e. X ) -> G e. ( RR ^m I ) )
18 eqid 
 |-  ( RR ^m I ) = ( RR ^m I )
19 1 eqcomi 
 |-  ( 1 ... N ) = I
20 19 fveq2i 
 |-  ( RR^ ` ( 1 ... N ) ) = ( RR^ ` I )
21 20 fveq2i 
 |-  ( dist ` ( RR^ ` ( 1 ... N ) ) ) = ( dist ` ( RR^ ` I ) )
22 18 21 rrxdsfival 
 |-  ( ( I e. Fin /\ F e. ( RR ^m I ) /\ G e. ( RR ^m I ) ) -> ( F ( dist ` ( RR^ ` ( 1 ... N ) ) ) G ) = ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
23 11 14 17 22 mp3an2i 
 |-  ( ( N e. NN0 /\ F e. X /\ G e. X ) -> ( F ( dist ` ( RR^ ` ( 1 ... N ) ) ) G ) = ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
24 9 23 eqtrd 
 |-  ( ( N e. NN0 /\ F e. X /\ G e. X ) -> ( F D G ) = ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )