Theorem esumpad

Description: Extend an extended sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 31-May-2020)

	Ref	Expression
Hypotheses	esumpad.1	$$⊢\phi \to A\in V$$
	esumpad.2	$$⊢\phi \to B\in W$$
	esumpad.3	$$⊢\left(\phi \wedge k\in A\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
	esumpad.4	$$⊢\left(\phi \wedge k\in B\right)\to C=0$$
Assertion	esumpad	$$⊢\phi \to \underset{k\in A\cup B}{{\sum }^{*}}C=\underset{k\in A}{{\sum }^{*}}C$$

Proof

Step	Hyp	Ref	Expression
1		esumpad.1	$$⊢\phi \to A\in V$$
2		esumpad.2	$$⊢\phi \to B\in W$$
3		esumpad.3	$$⊢\left(\phi \wedge k\in A\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
4		esumpad.4	$$⊢\left(\phi \wedge k\in B\right)\to C=0$$
5		nfv	$$⊢Ⅎk\phi$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}k\left(B\setminus A\right)$$
8		elex	$$⊢A\in V\to A\in \mathrm{V}$$
9	1 8	syl	$$⊢\phi \to A\in \mathrm{V}$$
10	2	difexd	$$⊢\phi \to B\setminus A\in \mathrm{V}$$
11		disjdif	$$⊢A\cap \left(B\setminus A\right)=\varnothing$$
12	11	a1i	$$⊢\phi \to A\cap \left(B\setminus A\right)=\varnothing$$
13		difssd	$$⊢\phi \to B\setminus A\subseteq B$$
14	13	sselda	$$⊢\left(\phi \wedge k\in \left(B\setminus A\right)\right)\to k\in B$$
15		0e0iccpnf	$$⊢0\in \left[0,\mathrm{+\infty }\right]$$
16	4 15	eqeltrdi	$$⊢\left(\phi \wedge k\in B\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
17	14 16	syldan	$$⊢\left(\phi \wedge k\in \left(B\setminus A\right)\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
18	5 6 7 9 10 12 3 17	esumsplit	$$⊢\phi \to \underset{k\in A\cup \left(B\setminus A\right)}{{\sum }^{*}}C=\underset{k\in A}{{\sum }^{*}}C{+}_{𝑒}\underset{k\in B\setminus A}{{\sum }^{*}}C$$
19		undif2	$$⊢A\cup \left(B\setminus A\right)=A\cup B$$
20		esumeq1	$$⊢A\cup \left(B\setminus A\right)=A\cup B\to \underset{k\in A\cup \left(B\setminus A\right)}{{\sum }^{*}}C=\underset{k\in A\cup B}{{\sum }^{*}}C$$
21	19 20	ax-mp	$$⊢\underset{k\in A\cup \left(B\setminus A\right)}{{\sum }^{*}}C=\underset{k\in A\cup B}{{\sum }^{*}}C$$
22	21	a1i	$$⊢\phi \to \underset{k\in A\cup \left(B\setminus A\right)}{{\sum }^{*}}C=\underset{k\in A\cup B}{{\sum }^{*}}C$$
23	14 4	syldan	$$⊢\left(\phi \wedge k\in \left(B\setminus A\right)\right)\to C=0$$
24	23	ralrimiva	$$⊢\phi \to \forall k\in \left(B\setminus A\right)C=0$$
25	5 24	esumeq2d	$$⊢\phi \to \underset{k\in B\setminus A}{{\sum }^{*}}C=\underset{k\in B\setminus A}{{\sum }^{*}}0$$
26	7	esum0	$$⊢B\setminus A\in \mathrm{V}\to \underset{k\in B\setminus A}{{\sum }^{*}}0=0$$
27	10 26	syl	$$⊢\phi \to \underset{k\in B\setminus A}{{\sum }^{*}}0=0$$
28	25 27	eqtrd	$$⊢\phi \to \underset{k\in B\setminus A}{{\sum }^{*}}C=0$$
29	28	oveq2d	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C{+}_{𝑒}\underset{k\in B\setminus A}{{\sum }^{*}}C=\underset{k\in A}{{\sum }^{*}}C{+}_{𝑒}0$$
30		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
31	3	ralrimiva	$$⊢\phi \to \forall k\in AC\in \left[0,\mathrm{+\infty }\right]$$
32	6	esumcl	$$⊢\left(A\in V\wedge \forall k\in AC\in \left[0,\mathrm{+\infty }\right]\right)\to \underset{k\in A}{{\sum }^{*}}C\in \left[0,\mathrm{+\infty }\right]$$
33	1 31 32	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C\in \left[0,\mathrm{+\infty }\right]$$
34	30 33	sselid	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C\in {ℝ}^{*}$$
35		xaddid1	$$⊢\underset{k\in A}{{\sum }^{*}}C\in {ℝ}^{*}\to \underset{k\in A}{{\sum }^{*}}C{+}_{𝑒}0=\underset{k\in A}{{\sum }^{*}}C$$
36	34 35	syl	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C{+}_{𝑒}0=\underset{k\in A}{{\sum }^{*}}C$$
37	29 36	eqtrd	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C{+}_{𝑒}\underset{k\in B\setminus A}{{\sum }^{*}}C=\underset{k\in A}{{\sum }^{*}}C$$
38	18 22 37	3eqtr3d	$$⊢\phi \to \underset{k\in A\cup B}{{\sum }^{*}}C=\underset{k\in A}{{\sum }^{*}}C$$