Metamath Proof Explorer

Theorem rrxdsfival

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

Ref Expression
Hypotheses rrxdsfival.1 
|- X = ( RR ^m I )
rrxdsfival.d 
|- D = ( dist ` ( RR^ ` I ) )
Assertion rrxdsfival 
|- ( ( I e. Fin /\ 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 rrxdsfival.1 
 |-  X = ( RR ^m I )
2 rrxdsfival.d 
 |-  D = ( dist ` ( RR^ ` I ) )
3 eqid 
 |-  ( RR^ ` I ) = ( RR^ ` I )
4 3 1 rrxdsfi 
 |-  ( I e. Fin -> ( dist ` ( RR^ ` I ) ) = ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
5 2 4 eqtrid 
 |-  ( I e. Fin -> D = ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
6 5 oveqd 
 |-  ( I e. Fin -> ( F D G ) = ( F ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) G ) )
7 6 3ad2ant1 
 |-  ( ( I e. Fin /\ F e. X /\ G e. X ) -> ( F D G ) = ( F ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) G ) )
8 eqidd 
 |-  ( ( I e. Fin /\ F e. X /\ G e. X ) -> ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) = ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
9 fveq1 
 |-  ( x = F -> ( x ` k ) = ( F ` k ) )
10 fveq1 
 |-  ( y = G -> ( y ` k ) = ( G ` k ) )
11 9 10 oveqan12d 
 |-  ( ( x = F /\ y = G ) -> ( ( x ` k ) - ( y ` k ) ) = ( ( F ` k ) - ( G ` k ) ) )
12 11 oveq1d 
 |-  ( ( x = F /\ y = G ) -> ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
13 12 sumeq2sdv 
 |-  ( ( x = F /\ y = G ) -> sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) = sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
14 13 fveq2d 
 |-  ( ( x = F /\ y = G ) -> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
15 14 adantl 
 |-  ( ( ( I e. Fin /\ F e. X /\ G e. X ) /\ ( x = F /\ y = G ) ) -> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) = ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
16 simp2 
 |-  ( ( I e. Fin /\ F e. X /\ G e. X ) -> F e. X )
17 simp3 
 |-  ( ( I e. Fin /\ F e. X /\ G e. X ) -> G e. X )
18 fvexd 
 |-  ( ( I e. Fin /\ F e. X /\ G e. X ) -> ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) e. _V )
19 8 15 16 17 18 ovmpod 
 |-  ( ( I e. Fin /\ F e. X /\ G e. X ) -> ( F ( x e. X , y e. X |-> ( sqrt ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) G ) = ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
20 7 19 eqtrd 
 |-  ( ( I e. Fin /\ F e. X /\ G e. X ) -> ( F D G ) = ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )