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 ffvelrnda
 |-  ( ( ( 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 ffvelrnda
 |-  ( ( ( 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 ) ) ) )