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

Proof

Step	Hyp	Ref	Expression
1		fprodeq02.1	$$⊢k=K\to B=C$$
2		fprodeq02.a	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fprodeq02.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
4		fprodeq02.k	$$⊢\phi \to K\in A$$
5		fprodeq02.c	$$⊢\phi \to C=0$$
6		disjdif	$$⊢\left\{K\right\}\cap \left(A\setminus \left\{K\right\}\right)=\varnothing$$
7	6	a1i	$$⊢\phi \to \left\{K\right\}\cap \left(A\setminus \left\{K\right\}\right)=\varnothing$$
8	4	snssd	$$⊢\phi \to \left\{K\right\}\subseteq A$$
9		undif	$$⊢\left\{K\right\}\subseteq A\leftrightarrow \left\{K\right\}\cup \left(A\setminus \left\{K\right\}\right)=A$$
10	8 9	sylib	$$⊢\phi \to \left\{K\right\}\cup \left(A\setminus \left\{K\right\}\right)=A$$
11	10	eqcomd	$$⊢\phi \to A=\left\{K\right\}\cup \left(A\setminus \left\{K\right\}\right)$$
12	7 11 2 3	fprodsplit	$$⊢\phi \to \prod _{k\in A}B=\prod _{k\in \left\{K\right\}}B\prod _{k\in A\setminus \left\{K\right\}}B$$
13		0cnd	$$⊢\phi \to 0\in ℂ$$
14	5 13	eqeltrd	$$⊢\phi \to C\in ℂ$$
15	1	prodsn	$$⊢\left(K\in A\wedge C\in ℂ\right)\to \prod _{k\in \left\{K\right\}}B=C$$
16	4 14 15	syl2anc	$$⊢\phi \to \prod _{k\in \left\{K\right\}}B=C$$
17	16 5	eqtrd	$$⊢\phi \to \prod _{k\in \left\{K\right\}}B=0$$
18	17	oveq1d	$$⊢\phi \to \prod _{k\in \left\{K\right\}}B\prod _{k\in A\setminus \left\{K\right\}}B=0\cdot \prod _{k\in A\setminus \left\{K\right\}}B$$
19		diffi	$$⊢A\in \mathrm{Fin}\to A\setminus \left\{K\right\}\in \mathrm{Fin}$$
20	2 19	syl	$$⊢\phi \to A\setminus \left\{K\right\}\in \mathrm{Fin}$$
21		difssd	$$⊢\phi \to A\setminus \left\{K\right\}\subseteq A$$
22	21	sselda	$$⊢\left(\phi \wedge k\in \left(A\setminus \left\{K\right\}\right)\right)\to k\in A$$
23	22 3	syldan	$$⊢\left(\phi \wedge k\in \left(A\setminus \left\{K\right\}\right)\right)\to B\in ℂ$$
24	20 23	fprodcl	$$⊢\phi \to \prod _{k\in A\setminus \left\{K\right\}}B\in ℂ$$
25	24	mul02d	$$⊢\phi \to 0\cdot \prod _{k\in A\setminus \left\{K\right\}}B=0$$
26	12 18 25	3eqtrd	$$⊢\phi \to \prod _{k\in A}B=0$$