Theorem fprod0

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

	Ref	Expression
Hypotheses	fprod0.kph	$$⊢Ⅎk\phi$$
	fprod0.kc	$$⊢\underset{\_}{Ⅎ}kC$$
	fprod0.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	fprod0.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
	fprod0.bc	$$⊢k=K\to B=C$$
	fprod0.k	$$⊢\phi \to K\in A$$
	fprod0.c	$$⊢\phi \to C=0$$
Assertion	fprod0	$$⊢\phi \to \prod _{k\in A}B=0$$

Proof

Step	Hyp	Ref	Expression
1		fprod0.kph	$$⊢Ⅎk\phi$$
2		fprod0.kc	$$⊢\underset{\_}{Ⅎ}kC$$
3		fprod0.a	$$⊢\phi \to A\in \mathrm{Fin}$$
4		fprod0.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
5		fprod0.bc	$$⊢k=K\to B=C$$
6		fprod0.k	$$⊢\phi \to K\in A$$
7		fprod0.c	$$⊢\phi \to C=0$$
8	2	a1i	$$⊢\phi \to \underset{\_}{Ⅎ}kC$$
9	5	adantl	$$⊢\left(\phi \wedge k=K\right)\to B=C$$
10	1 8 3 4 6 9	fprodsplit1f	$$⊢\phi \to \prod _{k\in A}B=C\prod _{k\in A\setminus \left\{K\right\}}B$$
11	7	oveq1d	$$⊢\phi \to C\prod _{k\in A\setminus \left\{K\right\}}B=0\cdot \prod _{k\in A\setminus \left\{K\right\}}B$$
12		diffi	$$⊢A\in \mathrm{Fin}\to A\setminus \left\{K\right\}\in \mathrm{Fin}$$
13	3 12	syl	$$⊢\phi \to A\setminus \left\{K\right\}\in \mathrm{Fin}$$
14		simpl	$$⊢\left(\phi \wedge k\in \left(A\setminus \left\{K\right\}\right)\right)\to \phi$$
15		eldifi	$$⊢k\in \left(A\setminus \left\{K\right\}\right)\to k\in A$$
16	15	adantl	$$⊢\left(\phi \wedge k\in \left(A\setminus \left\{K\right\}\right)\right)\to k\in A$$
17	14 16 4	syl2anc	$$⊢\left(\phi \wedge k\in \left(A\setminus \left\{K\right\}\right)\right)\to B\in ℂ$$
18	1 13 17	fprodclf	$$⊢\phi \to \prod _{k\in A\setminus \left\{K\right\}}B\in ℂ$$
19	18	mul02d	$$⊢\phi \to 0\cdot \prod _{k\in A\setminus \left\{K\right\}}B=0$$
20	10 11 19	3eqtrd	$$⊢\phi \to \prod _{k\in A}B=0$$