Theorem fprod0

Description: A finite product with a zero term is zero. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fprod0.kph	|- F/ k ph
	fprod0.kc	|- F/_ k C
	fprod0.a	|- ( ph -> A e. Fin )
	fprod0.b	|- ( ( ph /\ k e. A ) -> B e. CC )
	fprod0.bc	|- ( k = K -> B = C )
	fprod0.k	|- ( ph -> K e. A )
	fprod0.c	|- ( ph -> C = 0 )
Assertion	fprod0	|- ( ph -> prod_ k e. A B = 0 )

Proof

Step	Hyp	Ref	Expression
1		fprod0.kph	|- F/ k ph
2		fprod0.kc	|- F/_ k C
3		fprod0.a	|- ( ph -> A e. Fin )
4		fprod0.b	|- ( ( ph /\ k e. A ) -> B e. CC )
5		fprod0.bc	|- ( k = K -> B = C )
6		fprod0.k	|- ( ph -> K e. A )
7		fprod0.c	|- ( ph -> C = 0 )
8	2	a1i	|- ( ph -> F/_ k C )
9	5	adantl	|- ( ( ph /\ k = K ) -> B = C )
10	1 8 3 4 6 9	fprodsplit1f	|- ( ph -> prod_ k e. A B = ( C x. prod_ k e. ( A \ { K } ) B ) )
11	7	oveq1d	|- ( ph -> ( C x. prod_ k e. ( A \ { K } ) B ) = ( 0 x. prod_ k e. ( A \ { K } ) B ) )
12		diffi	|- ( A e. Fin -> ( A \ { K } ) e. Fin )
13	3 12	syl	|- ( ph -> ( A \ { K } ) e. Fin )
14		simpl	|- ( ( ph /\ k e. ( A \ { K } ) ) -> ph )
15		eldifi	|- ( k e. ( A \ { K } ) -> k e. A )
16	15	adantl	|- ( ( ph /\ k e. ( A \ { K } ) ) -> k e. A )
17	14 16 4	syl2anc	|- ( ( ph /\ k e. ( A \ { K } ) ) -> B e. CC )
18	1 13 17	fprodclf	|- ( ph -> prod_ k e. ( A \ { K } ) B e. CC )
19	18	mul02d	|- ( ph -> ( 0 x. prod_ k e. ( A \ { K } ) B ) = 0 )
20	10 11 19	3eqtrd	|- ( ph -> prod_ k e. A B = 0 )