Theorem fsumsupp0

Description: Finite sum of function values, for a function of finite support. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	fsumsupp0.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumsupp0.f	$$⊢\phi \to F:A⟶ℂ$$
Assertion	fsumsupp0	$$⊢\phi \to \sum _{k\in F\mathrm{supp}0}F\left(k\right)=\sum _{k\in A}F\left(k\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsumsupp0.a	$$⊢\phi \to A\in \mathrm{Fin}$$
2		fsumsupp0.f	$$⊢\phi \to F:A⟶ℂ$$
3	2	ffnd	$$⊢\phi \to FFnA$$
4		0red	$$⊢\phi \to 0\in ℝ$$
5		suppvalfn	$$⊢\left(FFnA\wedge A\in \mathrm{Fin}\wedge 0\in ℝ\right)\to F\mathrm{supp}0=\left\{k\in A|F\left(k\right)\ne 0\right\}$$
6	3 1 4 5	syl3anc	$$⊢\phi \to F\mathrm{supp}0=\left\{k\in A|F\left(k\right)\ne 0\right\}$$
7		ssrab2	$$⊢\left\{k\in A|F\left(k\right)\ne 0\right\}\subseteq A$$
8	6 7	eqsstrdi	$$⊢\phi \to F\mathrm{supp}0\subseteq A$$
9	2	adantr	$$⊢\left(\phi \wedge k\in {supp}_0\left(F\right)\right)\to F:A⟶ℂ$$
10	8	sselda	$$⊢\left(\phi \wedge k\in {supp}_0\left(F\right)\right)\to k\in A$$
11	9 10	ffvelrnd	$$⊢\left(\phi \wedge k\in {supp}_0\left(F\right)\right)\to F\left(k\right)\in ℂ$$
12		eldifi	$$⊢k\in \left(A\setminus {supp}_0\left(F\right)\right)\to k\in A$$
13	12	adantr	$$⊢\left(k\in \left(A\setminus {supp}_0\left(F\right)\right)\wedge \neg F\left(k\right)=0\right)\to k\in A$$
14		neqne	$$⊢\neg F\left(k\right)=0\to F\left(k\right)\ne 0$$
15	14	adantl	$$⊢\left(k\in \left(A\setminus {supp}_0\left(F\right)\right)\wedge \neg F\left(k\right)=0\right)\to F\left(k\right)\ne 0$$
16	13 15	jca	$$⊢\left(k\in \left(A\setminus {supp}_0\left(F\right)\right)\wedge \neg F\left(k\right)=0\right)\to \left(k\in A\wedge F\left(k\right)\ne 0\right)$$
17		rabid	$$⊢k\in \left\{k\in A|F\left(k\right)\ne 0\right\}\leftrightarrow \left(k\in A\wedge F\left(k\right)\ne 0\right)$$
18	16 17	sylibr	$$⊢\left(k\in \left(A\setminus {supp}_0\left(F\right)\right)\wedge \neg F\left(k\right)=0\right)\to k\in \left\{k\in A|F\left(k\right)\ne 0\right\}$$
19	18	adantll	$$⊢\left(\left(\phi \wedge k\in \left(A\setminus {supp}_0\left(F\right)\right)\right)\wedge \neg F\left(k\right)=0\right)\to k\in \left\{k\in A|F\left(k\right)\ne 0\right\}$$
20	6	eleq2d	$$⊢\phi \to \left(k\in {supp}_0\left(F\right)\leftrightarrow k\in \left\{k\in A|F\left(k\right)\ne 0\right\}\right)$$
21	20	ad2antrr	$$⊢\left(\left(\phi \wedge k\in \left(A\setminus {supp}_0\left(F\right)\right)\right)\wedge \neg F\left(k\right)=0\right)\to \left(k\in {supp}_0\left(F\right)\leftrightarrow k\in \left\{k\in A|F\left(k\right)\ne 0\right\}\right)$$
22	19 21	mpbird	$$⊢\left(\left(\phi \wedge k\in \left(A\setminus {supp}_0\left(F\right)\right)\right)\wedge \neg F\left(k\right)=0\right)\to k\in {supp}_0\left(F\right)$$
23		eldifn	$$⊢k\in \left(A\setminus {supp}_0\left(F\right)\right)\to \neg k\in {supp}_0\left(F\right)$$
24	23	ad2antlr	$$⊢\left(\left(\phi \wedge k\in \left(A\setminus {supp}_0\left(F\right)\right)\right)\wedge \neg F\left(k\right)=0\right)\to \neg k\in {supp}_0\left(F\right)$$
25	22 24	condan	$$⊢\left(\phi \wedge k\in \left(A\setminus {supp}_0\left(F\right)\right)\right)\to F\left(k\right)=0$$
26	8 11 25 1	fsumss	$$⊢\phi \to \sum _{k\in F\mathrm{supp}0}F\left(k\right)=\sum _{k\in A}F\left(k\right)$$