Metamath Proof Explorer

Theorem rrxdsfi

Description: The distance over generalized Euclidean spaces. Finite dimensional case. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses rrxdsfi.h 
|- H = ( RR^ ` I )
rrxdsfi.b 
|- B = ( RR ^m I )
Assertion rrxdsfi 
|- ( I e. Fin -> ( dist ` H ) = ( f e. B , g e. B |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 rrxdsfi.h 
 |-  H = ( RR^ ` I )
2 rrxdsfi.b 
 |-  B = ( RR ^m I )
3 id 
 |-  ( I e. Fin -> I e. Fin )
4 eqid 
 |-  ( Base ` H ) = ( Base ` H )
5 3 1 4 rrxbasefi 
 |-  ( I e. Fin -> ( Base ` H ) = ( RR ^m I ) )
6 2 5 eqtr4id 
 |-  ( I e. Fin -> B = ( Base ` H ) )
7 6 adantr 
 |-  ( ( I e. Fin /\ f e. B ) -> B = ( Base ` H ) )
8 df-refld 
 |-  RRfld = ( CCfld |`s RR )
9 8 oveq1i 
 |-  ( RRfld gsum ( k e. I |-> ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) = ( ( CCfld |`s RR ) gsum ( k e. I |-> ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )
10 simp1 
 |-  ( ( I e. Fin /\ f e. B /\ g e. B ) -> I e. Fin )
11 simpr 
 |-  ( ( I e. Fin /\ f e. B ) -> f e. B )
12 11 2 eleqtrdi 
 |-  ( ( I e. Fin /\ f e. B ) -> f e. ( RR ^m I ) )
13 12 3adant3 
 |-  ( ( I e. Fin /\ f e. B /\ g e. B ) -> f e. ( RR ^m I ) )
14 elmapi 
 |-  ( f e. ( RR ^m I ) -> f : I --> RR )
15 13 14 syl 
 |-  ( ( I e. Fin /\ f e. B /\ g e. B ) -> f : I --> RR )
16 15 ffvelcdmda 
 |-  ( ( ( I e. Fin /\ f e. B /\ g e. B ) /\ k e. I ) -> ( f ` k ) e. RR )
17 simpr 
 |-  ( ( I e. Fin /\ g e. B ) -> g e. B )
18 17 2 eleqtrdi 
 |-  ( ( I e. Fin /\ g e. B ) -> g e. ( RR ^m I ) )
19 18 3adant2 
 |-  ( ( I e. Fin /\ f e. B /\ g e. B ) -> g e. ( RR ^m I ) )
20 elmapi 
 |-  ( g e. ( RR ^m I ) -> g : I --> RR )
21 19 20 syl 
 |-  ( ( I e. Fin /\ f e. B /\ g e. B ) -> g : I --> RR )
22 21 ffvelcdmda 
 |-  ( ( ( I e. Fin /\ f e. B /\ g e. B ) /\ k e. I ) -> ( g ` k ) e. RR )
23 16 22 resubcld 
 |-  ( ( ( I e. Fin /\ f e. B /\ g e. B ) /\ k e. I ) -> ( ( f ` k ) - ( g ` k ) ) e. RR )
24 23 resqcld 
 |-  ( ( ( I e. Fin /\ f e. B /\ g e. B ) /\ k e. I ) -> ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) e. RR )
25 10 24 regsumfsum 
 |-  ( ( I e. Fin /\ f e. B /\ g e. B ) -> ( ( CCfld |`s RR ) gsum ( k e. I |-> ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) = sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) )
26 9 25 eqtr2id 
 |-  ( ( I e. Fin /\ f e. B /\ g e. B ) -> sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) = ( RRfld gsum ( k e. I |-> ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
27 26 fveq2d 
 |-  ( ( I e. Fin /\ f e. B /\ g e. B ) -> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) = ( sqrt ` ( RRfld gsum ( k e. I |-> ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) ) )
28 27 3expb 
 |-  ( ( I e. Fin /\ ( f e. B /\ g e. B ) ) -> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) = ( sqrt ` ( RRfld gsum ( k e. I |-> ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) ) )
29 6 7 28 mpoeq123dva 
 |-  ( I e. Fin -> ( f e. B , g e. B |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) = ( f e. ( Base ` H ) , g e. ( Base ` H ) |-> ( sqrt ` ( RRfld gsum ( k e. I |-> ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) ) ) )
30 1 4 rrxds 
 |-  ( I e. Fin -> ( f e. ( Base ` H ) , g e. ( Base ` H ) |-> ( sqrt ` ( RRfld gsum ( k e. I |-> ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) ) ) = ( dist ` H ) )
31 29 30 eqtr2d 
 |-  ( I e. Fin -> ( dist ` H ) = ( f e. B , g e. B |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )