| Step |
Hyp |
Ref |
Expression |
| 1 |
|
sumpr.1 |
|- ( k = A -> C = D ) |
| 2 |
|
sumpr.2 |
|- ( k = B -> C = E ) |
| 3 |
|
sumpr.3 |
|- ( ph -> ( D e. CC /\ E e. CC ) ) |
| 4 |
|
sumpr.4 |
|- ( ph -> ( A e. V /\ B e. W ) ) |
| 5 |
|
sumpr.5 |
|- ( ph -> A =/= B ) |
| 6 |
|
disjsn2 |
|- ( A =/= B -> ( { A } i^i { B } ) = (/) ) |
| 7 |
5 6
|
syl |
|- ( ph -> ( { A } i^i { B } ) = (/) ) |
| 8 |
|
df-pr |
|- { A , B } = ( { A } u. { B } ) |
| 9 |
8
|
a1i |
|- ( ph -> { A , B } = ( { A } u. { B } ) ) |
| 10 |
|
prfi |
|- { A , B } e. Fin |
| 11 |
10
|
a1i |
|- ( ph -> { A , B } e. Fin ) |
| 12 |
1
|
eleq1d |
|- ( k = A -> ( C e. CC <-> D e. CC ) ) |
| 13 |
2
|
eleq1d |
|- ( k = B -> ( C e. CC <-> E e. CC ) ) |
| 14 |
12 13
|
ralprg |
|- ( ( A e. V /\ B e. W ) -> ( A. k e. { A , B } C e. CC <-> ( D e. CC /\ E e. CC ) ) ) |
| 15 |
4 14
|
syl |
|- ( ph -> ( A. k e. { A , B } C e. CC <-> ( D e. CC /\ E e. CC ) ) ) |
| 16 |
3 15
|
mpbird |
|- ( ph -> A. k e. { A , B } C e. CC ) |
| 17 |
16
|
r19.21bi |
|- ( ( ph /\ k e. { A , B } ) -> C e. CC ) |
| 18 |
7 9 11 17
|
fsumsplit |
|- ( ph -> sum_ k e. { A , B } C = ( sum_ k e. { A } C + sum_ k e. { B } C ) ) |
| 19 |
4
|
simpld |
|- ( ph -> A e. V ) |
| 20 |
3
|
simpld |
|- ( ph -> D e. CC ) |
| 21 |
1
|
sumsn |
|- ( ( A e. V /\ D e. CC ) -> sum_ k e. { A } C = D ) |
| 22 |
19 20 21
|
syl2anc |
|- ( ph -> sum_ k e. { A } C = D ) |
| 23 |
4
|
simprd |
|- ( ph -> B e. W ) |
| 24 |
3
|
simprd |
|- ( ph -> E e. CC ) |
| 25 |
2
|
sumsn |
|- ( ( B e. W /\ E e. CC ) -> sum_ k e. { B } C = E ) |
| 26 |
23 24 25
|
syl2anc |
|- ( ph -> sum_ k e. { B } C = E ) |
| 27 |
22 26
|
oveq12d |
|- ( ph -> ( sum_ k e. { A } C + sum_ k e. { B } C ) = ( D + E ) ) |
| 28 |
18 27
|
eqtrd |
|- ( ph -> sum_ k e. { A , B } C = ( D + E ) ) |