Theorem fprodeq0g

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

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

Proof

Step	Hyp	Ref	Expression
1		fprodeq0g.kph	|- F/ k ph
2		fprodeq0g.a	|- ( ph -> A e. Fin )
3		fprodeq0g.b	|- ( ( ph /\ k e. A ) -> B e. CC )
4		fprodeq0g.c	|- ( ph -> C e. A )
5		fprodeq0g.b0	|- ( ( ph /\ k = C ) -> B = 0 )
6		nfcvd	|- ( ph -> F/_ k 0 )
7	1 6 2 3 4 5	fprodsplit1f	|- ( ph -> prod_ k e. A B = ( 0 x. prod_ k e. ( A \ { C } ) B ) )
8		diffi	|- ( A e. Fin -> ( A \ { C } ) e. Fin )
9	2 8	syl	|- ( ph -> ( A \ { C } ) e. Fin )
10		eldifi	|- ( k e. ( A \ { C } ) -> k e. A )
11	10 3	sylan2	|- ( ( ph /\ k e. ( A \ { C } ) ) -> B e. CC )
12	1 9 11	fprodclf	|- ( ph -> prod_ k e. ( A \ { C } ) B e. CC )
13	12	mul02d	|- ( ph -> ( 0 x. prod_ k e. ( A \ { C } ) B ) = 0 )
14	7 13	eqtrd	|- ( ph -> prod_ k e. A B = 0 )