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 φ A Fin
fsumiun.2 φ x A B Fin
fsumiun.3 φ Disj x A B
fsumiun.4 φ x A k B C
Assertion fsumiun φ k x A B C = x A k B C

Proof

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