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
|
syl5eqr |
|- ( ( ( 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
|
syl5eq |
|- ( ( ( 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 ) |