Metamath Proof Explorer

Theorem rrxmval

Description: The value of the Euclidean metric. Compare with rrnmval . (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 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 ) ) )

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 
 |-  ( RR^ ` I ) = ( RR^ ` I )
4 eqid 
 |-  ( Base ` ( RR^ ` I ) ) = ( Base ` ( RR^ ` I ) )
5 3 4 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 ) ) )
6 2 5 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 ) ) ) ) ) )
7 3 4 rrxbase 
 |-  ( I e. V -> ( Base ` ( RR^ ` I ) ) = { h e. ( RR ^m I ) | h finSupp 0 } )
8 1 7 eqtr4id 
 |-  ( I e. V -> X = ( Base ` ( RR^ ` I ) ) )
9 mpoeq12 
 |-  ( ( X = ( Base ` ( RR^ ` I ) ) /\ X = ( Base ` ( RR^ ` I ) ) ) -> ( f e. X , g e. X |-> ( 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 ) ) ) ) ) )
10 8 8 9 syl2anc 
 |-  ( I e. V -> ( f e. X , g e. X |-> ( 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 ) ) ) ) ) )
11 6 10 eqtr4d 
 |-  ( I e. V -> D = ( f e. X , g e. X |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) )
12 11 3ad2ant1 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> D = ( f e. X , g e. X |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) )
13 simprl 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ ( f = F /\ g = G ) ) -> f = F )
14 13 fveq1d 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ ( f = F /\ g = G ) ) -> ( f ` x ) = ( F ` x ) )
15 simprr 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ ( f = F /\ g = G ) ) -> g = G )
16 15 fveq1d 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ ( f = F /\ g = G ) ) -> ( g ` x ) = ( G ` x ) )
17 14 16 oveq12d 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ ( f = F /\ g = G ) ) -> ( ( f ` x ) - ( g ` x ) ) = ( ( F ` x ) - ( G ` x ) ) )
18 17 oveq1d 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ ( f = F /\ g = G ) ) -> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) = ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) )
19 18 mpteq2dv 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ ( f = F /\ g = G ) ) -> ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) = ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) )
20 19 oveq2d 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ ( f = F /\ g = G ) ) -> ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) = ( RRfld gsum ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) ) )
21 simp2 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> F e. X )
22 1 21 rrxf 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> F : I --> RR )
23 22 ffvelrnda 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> ( F ` x ) e. RR )
24 simp3 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> G e. X )
25 1 24 rrxf 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> G : I --> RR )
26 25 ffvelrnda 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> ( G ` x ) e. RR )
27 23 26 resubcld 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> ( ( F ` x ) - ( G ` x ) ) e. RR )
28 27 resqcld 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ x e. I ) -> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) e. RR )
29 28 fmpttd 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) : I --> RR )
30 1 21 rrxfsupp 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( F supp 0 ) e. Fin )
31 1 24 rrxfsupp 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( G supp 0 ) e. Fin )
32 unfi 
 |-  ( ( ( F supp 0 ) e. Fin /\ ( G supp 0 ) e. Fin ) -> ( ( F supp 0 ) u. ( G supp 0 ) ) e. Fin )
33 30 31 32 syl2anc 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( ( F supp 0 ) u. ( G supp 0 ) ) e. Fin )
34 1 rrxmvallem 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) ) )
35 33 34 ssfid 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) e. Fin )
36 mptexg 
 |-  ( I e. V -> ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) e. _V )
37 funmpt 
 |-  Fun ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) )
38 0cn 
 |-  0 e. CC
39 funisfsupp 
 |-  ( ( Fun ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) /\ ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) e. _V /\ 0 e. CC ) -> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) finSupp 0 <-> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) e. Fin ) )
40 37 38 39 mp3an13 
 |-  ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) e. _V -> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) finSupp 0 <-> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) e. Fin ) )
41 36 40 syl 
 |-  ( I e. V -> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) finSupp 0 <-> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) e. Fin ) )
42 41 3ad2ant1 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) finSupp 0 <-> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) e. Fin ) )
43 35 42 mpbird 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) finSupp 0 )
44 simp1 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> I e. V )
45 regsumsupp 
 |-  ( ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) : I --> RR /\ ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) finSupp 0 /\ I e. V ) -> ( RRfld gsum ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) ) = sum_ k e. ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) ` k ) )
46 29 43 44 45 syl3anc 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( RRfld gsum ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) ) = sum_ k e. ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) ` k ) )
47 suppssdm 
 |-  ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) C_ dom ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) )
48 eqid 
 |-  ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) = ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) )
49 48 dmmptss 
 |-  dom ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) C_ I
50 47 49 sstri 
 |-  ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) C_ I
51 50 a1i 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) C_ I )
52 51 sselda 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ) -> k e. I )
53 eqidd 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) -> ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) = ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) )
54 simpr 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) /\ x = k ) -> x = k )
55 54 fveq2d 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) /\ x = k ) -> ( F ` x ) = ( F ` k ) )
56 54 fveq2d 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) /\ x = k ) -> ( G ` x ) = ( G ` k ) )
57 55 56 oveq12d 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) /\ x = k ) -> ( ( F ` x ) - ( G ` x ) ) = ( ( F ` k ) - ( G ` k ) ) )
58 57 oveq1d 
 |-  ( ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) /\ x = k ) -> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) = ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
59 simpr 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) -> k e. I )
60 ovexd 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) e. _V )
61 53 58 59 60 fvmptd 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) -> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) ` k ) = ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
62 61 eqcomd 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) = ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) ` k ) )
63 52 62 syldan 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ) -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) = ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) ` k ) )
64 63 sumeq2dv 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> sum_ k e. ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) = sum_ k e. ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) ` k ) )
65 46 64 eqtr4d 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( RRfld gsum ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) ) = sum_ k e. ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
66 65 adantr 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ ( f = F /\ g = G ) ) -> ( RRfld gsum ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) ) = sum_ k e. ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
67 22 ffvelrnda 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) -> ( F ` k ) e. RR )
68 67 recnd 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) -> ( F ` k ) e. CC )
69 25 ffvelrnda 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) -> ( G ` k ) e. RR )
70 69 recnd 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) -> ( G ` k ) e. CC )
71 68 70 subcld 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) -> ( ( F ` k ) - ( G ` k ) ) e. CC )
72 71 sqcld 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. I ) -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) e. CC )
73 52 72 syldan 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ) -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) e. CC )
74 1 21 rrxsuppss 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( F supp 0 ) C_ I )
75 1 24 rrxsuppss 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( G supp 0 ) C_ I )
76 74 75 unssd 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( ( F supp 0 ) u. ( G supp 0 ) ) C_ I )
77 76 ssdifssd 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( ( ( F supp 0 ) u. ( G supp 0 ) ) \ ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ) C_ I )
78 77 sselda 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. ( ( ( F supp 0 ) u. ( G supp 0 ) ) \ ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ) ) -> k e. I )
79 78 62 syldan 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. ( ( ( F supp 0 ) u. ( G supp 0 ) ) \ ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ) ) -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) = ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) ` k ) )
80 76 ssdifd 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( ( ( F supp 0 ) u. ( G supp 0 ) ) \ ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ) C_ ( I \ ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ) )
81 80 sselda 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. ( ( ( F supp 0 ) u. ( G supp 0 ) ) \ ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ) ) -> k e. ( I \ ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ) )
82 ssidd 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) C_ ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) )
83 0cnd 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> 0 e. CC )
84 29 82 44 83 suppssr 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. ( I \ ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ) ) -> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) ` k ) = 0 )
85 81 84 syldan 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. ( ( ( F supp 0 ) u. ( G supp 0 ) ) \ ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ) ) -> ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) ` k ) = 0 )
86 79 85 eqtrd 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ k e. ( ( ( F supp 0 ) u. ( G supp 0 ) ) \ ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ) ) -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) = 0 )
87 34 73 86 33 fsumss 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> sum_ k e. ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) = sum_ k e. ( ( F supp 0 ) u. ( G supp 0 ) ) ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
88 87 adantr 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ ( f = F /\ g = G ) ) -> sum_ k e. ( ( x e. I |-> ( ( ( F ` x ) - ( G ` x ) ) ^ 2 ) ) supp 0 ) ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) = sum_ k e. ( ( F supp 0 ) u. ( G supp 0 ) ) ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
89 20 66 88 3eqtrd 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ ( f = F /\ g = G ) ) -> ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) = sum_ k e. ( ( F supp 0 ) u. ( G supp 0 ) ) ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
90 89 fveq2d 
 |-  ( ( ( I e. V /\ F e. X /\ G e. X ) /\ ( f = F /\ g = G ) ) -> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) = ( sqrt ` sum_ k e. ( ( F supp 0 ) u. ( G supp 0 ) ) ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
91 fvexd 
 |-  ( ( I e. V /\ F e. X /\ G e. X ) -> ( sqrt ` sum_ k e. ( ( F supp 0 ) u. ( G supp 0 ) ) ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) e. _V )
92 12 90 21 24 91 ovmpod 
 |-  ( ( 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 ) ) )