fprodeq02

Description: If one of the factors is zero the product is zero. (Contributed by Thierry Arnoux, 11-Dec-2021)

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

Metamath Proof Explorer