| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fprodeq02.1 |
|- ( k = K -> B = C ) |
| 2 |
|
fprodeq02.a |
|- ( ph -> A e. Fin ) |
| 3 |
|
fprodeq02.b |
|- ( ( ph /\ k e. A ) -> B e. CC ) |
| 4 |
|
fprodeq02.k |
|- ( ph -> K e. A ) |
| 5 |
|
fprodeq02.c |
|- ( ph -> C = 0 ) |
| 6 |
|
disjdif |
|- ( { K } i^i ( A \ { K } ) ) = (/) |
| 7 |
6
|
a1i |
|- ( ph -> ( { K } i^i ( A \ { K } ) ) = (/) ) |
| 8 |
4
|
snssd |
|- ( ph -> { K } C_ A ) |
| 9 |
|
undif |
|- ( { K } C_ A <-> ( { K } u. ( A \ { K } ) ) = A ) |
| 10 |
8 9
|
sylib |
|- ( ph -> ( { K } u. ( A \ { K } ) ) = A ) |
| 11 |
10
|
eqcomd |
|- ( ph -> A = ( { K } u. ( A \ { K } ) ) ) |
| 12 |
7 11 2 3
|
fprodsplit |
|- ( ph -> prod_ k e. A B = ( prod_ k e. { K } B x. prod_ k e. ( A \ { K } ) B ) ) |
| 13 |
|
0cnd |
|- ( ph -> 0 e. CC ) |
| 14 |
5 13
|
eqeltrd |
|- ( ph -> C e. CC ) |
| 15 |
1
|
prodsn |
|- ( ( K e. A /\ C e. CC ) -> prod_ k e. { K } B = C ) |
| 16 |
4 14 15
|
syl2anc |
|- ( ph -> prod_ k e. { K } B = C ) |
| 17 |
16 5
|
eqtrd |
|- ( ph -> prod_ k e. { K } B = 0 ) |
| 18 |
17
|
oveq1d |
|- ( ph -> ( prod_ k e. { K } B x. prod_ k e. ( A \ { K } ) B ) = ( 0 x. prod_ k e. ( A \ { K } ) B ) ) |
| 19 |
|
diffi |
|- ( A e. Fin -> ( A \ { K } ) e. Fin ) |
| 20 |
2 19
|
syl |
|- ( ph -> ( A \ { K } ) e. Fin ) |
| 21 |
|
difssd |
|- ( ph -> ( A \ { K } ) C_ A ) |
| 22 |
21
|
sselda |
|- ( ( ph /\ k e. ( A \ { K } ) ) -> k e. A ) |
| 23 |
22 3
|
syldan |
|- ( ( ph /\ k e. ( A \ { K } ) ) -> B e. CC ) |
| 24 |
20 23
|
fprodcl |
|- ( ph -> prod_ k e. ( A \ { K } ) B e. CC ) |
| 25 |
24
|
mul02d |
|- ( ph -> ( 0 x. prod_ k e. ( A \ { K } ) B ) = 0 ) |
| 26 |
12 18 25
|
3eqtrd |
|- ( ph -> prod_ k e. A B = 0 ) |