# Metamath Proof Explorer

## Theorem rrxmetlem

Description: Lemma for rrxmet . (Contributed by Thierry Arnoux, 5-Jul-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)$
rrxmetlem.1 ${⊢}{\phi }\to {I}\in {V}$
rrxmetlem.2 ${⊢}{\phi }\to {F}\in {X}$
rrxmetlem.3 ${⊢}{\phi }\to {G}\in {X}$
rrxmetlem.4 ${⊢}{\phi }\to {A}\subseteq {I}$
rrxmetlem.5 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
rrxmetlem.6 ${⊢}{\phi }\to {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\subseteq {A}$
Assertion rrxmetlem ${⊢}{\phi }\to \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}=\sum _{{k}\in {A}}{\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 rrxmetlem.1 ${⊢}{\phi }\to {I}\in {V}$
4 rrxmetlem.2 ${⊢}{\phi }\to {F}\in {X}$
5 rrxmetlem.3 ${⊢}{\phi }\to {G}\in {X}$
6 rrxmetlem.4 ${⊢}{\phi }\to {A}\subseteq {I}$
7 rrxmetlem.5 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
8 rrxmetlem.6 ${⊢}{\phi }\to {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\subseteq {A}$
9 8 6 sstrd ${⊢}{\phi }\to {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\subseteq {I}$
10 9 sselda ${⊢}\left({\phi }\wedge {k}\in \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\to {k}\in {I}$
11 1 4 rrxf ${⊢}{\phi }\to {F}:{I}⟶ℝ$
12 11 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in {I}\right)\to {F}\left({k}\right)\in ℝ$
13 12 recnd ${⊢}\left({\phi }\wedge {k}\in {I}\right)\to {F}\left({k}\right)\in ℂ$
14 10 13 syldan ${⊢}\left({\phi }\wedge {k}\in \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\to {F}\left({k}\right)\in ℂ$
15 1 5 rrxf ${⊢}{\phi }\to {G}:{I}⟶ℝ$
16 15 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in {I}\right)\to {G}\left({k}\right)\in ℝ$
17 16 recnd ${⊢}\left({\phi }\wedge {k}\in {I}\right)\to {G}\left({k}\right)\in ℂ$
18 10 17 syldan ${⊢}\left({\phi }\wedge {k}\in \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\to {G}\left({k}\right)\in ℂ$
19 14 18 subcld ${⊢}\left({\phi }\wedge {k}\in \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\to {F}\left({k}\right)-{G}\left({k}\right)\in ℂ$
20 19 sqcld ${⊢}\left({\phi }\wedge {k}\in \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\to {\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}\in ℂ$
21 6 ssdifd ${⊢}{\phi }\to {A}\setminus \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\subseteq {I}\setminus \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)$
22 21 sselda ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\right)\to {k}\in \left({I}\setminus \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)$
23 simpr ${⊢}\left({\phi }\wedge {k}\in \left({I}\setminus \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\right)\to {k}\in \left({I}\setminus \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)$
24 23 eldifad ${⊢}\left({\phi }\wedge {k}\in \left({I}\setminus \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\right)\to {k}\in {I}$
25 24 13 syldan ${⊢}\left({\phi }\wedge {k}\in \left({I}\setminus \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\right)\to {F}\left({k}\right)\in ℂ$
26 ssun1 ${⊢}{F}\mathrm{supp}0\subseteq {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)$
27 26 a1i ${⊢}{\phi }\to {F}\mathrm{supp}0\subseteq {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)$
28 0red ${⊢}{\phi }\to 0\in ℝ$
29 11 27 3 28 suppssr ${⊢}\left({\phi }\wedge {k}\in \left({I}\setminus \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\right)\to {F}\left({k}\right)=0$
30 ssun2 ${⊢}{G}\mathrm{supp}0\subseteq {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)$
31 30 a1i ${⊢}{\phi }\to {G}\mathrm{supp}0\subseteq {supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)$
32 15 31 3 28 suppssr ${⊢}\left({\phi }\wedge {k}\in \left({I}\setminus \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\right)\to {G}\left({k}\right)=0$
33 29 32 eqtr4d ${⊢}\left({\phi }\wedge {k}\in \left({I}\setminus \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\right)\to {F}\left({k}\right)={G}\left({k}\right)$
34 25 33 subeq0bd ${⊢}\left({\phi }\wedge {k}\in \left({I}\setminus \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\right)\to {F}\left({k}\right)-{G}\left({k}\right)=0$
35 34 sq0id ${⊢}\left({\phi }\wedge {k}\in \left({I}\setminus \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\right)\to {\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}=0$
36 22 35 syldan ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus \left({supp}_{0}\left({F}\right)\cup {supp}_{0}\left({G}\right)\right)\right)\right)\to {\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}=0$
37 8 20 36 7 fsumss ${⊢}{\phi }\to \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}=\sum _{{k}\in {A}}{\left({F}\left({k}\right)-{G}\left({k}\right)\right)}^{2}$