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		difexg	$$⊢B\in W\to B\setminus A\in \mathrm{V}$$
11	2 10	syl	$$⊢\phi \to B\setminus A\in \mathrm{V}$$
12		disjdif	$$⊢A\cap \left(B\setminus A\right)=\varnothing$$
13	12	a1i	$$⊢\phi \to A\cap \left(B\setminus A\right)=\varnothing$$
14		difssd	$$⊢\phi \to B\setminus A\subseteq B$$
15	14	sselda	$$⊢\left(\phi \wedge k\in \left(B\setminus A\right)\right)\to k\in B$$
16		0e0iccpnf	$$⊢0\in \left[0,\mathrm{+\infty }\right]$$
17	4 16	eqeltrdi	$$⊢\left(\phi \wedge k\in B\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
18	15 17	syldan	$$⊢\left(\phi \wedge k\in \left(B\setminus A\right)\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
19	5 6 7 9 11 13 3 18	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$$
20		undif2	$$⊢A\cup \left(B\setminus A\right)=A\cup B$$
21		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$$
22	20 21	ax-mp	$$⊢\underset{k\in A\cup \left(B\setminus A\right)}{{\sum }^{*}}C=\underset{k\in A\cup B}{{\sum }^{*}}C$$
23	22	a1i	$$⊢\phi \to \underset{k\in A\cup \left(B\setminus A\right)}{{\sum }^{*}}C=\underset{k\in A\cup B}{{\sum }^{*}}C$$
24	15 4	syldan	$$⊢\left(\phi \wedge k\in \left(B\setminus A\right)\right)\to C=0$$
25	24	ralrimiva	$$⊢\phi \to \forall k\in \left(B\setminus A\right)C=0$$
26	5 25	esumeq2d	$$⊢\phi \to \underset{k\in B\setminus A}{{\sum }^{*}}C=\underset{k\in B\setminus A}{{\sum }^{*}}0$$
27	7	esum0	$$⊢B\setminus A\in \mathrm{V}\to \underset{k\in B\setminus A}{{\sum }^{*}}0=0$$
28	11 27	syl	$$⊢\phi \to \underset{k\in B\setminus A}{{\sum }^{*}}0=0$$
29	26 28	eqtrd	$$⊢\phi \to \underset{k\in B\setminus A}{{\sum }^{*}}C=0$$
30	29	oveq2d	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C{+}_{𝑒}\underset{k\in B\setminus A}{{\sum }^{*}}C=\underset{k\in A}{{\sum }^{*}}C{+}_{𝑒}0$$
31		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
32	3	ralrimiva	$$⊢\phi \to \forall k\in AC\in \left[0,\mathrm{+\infty }\right]$$
33	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]$$
34	1 32 33	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C\in \left[0,\mathrm{+\infty }\right]$$
35	31 34	sseldi	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C\in {ℝ}^{*}$$
36		xaddid1	$$⊢\underset{k\in A}{{\sum }^{*}}C\in {ℝ}^{*}\to \underset{k\in A}{{\sum }^{*}}C{+}_{𝑒}0=\underset{k\in A}{{\sum }^{*}}C$$
37	35 36	syl	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C{+}_{𝑒}0=\underset{k\in A}{{\sum }^{*}}C$$
38	30 37	eqtrd	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}C{+}_{𝑒}\underset{k\in B\setminus A}{{\sum }^{*}}C=\underset{k\in A}{{\sum }^{*}}C$$
39	19 23 38	3eqtr3d	$$⊢\phi \to \underset{k\in A\cup B}{{\sum }^{*}}C=\underset{k\in A}{{\sum }^{*}}C$$