Metamath Proof Explorer

Theorem rrxmfval

Description: The value of the Euclidean metric. Compare with rrnval . (Contributed by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Hypotheses rrxmval.1 
|- X = { h e. ( RR ^m I ) | h finSupp 0 }
rrxmval.d 
|- D = ( dist ` ( RR^ ` I ) )
Assertion rrxmfval 
|- ( I e. V -> D = ( f e. X , g e. X |-> ( sqrt ` sum_ k e. ( ( f supp 0 ) u. ( g supp 0 ) ) ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 rrxmval.1 
 |-  X = { h e. ( RR ^m I ) | h finSupp 0 }
2 rrxmval.d 
 |-  D = ( dist ` ( RR^ ` I ) )
3 eqid 
 |-  ( f e. ( Base ` ( RR^ ` I ) ) , g e. ( Base ` ( RR^ ` I ) ) |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) = ( f e. ( Base ` ( RR^ ` I ) ) , g e. ( Base ` ( RR^ ` I ) ) |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) )
4 fvex 
 |-  ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) e. _V
5 3 4 fnmpoi 
 |-  ( f e. ( Base ` ( RR^ ` I ) ) , g e. ( Base ` ( RR^ ` I ) ) |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) Fn ( ( Base ` ( RR^ ` I ) ) X. ( Base ` ( RR^ ` I ) ) )
6 eqid 
 |-  ( RR^ ` I ) = ( RR^ ` I )
7 eqid 
 |-  ( Base ` ( RR^ ` I ) ) = ( Base ` ( RR^ ` I ) )
8 6 7 rrxds 
 |-  ( I e. V -> ( f e. ( Base ` ( RR^ ` I ) ) , g e. ( Base ` ( RR^ ` I ) ) |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) = ( dist ` ( RR^ ` I ) ) )
9 2 8 eqtr4id 
 |-  ( I e. V -> D = ( f e. ( Base ` ( RR^ ` I ) ) , g e. ( Base ` ( RR^ ` I ) ) |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) )
10 6 7 rrxbase 
 |-  ( I e. V -> ( Base ` ( RR^ ` I ) ) = { h e. ( RR ^m I ) | h finSupp 0 } )
11 1 10 eqtr4id 
 |-  ( I e. V -> X = ( Base ` ( RR^ ` I ) ) )
12 11 sqxpeqd 
 |-  ( I e. V -> ( X X. X ) = ( ( Base ` ( RR^ ` I ) ) X. ( Base ` ( RR^ ` I ) ) ) )
13 9 12 fneq12d 
 |-  ( I e. V -> ( D Fn ( X X. X ) <-> ( f e. ( Base ` ( RR^ ` I ) ) , g e. ( Base ` ( RR^ ` I ) ) |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) Fn ( ( Base ` ( RR^ ` I ) ) X. ( Base ` ( RR^ ` I ) ) ) ) )
14 5 13 mpbiri 
 |-  ( I e. V -> D Fn ( X X. X ) )
15 fnov 
 |-  ( D Fn ( X X. X ) <-> D = ( f e. X , g e. X |-> ( f D g ) ) )
16 14 15 sylib 
 |-  ( I e. V -> D = ( f e. X , g e. X |-> ( f D g ) ) )
17 1 2 rrxmval 
 |-  ( ( I e. V /\ f e. X /\ g e. X ) -> ( f D g ) = ( sqrt ` sum_ k e. ( ( f supp 0 ) u. ( g supp 0 ) ) ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )
18 17 mpoeq3dva 
 |-  ( I e. V -> ( f e. X , g e. X |-> ( f D g ) ) = ( f e. X , g e. X |-> ( sqrt ` sum_ k e. ( ( f supp 0 ) u. ( g supp 0 ) ) ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
19 16 18 eqtrd 
 |-  ( I e. V -> D = ( f e. X , g e. X |-> ( sqrt ` sum_ k e. ( ( f supp 0 ) u. ( g supp 0 ) ) ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )