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	$$⊢Ⅎk\phi$$
	fprodeq0g.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	fprodeq0g.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
	fprodeq0g.c	$$⊢\phi \to C\in A$$
	fprodeq0g.b0	$$⊢\left(\phi \wedge k=C\right)\to B=0$$
Assertion	fprodeq0g	$$⊢\phi \to \prod _{k\in A}B=0$$

Proof

Step	Hyp	Ref	Expression
1		fprodeq0g.kph	$$⊢Ⅎk\phi$$
2		fprodeq0g.a	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fprodeq0g.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
4		fprodeq0g.c	$$⊢\phi \to C\in A$$
5		fprodeq0g.b0	$$⊢\left(\phi \wedge k=C\right)\to B=0$$
6		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}k0$$
7	1 6 2 3 4 5	fprodsplit1f	$$⊢\phi \to \prod _{k\in A}B=0\cdot \prod _{k\in A\setminus \left\{C\right\}}B$$
8		diffi	$$⊢A\in \mathrm{Fin}\to A\setminus \left\{C\right\}\in \mathrm{Fin}$$
9	2 8	syl	$$⊢\phi \to A\setminus \left\{C\right\}\in \mathrm{Fin}$$
10		eldifi	$$⊢k\in \left(A\setminus \left\{C\right\}\right)\to k\in A$$
11	10 3	sylan2	$$⊢\left(\phi \wedge k\in \left(A\setminus \left\{C\right\}\right)\right)\to B\in ℂ$$
12	1 9 11	fprodclf	$$⊢\phi \to \prod _{k\in A\setminus \left\{C\right\}}B\in ℂ$$
13	12	mul02d	$$⊢\phi \to 0\cdot \prod _{k\in A\setminus \left\{C\right\}}B=0$$
14	7 13	eqtrd	$$⊢\phi \to \prod _{k\in A}B=0$$