# Metamath Proof Explorer

## 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}↔\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 syl6eq ${⊢}{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}↔\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)↔\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)↔\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}↔{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}↔\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)↔\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)↔\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}↔{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}↔\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)↔\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)↔\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}↔{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}↔\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)↔\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)↔\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
44 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{B}$
45 nfcsb1v
46 csbeq1a
47 44 45 46 cbviun
48 vex ${⊢}{w}\in \mathrm{V}$
49 csbeq1
50 48 49 iunxsn
51 47 50 eqtri
52 51 ineq2i
53 3 ad2antrr ${⊢}\left(\left({\phi }\wedge ¬{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 ¬{w}\in {z}\right)\wedge {z}\cup \left\{{w}\right\}\subseteq {A}\right)\to {z}\subseteq {A}$
55 simpr ${⊢}\left(\left({\phi }\wedge ¬{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 ¬{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 ¬{w}\in {z}\right)\wedge {z}\cup \left\{{w}\right\}\subseteq {A}\right)\to ¬{w}\in {z}$
58 disjsn ${⊢}{z}\cap \left\{{w}\right\}=\varnothing ↔¬{w}\in {z}$
59 57 58 sylibr ${⊢}\left(\left({\phi }\wedge ¬{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 ¬{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
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
65 63 64 eqtri
66 65 a1i
67 1 ad2antrr ${⊢}\left(\left({\phi }\wedge ¬{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 ¬{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 {A}\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{Fin}$
70 69 ad2antrr ${⊢}\left(\left({\phi }\wedge ¬{w}\in {z}\right)\wedge {z}\cup \left\{{w}\right\}\subseteq {A}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{Fin}$
71 ssralv ${⊢}{z}\cup \left\{{w}\right\}\subseteq {A}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{Fin}\to \forall {x}\in \left({z}\cup \left\{{w}\right\}\right)\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{Fin}\right)$
72 55 70 71 sylc ${⊢}\left(\left({\phi }\wedge ¬{w}\in {z}\right)\wedge {z}\cup \left\{{w}\right\}\subseteq {A}\right)\to \forall {x}\in \left({z}\cup \left\{{w}\right\}\right)\phantom{\rule{.4em}{0ex}}{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)\phantom{\rule{.4em}{0ex}}{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 ¬{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 ¬{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 ¬{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}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{k}\in {B}$
79 4 rexlimdvaa ${⊢}{\phi }\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{k}\in {B}\to {C}\in ℂ\right)$
80 79 ad2antrr ${⊢}\left(\left({\phi }\wedge ¬{w}\in {z}\right)\wedge {z}\cup \left\{{w}\right\}\subseteq {A}\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{k}\in {B}\to {C}\in ℂ\right)$
81 78 80 syl5bi ${⊢}\left(\left({\phi }\wedge ¬{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 ¬{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 ¬{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
85 eqidd ${⊢}\left(\left({\phi }\wedge ¬{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 ¬{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}\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {B}}{C}\in ℂ$
90 89 ad2antrr ${⊢}\left(\left({\phi }\wedge ¬{w}\in {z}\right)\wedge {z}\cup \left\{{w}\right\}\subseteq {A}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {B}}{C}\in ℂ$
91 90 r19.21bi ${⊢}\left(\left(\left({\phi }\wedge ¬{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 ¬{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 ¬{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}\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {B}}{C}$
95 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
96 45 95 nfsumw
97 46 sumeq1d
98 94 96 97 cbvsumi
99 48 snss ${⊢}{w}\in {A}↔\left\{{w}\right\}\subseteq {A}$
100 56 99 sylibr ${⊢}\left(\left({\phi }\wedge ¬{w}\in {z}\right)\wedge {z}\cup \left\{{w}\right\}\subseteq {A}\right)\to {w}\in {A}$
101 nfcsb1v
102 101 95 nfsumw
103 102 nfel1
104 csbeq1a
105 104 sumeq1d
106 105 eleq1d
107 103 106 rspc
108 100 90 107 sylc
109 49 sumeq1d
110 109 sumsn
111 48 108 110 sylancr
112 98 111 syl5eq
113 112 oveq2d
114 93 113 eqtrd
115 84 114 eqeq12d
116 43 115 syl5ibr ${⊢}\left(\left({\phi }\wedge ¬{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 ¬{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 ¬{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 ¬{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 ${⊢}¬{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 ${⊢}¬{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 ¬{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}$