Step |
Hyp |
Ref |
Expression |
1 |
|
fprodsplitsn.ph |
|- F/ k ph |
2 |
|
fprodsplitsn.kd |
|- F/_ k D |
3 |
|
fprodsplitsn.a |
|- ( ph -> A e. Fin ) |
4 |
|
fprodsplitsn.b |
|- ( ph -> B e. V ) |
5 |
|
fprodsplitsn.ba |
|- ( ph -> -. B e. A ) |
6 |
|
fprodsplitsn.c |
|- ( ( ph /\ k e. A ) -> C e. CC ) |
7 |
|
fprodsplitsn.d |
|- ( k = B -> C = D ) |
8 |
|
fprodsplitsn.dcn |
|- ( ph -> D e. CC ) |
9 |
|
disjsn |
|- ( ( A i^i { B } ) = (/) <-> -. B e. A ) |
10 |
5 9
|
sylibr |
|- ( ph -> ( A i^i { B } ) = (/) ) |
11 |
|
eqidd |
|- ( ph -> ( A u. { B } ) = ( A u. { B } ) ) |
12 |
|
snfi |
|- { B } e. Fin |
13 |
|
unfi |
|- ( ( A e. Fin /\ { B } e. Fin ) -> ( A u. { B } ) e. Fin ) |
14 |
3 12 13
|
sylancl |
|- ( ph -> ( A u. { B } ) e. Fin ) |
15 |
6
|
adantlr |
|- ( ( ( ph /\ k e. ( A u. { B } ) ) /\ k e. A ) -> C e. CC ) |
16 |
|
elunnel1 |
|- ( ( k e. ( A u. { B } ) /\ -. k e. A ) -> k e. { B } ) |
17 |
|
elsni |
|- ( k e. { B } -> k = B ) |
18 |
16 17
|
syl |
|- ( ( k e. ( A u. { B } ) /\ -. k e. A ) -> k = B ) |
19 |
18
|
adantll |
|- ( ( ( ph /\ k e. ( A u. { B } ) ) /\ -. k e. A ) -> k = B ) |
20 |
19 7
|
syl |
|- ( ( ( ph /\ k e. ( A u. { B } ) ) /\ -. k e. A ) -> C = D ) |
21 |
8
|
ad2antrr |
|- ( ( ( ph /\ k e. ( A u. { B } ) ) /\ -. k e. A ) -> D e. CC ) |
22 |
20 21
|
eqeltrd |
|- ( ( ( ph /\ k e. ( A u. { B } ) ) /\ -. k e. A ) -> C e. CC ) |
23 |
15 22
|
pm2.61dan |
|- ( ( ph /\ k e. ( A u. { B } ) ) -> C e. CC ) |
24 |
1 10 11 14 23
|
fprodsplitf |
|- ( ph -> prod_ k e. ( A u. { B } ) C = ( prod_ k e. A C x. prod_ k e. { B } C ) ) |
25 |
2 7
|
prodsnf |
|- ( ( B e. V /\ D e. CC ) -> prod_ k e. { B } C = D ) |
26 |
4 8 25
|
syl2anc |
|- ( ph -> prod_ k e. { B } C = D ) |
27 |
26
|
oveq2d |
|- ( ph -> ( prod_ k e. A C x. prod_ k e. { B } C ) = ( prod_ k e. A C x. D ) ) |
28 |
24 27
|
eqtrd |
|- ( ph -> prod_ k e. ( A u. { B } ) C = ( prod_ k e. A C x. D ) ) |