Theorem fprodeq02

Description: If one of the factors is zero the product is zero. (Contributed by Thierry Arnoux, 11-Dec-2021)

	Ref	Expression
Hypotheses	fprodeq02.1	|- ( k = K -> B = C )
	fprodeq02.a	|- ( ph -> A e. Fin )
	fprodeq02.b	|- ( ( ph /\ k e. A ) -> B e. CC )
	fprodeq02.k	|- ( ph -> K e. A )
	fprodeq02.c	|- ( ph -> C = 0 )
Assertion	fprodeq02	|- ( ph -> prod_ k e. A B = 0 )

Proof

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 )