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
	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
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$$