Theorem fsumiun

Description: Sum over a disjoint indexed union. (Contributed by Mario Carneiro, 1-Jul-2015) (Revised by Mario Carneiro, 10-Dec-2016)

	Ref	Expression
Hypotheses	fsumiun.1	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumiun.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in \mathrm{Fin}$$
	fsumiun.3	$$⊢\phi \to \underset{x\in A}{Disj}B$$
	fsumiun.4	$$⊢\left(\phi \wedge \left(x\in A\wedge k\in B\right)\right)\to C\in ℂ$$
Assertion	fsumiun	$$⊢\phi \to \sum _{k\in \bigcup _{x\in A}B}C=\sum _{x\in A}\sum _{k\in B}C$$

Proof

Step	Hyp	Ref	Expression
1		fsumiun.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		fsumiun.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in \mathrm{Fin}$$
3		fsumiun.3	$$⊢\phi \to \underset{x\in A}{Disj}B$$
4		fsumiun.4	$$⊢\left(\phi \wedge \left(x\in A\wedge k\in B\right)\right)\to C\in ℂ$$
5		ssid	$$⊢A\subseteq A$$
6		sseq1	$$⊢u=\varnothing \to \left(u\subseteq A\leftrightarrow \varnothing \subseteq A\right)$$
7		iuneq1	$$⊢u=\varnothing \to \bigcup _{x\in u}B=\bigcup _{x\in \varnothing }B$$
8		0iun	$$⊢\bigcup _{x\in \varnothing }B=\varnothing$$
9	7 8	eqtrdi	$$⊢u=\varnothing \to \bigcup _{x\in u}B=\varnothing$$
10	9	sumeq1d	$$⊢u=\varnothing \to \sum _{k\in \bigcup _{x\in u}B}C=\sum _{k\in \varnothing }C$$
11		sumeq1	$$⊢u=\varnothing \to \sum _{x\in u}\sum _{k\in B}C=\sum _{x\in \varnothing }\sum _{k\in B}C$$
12	10 11	eqeq12d	$$⊢u=\varnothing \to \left(\sum _{k\in \bigcup _{x\in u}B}C=\sum _{x\in u}\sum _{k\in B}C\leftrightarrow \sum _{k\in \varnothing }C=\sum _{x\in \varnothing }\sum _{k\in B}C\right)$$
13	6 12	imbi12d	$$⊢u=\varnothing \to \left(\left(u\subseteq A\to \sum _{k\in \bigcup _{x\in u}B}C=\sum _{x\in u}\sum _{k\in B}C\right)\leftrightarrow \left(\varnothing \subseteq A\to \sum _{k\in \varnothing }C=\sum _{x\in \varnothing }\sum _{k\in B}C\right)\right)$$
14	13	imbi2d	$$⊢u=\varnothing \to \left(\left(\phi \to \left(u\subseteq A\to \sum _{k\in \bigcup _{x\in u}B}C=\sum _{x\in u}\sum _{k\in B}C\right)\right)\leftrightarrow \left(\phi \to \left(\varnothing \subseteq A\to \sum _{k\in \varnothing }C=\sum _{x\in \varnothing }\sum _{k\in B}C\right)\right)\right)$$
15		sseq1	$$⊢u=z\to \left(u\subseteq A\leftrightarrow z\subseteq A\right)$$
16		iuneq1	$$⊢u=z\to \bigcup _{x\in u}B=\bigcup _{x\in z}B$$
17	16	sumeq1d	$$⊢u=z\to \sum _{k\in \bigcup _{x\in u}B}C=\sum _{k\in \bigcup _{x\in z}B}C$$
18		sumeq1	$$⊢u=z\to \sum _{x\in u}\sum _{k\in B}C=\sum _{x\in z}\sum _{k\in B}C$$
19	17 18	eqeq12d	$$⊢u=z\to \left(\sum _{k\in \bigcup _{x\in u}B}C=\sum _{x\in u}\sum _{k\in B}C\leftrightarrow \sum _{k\in \bigcup _{x\in z}B}C=\sum _{x\in z}\sum _{k\in B}C\right)$$
20	15 19	imbi12d	$$⊢u=z\to \left(\left(u\subseteq A\to \sum _{k\in \bigcup _{x\in u}B}C=\sum _{x\in u}\sum _{k\in B}C\right)\leftrightarrow \left(z\subseteq A\to \sum _{k\in \bigcup _{x\in z}B}C=\sum _{x\in z}\sum _{k\in B}C\right)\right)$$
21	20	imbi2d	$$⊢u=z\to \left(\left(\phi \to \left(u\subseteq A\to \sum _{k\in \bigcup _{x\in u}B}C=\sum _{x\in u}\sum _{k\in B}C\right)\right)\leftrightarrow \left(\phi \to \left(z\subseteq A\to \sum _{k\in \bigcup _{x\in z}B}C=\sum _{x\in z}\sum _{k\in B}C\right)\right)\right)$$
22		sseq1	$$⊢u=z\cup \left\{w\right\}\to \left(u\subseteq A\leftrightarrow z\cup \left\{w\right\}\subseteq A\right)$$
23		iuneq1	$$⊢u=z\cup \left\{w\right\}\to \bigcup _{x\in u}B=\bigcup _{x\in z\cup \left\{w\right\}}B$$
24	23	sumeq1d	$$⊢u=z\cup \left\{w\right\}\to \sum _{k\in \bigcup _{x\in u}B}C=\sum _{k\in \bigcup _{x\in z\cup \left\{w\right\}}B}C$$
25		sumeq1	$$⊢u=z\cup \left\{w\right\}\to \sum _{x\in u}\sum _{k\in B}C=\sum _{x\in z\cup \left\{w\right\}}\sum _{k\in B}C$$
26	24 25	eqeq12d	$$⊢u=z\cup \left\{w\right\}\to \left(\sum _{k\in \bigcup _{x\in u}B}C=\sum _{x\in u}\sum _{k\in B}C\leftrightarrow \sum _{k\in \bigcup _{x\in z\cup \left\{w\right\}}B}C=\sum _{x\in z\cup \left\{w\right\}}\sum _{k\in B}C\right)$$
27	22 26	imbi12d	$$⊢u=z\cup \left\{w\right\}\to \left(\left(u\subseteq A\to \sum _{k\in \bigcup _{x\in u}B}C=\sum _{x\in u}\sum _{k\in B}C\right)\leftrightarrow \left(z\cup \left\{w\right\}\subseteq A\to \sum _{k\in \bigcup _{x\in z\cup \left\{w\right\}}B}C=\sum _{x\in z\cup \left\{w\right\}}\sum _{k\in B}C\right)\right)$$
28	27	imbi2d	$$⊢u=z\cup \left\{w\right\}\to \left(\left(\phi \to \left(u\subseteq A\to \sum _{k\in \bigcup _{x\in u}B}C=\sum _{x\in u}\sum _{k\in B}C\right)\right)\leftrightarrow \left(\phi \to \left(z\cup \left\{w\right\}\subseteq A\to \sum _{k\in \bigcup _{x\in z\cup \left\{w\right\}}B}C=\sum _{x\in z\cup \left\{w\right\}}\sum _{k\in B}C\right)\right)\right)$$
29		sseq1	$$⊢u=A\to \left(u\subseteq A\leftrightarrow A\subseteq A\right)$$
30		iuneq1	$$⊢u=A\to \bigcup _{x\in u}B=\bigcup _{x\in A}B$$
31	30	sumeq1d	$$⊢u=A\to \sum _{k\in \bigcup _{x\in u}B}C=\sum _{k\in \bigcup _{x\in A}B}C$$
32		sumeq1	$$⊢u=A\to \sum _{x\in u}\sum _{k\in B}C=\sum _{x\in A}\sum _{k\in B}C$$
33	31 32	eqeq12d	$$⊢u=A\to \left(\sum _{k\in \bigcup _{x\in u}B}C=\sum _{x\in u}\sum _{k\in B}C\leftrightarrow \sum _{k\in \bigcup _{x\in A}B}C=\sum _{x\in A}\sum _{k\in B}C\right)$$
34	29 33	imbi12d	$$⊢u=A\to \left(\left(u\subseteq A\to \sum _{k\in \bigcup _{x\in u}B}C=\sum _{x\in u}\sum _{k\in B}C\right)\leftrightarrow \left(A\subseteq A\to \sum _{k\in \bigcup _{x\in A}B}C=\sum _{x\in A}\sum _{k\in B}C\right)\right)$$
35	34	imbi2d	$$⊢u=A\to \left(\left(\phi \to \left(u\subseteq A\to \sum _{k\in \bigcup _{x\in u}B}C=\sum _{x\in u}\sum _{k\in B}C\right)\right)\leftrightarrow \left(\phi \to \left(A\subseteq A\to \sum _{k\in \bigcup _{x\in A}B}C=\sum _{x\in A}\sum _{k\in B}C\right)\right)\right)$$
36		sum0	$$⊢\sum _{k\in \varnothing }C=0$$
37		sum0	$$⊢\sum _{x\in \varnothing }\sum _{k\in B}C=0$$
38	36 37	eqtr4i	$$⊢\sum _{k\in \varnothing }C=\sum _{x\in \varnothing }\sum _{k\in B}C$$
39	38	2a1i	$$⊢\phi \to \left(\varnothing \subseteq A\to \sum _{k\in \varnothing }C=\sum _{x\in \varnothing }\sum _{k\in B}C\right)$$
40		id	$$⊢z\cup \left\{w\right\}\subseteq A\to z\cup \left\{w\right\}\subseteq A$$
41	40	unssad	$$⊢z\cup \left\{w\right\}\subseteq A\to z\subseteq A$$
42	41	imim1i	$$⊢\left(z\subseteq A\to \sum _{k\in \bigcup _{x\in z}B}C=\sum _{x\in z}\sum _{k\in B}C\right)\to \left(z\cup \left\{w\right\}\subseteq A\to \sum _{k\in \bigcup _{x\in z}B}C=\sum _{x\in z}\sum _{k\in B}C\right)$$
43		oveq1	$$⊢\sum _{k\in \bigcup _{x\in z}B}C=\sum _{x\in z}\sum _{k\in B}C\to \sum _{k\in \bigcup _{x\in z}B}C+\sum _{k\in ⦋w/x⦌B}C=\sum _{x\in z}\sum _{k\in B}C+\sum _{k\in ⦋w/x⦌B}C$$
44		nfcv	$$⊢\underset{\_}{Ⅎ}zB$$
45		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋z/x⦌B$$
46		csbeq1a	$$⊢x=z\to B=⦋z/x⦌B$$
47	44 45 46	cbviun	$$⊢\bigcup _{x\in \left\{w\right\}}B=\bigcup _{z\in \left\{w\right\}}⦋z/x⦌B$$
48		vex	$$⊢w\in \mathrm{V}$$
49		csbeq1	$$⊢z=w\to ⦋z/x⦌B=⦋w/x⦌B$$
50	48 49	iunxsn	$$⊢\bigcup _{z\in \left\{w\right\}}⦋z/x⦌B=⦋w/x⦌B$$
51	47 50	eqtri	$$⊢\bigcup _{x\in \left\{w\right\}}B=⦋w/x⦌B$$
52	51	ineq2i	$$⊢\bigcup _{x\in z}B\cap \bigcup _{x\in \left\{w\right\}}B=\bigcup _{x\in z}B\cap ⦋w/x⦌B$$
53	3	ad2antrr	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \underset{x\in A}{Disj}B$$
54	41	adantl	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to z\subseteq A$$
55		simpr	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to z\cup \left\{w\right\}\subseteq A$$
56	55	unssbd	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \left\{w\right\}\subseteq A$$
57		simplr	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \neg w\in z$$
58		disjsn	$$⊢z\cap \left\{w\right\}=\varnothing \leftrightarrow \neg w\in z$$
59	57 58	sylibr	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to z\cap \left\{w\right\}=\varnothing$$
60		disjiun	$$⊢\left(\underset{x\in A}{Disj}B\wedge \left(z\subseteq A\wedge \left\{w\right\}\subseteq A\wedge z\cap \left\{w\right\}=\varnothing \right)\right)\to \bigcup _{x\in z}B\cap \bigcup _{x\in \left\{w\right\}}B=\varnothing$$
61	53 54 56 59 60	syl13anc	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \bigcup _{x\in z}B\cap \bigcup _{x\in \left\{w\right\}}B=\varnothing$$
62	52 61	syl5eqr	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \bigcup _{x\in z}B\cap ⦋w/x⦌B=\varnothing$$
63		iunxun	$$⊢\bigcup _{x\in z\cup \left\{w\right\}}B=\bigcup _{x\in z}B\cup \bigcup _{x\in \left\{w\right\}}B$$
64	51	uneq2i	$$⊢\bigcup _{x\in z}B\cup \bigcup _{x\in \left\{w\right\}}B=\bigcup _{x\in z}B\cup ⦋w/x⦌B$$
65	63 64	eqtri	$$⊢\bigcup _{x\in z\cup \left\{w\right\}}B=\bigcup _{x\in z}B\cup ⦋w/x⦌B$$
66	65	a1i	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \bigcup _{x\in z\cup \left\{w\right\}}B=\bigcup _{x\in z}B\cup ⦋w/x⦌B$$
67	1	ad2antrr	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to A\in \mathrm{Fin}$$
68	67 55	ssfid	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to z\cup \left\{w\right\}\in \mathrm{Fin}$$
69	2	ralrimiva	$$⊢\phi \to \forall x\in AB\in \mathrm{Fin}$$
70	69	ad2antrr	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \forall x\in AB\in \mathrm{Fin}$$
71		ssralv	$$⊢z\cup \left\{w\right\}\subseteq A\to \left(\forall x\in AB\in \mathrm{Fin}\to \forall x\in \left(z\cup \left\{w\right\}\right)B\in \mathrm{Fin}\right)$$
72	55 70 71	sylc	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \forall x\in \left(z\cup \left\{w\right\}\right)B\in \mathrm{Fin}$$
73		iunfi	$$⊢\left(z\cup \left\{w\right\}\in \mathrm{Fin}\wedge \forall x\in \left(z\cup \left\{w\right\}\right)B\in \mathrm{Fin}\right)\to \bigcup _{x\in z\cup \left\{w\right\}}B\in \mathrm{Fin}$$
74	68 72 73	syl2anc	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \bigcup _{x\in z\cup \left\{w\right\}}B\in \mathrm{Fin}$$
75		iunss1	$$⊢z\cup \left\{w\right\}\subseteq A\to \bigcup _{x\in z\cup \left\{w\right\}}B\subseteq \bigcup _{x\in A}B$$
76	75	adantl	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \bigcup _{x\in z\cup \left\{w\right\}}B\subseteq \bigcup _{x\in A}B$$
77	76	sselda	$$⊢\left(\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\wedge k\in \bigcup _{x\in z\cup \left\{w\right\}}B\right)\to k\in \bigcup _{x\in A}B$$
78		eliun	$$⊢k\in \bigcup _{x\in A}B\leftrightarrow \exists x\in Ak\in B$$
79	4	rexlimdvaa	$$⊢\phi \to \left(\exists x\in Ak\in B\to C\in ℂ\right)$$
80	79	ad2antrr	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \left(\exists x\in Ak\in B\to C\in ℂ\right)$$
81	78 80	syl5bi	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \left(k\in \bigcup _{x\in A}B\to C\in ℂ\right)$$
82	81	imp	$$⊢\left(\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\wedge k\in \bigcup _{x\in A}B\right)\to C\in ℂ$$
83	77 82	syldan	$$⊢\left(\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\wedge k\in \bigcup _{x\in z\cup \left\{w\right\}}B\right)\to C\in ℂ$$
84	62 66 74 83	fsumsplit	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \sum _{k\in \bigcup _{x\in z\cup \left\{w\right\}}B}C=\sum _{k\in \bigcup _{x\in z}B}C+\sum _{k\in ⦋w/x⦌B}C$$
85		eqidd	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to z\cup \left\{w\right\}=z\cup \left\{w\right\}$$
86	55	sselda	$$⊢\left(\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\wedge x\in \left(z\cup \left\{w\right\}\right)\right)\to x\in A$$
87	4	anassrs	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge k\in B\right)\to C\in ℂ$$
88	2 87	fsumcl	$$⊢\left(\phi \wedge x\in A\right)\to \sum _{k\in B}C\in ℂ$$
89	88	ralrimiva	$$⊢\phi \to \forall x\in A\sum _{k\in B}C\in ℂ$$
90	89	ad2antrr	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \forall x\in A\sum _{k\in B}C\in ℂ$$
91	90	r19.21bi	$$⊢\left(\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\wedge x\in A\right)\to \sum _{k\in B}C\in ℂ$$
92	86 91	syldan	$$⊢\left(\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\wedge x\in \left(z\cup \left\{w\right\}\right)\right)\to \sum _{k\in B}C\in ℂ$$
93	59 85 68 92	fsumsplit	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \sum _{x\in z\cup \left\{w\right\}}\sum _{k\in B}C=\sum _{x\in z}\sum _{k\in B}C+\sum _{x\in \left\{w\right\}}\sum _{k\in B}C$$
94		nfcv	$$⊢\underset{\_}{Ⅎ}z\sum _{k\in B}C$$
95		nfcv	$$⊢\underset{\_}{Ⅎ}xC$$
96	45 95	nfsum	$$⊢\underset{\_}{Ⅎ}x\sum _{k\in ⦋z/x⦌B}C$$
97	46	sumeq1d	$$⊢x=z\to \sum _{k\in B}C=\sum _{k\in ⦋z/x⦌B}C$$
98	94 96 97	cbvsumi	$$⊢\sum _{x\in \left\{w\right\}}\sum _{k\in B}C=\sum _{z\in \left\{w\right\}}\sum _{k\in ⦋z/x⦌B}C$$
99	48	snss	$$⊢w\in A\leftrightarrow \left\{w\right\}\subseteq A$$
100	56 99	sylibr	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to w\in A$$
101		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋w/x⦌B$$
102	101 95	nfsum	$$⊢\underset{\_}{Ⅎ}x\sum _{k\in ⦋w/x⦌B}C$$
103	102	nfel1	$$⊢Ⅎx\sum _{k\in ⦋w/x⦌B}C\in ℂ$$
104		csbeq1a	$$⊢x=w\to B=⦋w/x⦌B$$
105	104	sumeq1d	$$⊢x=w\to \sum _{k\in B}C=\sum _{k\in ⦋w/x⦌B}C$$
106	105	eleq1d	$$⊢x=w\to \left(\sum _{k\in B}C\in ℂ\leftrightarrow \sum _{k\in ⦋w/x⦌B}C\in ℂ\right)$$
107	103 106	rspc	$$⊢w\in A\to \left(\forall x\in A\sum _{k\in B}C\in ℂ\to \sum _{k\in ⦋w/x⦌B}C\in ℂ\right)$$
108	100 90 107	sylc	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \sum _{k\in ⦋w/x⦌B}C\in ℂ$$
109	49	sumeq1d	$$⊢z=w\to \sum _{k\in ⦋z/x⦌B}C=\sum _{k\in ⦋w/x⦌B}C$$
110	109	sumsn	$$⊢\left(w\in \mathrm{V}\wedge \sum _{k\in ⦋w/x⦌B}C\in ℂ\right)\to \sum _{z\in \left\{w\right\}}\sum _{k\in ⦋z/x⦌B}C=\sum _{k\in ⦋w/x⦌B}C$$
111	48 108 110	sylancr	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \sum _{z\in \left\{w\right\}}\sum _{k\in ⦋z/x⦌B}C=\sum _{k\in ⦋w/x⦌B}C$$
112	98 111	syl5eq	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \sum _{x\in \left\{w\right\}}\sum _{k\in B}C=\sum _{k\in ⦋w/x⦌B}C$$
113	112	oveq2d	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \sum _{x\in z}\sum _{k\in B}C+\sum _{x\in \left\{w\right\}}\sum _{k\in B}C=\sum _{x\in z}\sum _{k\in B}C+\sum _{k\in ⦋w/x⦌B}C$$
114	93 113	eqtrd	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \sum _{x\in z\cup \left\{w\right\}}\sum _{k\in B}C=\sum _{x\in z}\sum _{k\in B}C+\sum _{k\in ⦋w/x⦌B}C$$
115	84 114	eqeq12d	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \left(\sum _{k\in \bigcup _{x\in z\cup \left\{w\right\}}B}C=\sum _{x\in z\cup \left\{w\right\}}\sum _{k\in B}C\leftrightarrow \sum _{k\in \bigcup _{x\in z}B}C+\sum _{k\in ⦋w/x⦌B}C=\sum _{x\in z}\sum _{k\in B}C+\sum _{k\in ⦋w/x⦌B}C\right)$$
116	43 115	syl5ibr	$$⊢\left(\left(\phi \wedge \neg w\in z\right)\wedge z\cup \left\{w\right\}\subseteq A\right)\to \left(\sum _{k\in \bigcup _{x\in z}B}C=\sum _{x\in z}\sum _{k\in B}C\to \sum _{k\in \bigcup _{x\in z\cup \left\{w\right\}}B}C=\sum _{x\in z\cup \left\{w\right\}}\sum _{k\in B}C\right)$$
117	116	ex	$$⊢\left(\phi \wedge \neg w\in z\right)\to \left(z\cup \left\{w\right\}\subseteq A\to \left(\sum _{k\in \bigcup _{x\in z}B}C=\sum _{x\in z}\sum _{k\in B}C\to \sum _{k\in \bigcup _{x\in z\cup \left\{w\right\}}B}C=\sum _{x\in z\cup \left\{w\right\}}\sum _{k\in B}C\right)\right)$$
118	117	a2d	$$⊢\left(\phi \wedge \neg w\in z\right)\to \left(\left(z\cup \left\{w\right\}\subseteq A\to \sum _{k\in \bigcup _{x\in z}B}C=\sum _{x\in z}\sum _{k\in B}C\right)\to \left(z\cup \left\{w\right\}\subseteq A\to \sum _{k\in \bigcup _{x\in z\cup \left\{w\right\}}B}C=\sum _{x\in z\cup \left\{w\right\}}\sum _{k\in B}C\right)\right)$$
119	42 118	syl5	$$⊢\left(\phi \wedge \neg w\in z\right)\to \left(\left(z\subseteq A\to \sum _{k\in \bigcup _{x\in z}B}C=\sum _{x\in z}\sum _{k\in B}C\right)\to \left(z\cup \left\{w\right\}\subseteq A\to \sum _{k\in \bigcup _{x\in z\cup \left\{w\right\}}B}C=\sum _{x\in z\cup \left\{w\right\}}\sum _{k\in B}C\right)\right)$$
120	119	expcom	$$⊢\neg w\in z\to \left(\phi \to \left(\left(z\subseteq A\to \sum _{k\in \bigcup _{x\in z}B}C=\sum _{x\in z}\sum _{k\in B}C\right)\to \left(z\cup \left\{w\right\}\subseteq A\to \sum _{k\in \bigcup _{x\in z\cup \left\{w\right\}}B}C=\sum _{x\in z\cup \left\{w\right\}}\sum _{k\in B}C\right)\right)\right)$$
121	120	a2d	$$⊢\neg w\in z\to \left(\left(\phi \to \left(z\subseteq A\to \sum _{k\in \bigcup _{x\in z}B}C=\sum _{x\in z}\sum _{k\in B}C\right)\right)\to \left(\phi \to \left(z\cup \left\{w\right\}\subseteq A\to \sum _{k\in \bigcup _{x\in z\cup \left\{w\right\}}B}C=\sum _{x\in z\cup \left\{w\right\}}\sum _{k\in B}C\right)\right)\right)$$
122	121	adantl	$$⊢\left(z\in \mathrm{Fin}\wedge \neg w\in z\right)\to \left(\left(\phi \to \left(z\subseteq A\to \sum _{k\in \bigcup _{x\in z}B}C=\sum _{x\in z}\sum _{k\in B}C\right)\right)\to \left(\phi \to \left(z\cup \left\{w\right\}\subseteq A\to \sum _{k\in \bigcup _{x\in z\cup \left\{w\right\}}B}C=\sum _{x\in z\cup \left\{w\right\}}\sum _{k\in B}C\right)\right)\right)$$
123	14 21 28 35 39 122	findcard2s	$$⊢A\in \mathrm{Fin}\to \left(\phi \to \left(A\subseteq A\to \sum _{k\in \bigcup _{x\in A}B}C=\sum _{x\in A}\sum _{k\in B}C\right)\right)$$
124	1 123	mpcom	$$⊢\phi \to \left(A\subseteq A\to \sum _{k\in \bigcup _{x\in A}B}C=\sum _{x\in A}\sum _{k\in B}C\right)$$
125	5 124	mpi	$$⊢\phi \to \sum _{k\in \bigcup _{x\in A}B}C=\sum _{x\in A}\sum _{k\in B}C$$