# 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}=\left\{{h}\in \left({ℝ}^{{I}}\right)|{finSupp}_{0}\left({h}\right)\right\}$
rrxmval.d ${⊢}{D}=\mathrm{dist}\left({{I}}^{}\right)$
Assertion rrxmval ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {F}{D}{G}=\sqrt{\sum _{{k}\in {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)}{\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}}$

### Proof

Step Hyp Ref Expression
1 rrxmval.1 ${⊢}{X}=\left\{{h}\in \left({ℝ}^{{I}}\right)|{finSupp}_{0}\left({h}\right)\right\}$
2 rrxmval.d ${⊢}{D}=\mathrm{dist}\left({{I}}^{}\right)$
3 eqid ${⊢}{{I}}^{}={{I}}^{}$
4 eqid ${⊢}{\mathrm{Base}}_{{{I}}^{}}={\mathrm{Base}}_{{{I}}^{}}$
5 3 4 rrxds ${⊢}{I}\in {V}\to \left({f}\in {\mathrm{Base}}_{{{I}}^{}},{g}\in {\mathrm{Base}}_{{{I}}^{}}⟼\sqrt{\underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({f}\left({x}\right)-{g}\left({x}\right)\right)}^{2}}\right)=\mathrm{dist}\left({{I}}^{}\right)$
6 5 2 syl6reqr ${⊢}{I}\in {V}\to {D}=\left({f}\in {\mathrm{Base}}_{{{I}}^{}},{g}\in {\mathrm{Base}}_{{{I}}^{}}⟼\sqrt{\underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({f}\left({x}\right)-{g}\left({x}\right)\right)}^{2}}\right)$
7 3 4 rrxbase ${⊢}{I}\in {V}\to {\mathrm{Base}}_{{{I}}^{}}=\left\{{h}\in \left({ℝ}^{{I}}\right)|{finSupp}_{0}\left({h}\right)\right\}$
8 7 1 syl6reqr ${⊢}{I}\in {V}\to {X}={\mathrm{Base}}_{{{I}}^{}}$
9 mpoeq12 ${⊢}\left({X}={\mathrm{Base}}_{{{I}}^{}}\wedge {X}={\mathrm{Base}}_{{{I}}^{}}\right)\to \left({f}\in {X},{g}\in {X}⟼\sqrt{\underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({f}\left({x}\right)-{g}\left({x}\right)\right)}^{2}}\right)=\left({f}\in {\mathrm{Base}}_{{{I}}^{}},{g}\in {\mathrm{Base}}_{{{I}}^{}}⟼\sqrt{\underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({f}\left({x}\right)-{g}\left({x}\right)\right)}^{2}}\right)$
10 8 8 9 syl2anc ${⊢}{I}\in {V}\to \left({f}\in {X},{g}\in {X}⟼\sqrt{\underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({f}\left({x}\right)-{g}\left({x}\right)\right)}^{2}}\right)=\left({f}\in {\mathrm{Base}}_{{{I}}^{}},{g}\in {\mathrm{Base}}_{{{I}}^{}}⟼\sqrt{\underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({f}\left({x}\right)-{g}\left({x}\right)\right)}^{2}}\right)$
11 6 10 eqtr4d ${⊢}{I}\in {V}\to {D}=\left({f}\in {X},{g}\in {X}⟼\sqrt{\underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({f}\left({x}\right)-{g}\left({x}\right)\right)}^{2}}\right)$
12 11 3ad2ant1 ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {D}=\left({f}\in {X},{g}\in {X}⟼\sqrt{\underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({f}\left({x}\right)-{g}\left({x}\right)\right)}^{2}}\right)$
13 simprl ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge \left({f}={F}\wedge {g}={G}\right)\right)\to {f}={F}$
14 13 fveq1d ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge \left({f}={F}\wedge {g}={G}\right)\right)\to {f}\left({x}\right)={F}\left({x}\right)$
15 simprr ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge \left({f}={F}\wedge {g}={G}\right)\right)\to {g}={G}$
16 15 fveq1d ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge \left({f}={F}\wedge {g}={G}\right)\right)\to {g}\left({x}\right)={G}\left({x}\right)$
17 14 16 oveq12d ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge \left({f}={F}\wedge {g}={G}\right)\right)\to {f}\left({x}\right)-{g}\left({x}\right)={F}\left({x}\right)-{G}\left({x}\right)$
18 17 oveq1d ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge \left({f}={F}\wedge {g}={G}\right)\right)\to {\left({f}\left({x}\right)-{g}\left({x}\right)\right)}^{2}={\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}$
19 18 mpteq2dv ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge \left({f}={F}\wedge {g}={G}\right)\right)\to \left({x}\in {I}⟼{\left({f}\left({x}\right)-{g}\left({x}\right)\right)}^{2}\right)=\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)$
20 19 oveq2d ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge \left({f}={F}\wedge {g}={G}\right)\right)\to \underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({f}\left({x}\right)-{g}\left({x}\right)\right)}^{2}=\underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}$
21 simp2 ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {F}\in {X}$
22 1 21 rrxf ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {F}:{I}⟶ℝ$
23 22 ffvelrnda ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {x}\in {I}\right)\to {F}\left({x}\right)\in ℝ$
24 simp3 ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {G}\in {X}$
25 1 24 rrxf ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {G}:{I}⟶ℝ$
26 25 ffvelrnda ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {x}\in {I}\right)\to {G}\left({x}\right)\in ℝ$
27 23 26 resubcld ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {x}\in {I}\right)\to {F}\left({x}\right)-{G}\left({x}\right)\in ℝ$
28 27 resqcld ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {x}\in {I}\right)\to {\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\in ℝ$
29 28 fmpttd ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right):{I}⟶ℝ$
30 1 21 rrxfsupp ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {F}\mathrm{supp}0\in \mathrm{Fin}$
31 1 24 rrxfsupp ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {G}\mathrm{supp}0\in \mathrm{Fin}$
32 unfi ${⊢}\left({F}\mathrm{supp}0\in \mathrm{Fin}\wedge {G}\mathrm{supp}0\in \mathrm{Fin}\right)\to {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\in \mathrm{Fin}$
33 30 31 32 syl2anc ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\in \mathrm{Fin}$
34 1 rrxmvallem ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0\subseteq {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)$
35 33 34 ssfid ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0\in \mathrm{Fin}$
36 mptexg ${⊢}{I}\in {V}\to \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\in \mathrm{V}$
37 funmpt ${⊢}\mathrm{Fun}\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)$
38 0cn ${⊢}0\in ℂ$
39 funisfsupp ${⊢}\left(\mathrm{Fun}\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\wedge \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\in \mathrm{V}\wedge 0\in ℂ\right)\to \left({finSupp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)↔\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0\in \mathrm{Fin}\right)$
40 37 38 39 mp3an13 ${⊢}\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\in \mathrm{V}\to \left({finSupp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)↔\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0\in \mathrm{Fin}\right)$
41 36 40 syl ${⊢}{I}\in {V}\to \left({finSupp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)↔\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0\in \mathrm{Fin}\right)$
42 41 3ad2ant1 ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to \left({finSupp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)↔\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0\in \mathrm{Fin}\right)$
43 35 42 mpbird ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {finSupp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)$
44 simp1 ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {I}\in {V}$
45 regsumsupp ${⊢}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right):{I}⟶ℝ\wedge {finSupp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)\wedge {I}\in {V}\right)\to \underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}=\sum _{{k}\in \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0}\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\left({k}\right)$
46 29 43 44 45 syl3anc ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to \underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}=\sum _{{k}\in \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0}\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\left({k}\right)$
47 suppssdm ${⊢}\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0\subseteq \mathrm{dom}\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)$
48 eqid ${⊢}\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)=\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)$
49 48 dmmptss ${⊢}\mathrm{dom}\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\subseteq {I}$
50 47 49 sstri ${⊢}\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0\subseteq {I}$
51 50 a1i ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0\subseteq {I}$
52 51 sselda ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {supp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)\right)\to {k}\in {I}$
53 eqidd ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\to \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)=\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)$
54 simpr ${⊢}\left(\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\wedge {x}={k}\right)\to {x}={k}$
55 54 fveq2d ${⊢}\left(\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\wedge {x}={k}\right)\to {F}\left({x}\right)={F}\left({k}\right)$
56 54 fveq2d ${⊢}\left(\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\wedge {x}={k}\right)\to {G}\left({x}\right)={G}\left({k}\right)$
57 55 56 oveq12d ${⊢}\left(\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\wedge {x}={k}\right)\to {F}\left({x}\right)-{G}\left({x}\right)={F}\left({k}\right)-{G}\left({k}\right)$
58 57 oveq1d ${⊢}\left(\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\wedge {x}={k}\right)\to {\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}={\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}$
59 simpr ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\to {k}\in {I}$
60 ovexd ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\to {\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}\in \mathrm{V}$
61 53 58 59 60 fvmptd ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\to \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\left({k}\right)={\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}$
62 61 eqcomd ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\to {\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}=\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\left({k}\right)$
63 52 62 syldan ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {supp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)\right)\to {\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}=\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\left({k}\right)$
64 63 sumeq2dv ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to \sum _{{k}\in \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0}{\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}=\sum _{{k}\in \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0}\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\left({k}\right)$
65 46 64 eqtr4d ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to \underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}=\sum _{{k}\in \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0}{\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}$
66 65 adantr ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge \left({f}={F}\wedge {g}={G}\right)\right)\to \underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}=\sum _{{k}\in \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0}{\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}$
67 22 ffvelrnda ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\to {F}\left({k}\right)\in ℝ$
68 67 recnd ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\to {F}\left({k}\right)\in ℂ$
69 25 ffvelrnda ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\to {G}\left({k}\right)\in ℝ$
70 69 recnd ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\to {G}\left({k}\right)\in ℂ$
71 68 70 subcld ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\to {F}\left({k}\right)-{G}\left({k}\right)\in ℂ$
72 71 sqcld ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {I}\right)\to {\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}\in ℂ$
73 52 72 syldan ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in {supp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)\right)\to {\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}\in ℂ$
74 1 21 rrxsuppss ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {F}\mathrm{supp}0\subseteq {I}$
75 1 24 rrxsuppss ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {G}\mathrm{supp}0\subseteq {I}$
76 74 75 unssd ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\subseteq {I}$
77 76 ssdifssd ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\setminus {supp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)\subseteq {I}$
78 77 sselda ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in \left(\left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\setminus {supp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)\right)\right)\to {k}\in {I}$
79 78 62 syldan ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in \left(\left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\setminus {supp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)\right)\right)\to {\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}=\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\left({k}\right)$
80 76 ssdifd ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\setminus {supp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)\subseteq {I}\setminus {supp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)$
81 80 sselda ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in \left(\left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\setminus {supp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)\right)\right)\to {k}\in \left({I}\setminus {supp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)\right)$
82 ssidd ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0\subseteq \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0$
83 0cnd ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to 0\in ℂ$
84 29 82 44 83 suppssr ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in \left({I}\setminus {supp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)\right)\right)\to \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\left({k}\right)=0$
85 81 84 syldan ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in \left(\left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\setminus {supp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)\right)\right)\to \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\left({k}\right)=0$
86 79 85 eqtrd ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge {k}\in \left(\left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\setminus {supp}_{0}\left(\left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\right)\right)\right)\to {\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}=0$
87 34 73 86 33 fsumss ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to \sum _{{k}\in \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0}{\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}=\sum _{{k}\in {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)}{\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}$
88 87 adantr ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge \left({f}={F}\wedge {g}={G}\right)\right)\to \sum _{{k}\in \left({x}\in {I}⟼{\left({F}\left({x}\right)-{G}\left({x}\right)\right)}^{2}\right)\mathrm{supp}0}{\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}=\sum _{{k}\in {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)}{\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}$
89 20 66 88 3eqtrd ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge \left({f}={F}\wedge {g}={G}\right)\right)\to \underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({f}\left({x}\right)-{g}\left({x}\right)\right)}^{2}=\sum _{{k}\in {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)}{\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}$
90 89 fveq2d ${⊢}\left(\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\wedge \left({f}={F}\wedge {g}={G}\right)\right)\to \sqrt{\underset{{x}\in {I}}{{\sum }_{{ℝ}_{\mathrm{fld}}}}{\left({f}\left({x}\right)-{g}\left({x}\right)\right)}^{2}}=\sqrt{\sum _{{k}\in {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)}{\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}}$
91 fvexd ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to \sqrt{\sum _{{k}\in {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)}{\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}}\in \mathrm{V}$
92 12 90 21 24 91 ovmpod ${⊢}\left({I}\in {V}\wedge {F}\in {X}\wedge {G}\in {X}\right)\to {F}{D}{G}=\sqrt{\sum _{{k}\in {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)}{\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}}$