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 
|- ( ph -> A e. Fin )
fsumiun.2 
|- ( ( ph /\ x e. A ) -> B e. Fin )
fsumiun.3 
|- ( ph -> Disj_ x e. A B )
fsumiun.4 
|- ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. CC )
Assertion fsumiun 
|- ( ph -> sum_ k e. U_ x e. A B C = sum_ x e. A sum_ k e. B C )

Proof

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