fprodex01

Description: A product of factors equal to zero or one is zero exactly when one of the factors is zero. (Contributed by Thierry Arnoux, 11-Dec-2021)

	Ref	Expression
Hypotheses	fprodex01.1	$⊢ k = l \to B = C$
	fprodex01.a	$⊢ φ \to A \in Fin$
	fprodex01.b	$⊢ (φ \land k \in A) \to B \in \{0, 1\}$
Assertion	fprodex01	$⊢ φ \to \prod_{k \in A} B = if (\forall l \in A C = 1, 1, 0)$

Proof

Step	Hyp	Ref	Expression
1		fprodex01.1	$⊢ k = l \to B = C$
2		fprodex01.a	$⊢ φ \to A \in Fin$
3		fprodex01.b	$⊢ (φ \land k \in A) \to B \in \{0, 1\}$
4		simpr	$⊢ (φ \land \forall l \in A C = 1) \to \forall l \in A C = 1$
5	1	eqeq1d	$⊢ k = l \to (B = 1 \leftrightarrow C = 1)$
6	5	cbvralvw	$⊢ \forall k \in A B = 1 \leftrightarrow \forall l \in A C = 1$
7	4 6	sylibr	$⊢ (φ \land \forall l \in A C = 1) \to \forall k \in A B = 1$
8	7	prodeq2d	$⊢ (φ \land \forall l \in A C = 1) \to \prod_{k \in A} B = \prod_{k \in A} 1$
9		prod1	$⊢ (A \subseteq ℤ_{\geq 0} \lor A \in Fin) \to \prod_{k \in A} 1 = 1$
10	9	olcs	$⊢ A \in Fin \to \prod_{k \in A} 1 = 1$
11	2 10	syl	$⊢ φ \to \prod_{k \in A} 1 = 1$
12	11	adantr	$⊢ (φ \land \forall l \in A C = 1) \to \prod_{k \in A} 1 = 1$
13	8 12	eqtr2d	$⊢ (φ \land \forall l \in A C = 1) \to 1 = \prod_{k \in A} B$
14		nfv	$⊢ Ⅎ l φ$
15		nfra1	$⊢ Ⅎ l \forall l \in A C = 1$
16	15	nfn	$⊢ Ⅎ l \neg \forall l \in A C = 1$
17	14 16	nfan	$⊢ Ⅎ l (φ \land \neg \forall l \in A C = 1)$
18		nfv	$⊢ Ⅎ l \prod_{k \in A} B = 0$
19	2	adantr	$⊢ (φ \land \neg \forall l \in A C = 1) \to A \in Fin$
20	19	ad2antrr	$⊢ (((φ \land \neg \forall l \in A C = 1) \land l \in A) \land C = 0) \to A \in Fin$
21		pr01ssre	$⊢ \{0, 1\} \subseteq ℝ$
22		ax-resscn	$⊢ ℝ \subseteq ℂ$
23	21 22	sstri	$⊢ \{0, 1\} \subseteq ℂ$
24	23 3	sselid	$⊢ (φ \land k \in A) \to B \in ℂ$
25	24	adantlr	$⊢ ((φ \land \neg \forall l \in A C = 1) \land k \in A) \to B \in ℂ$
26	25	adantlr	$⊢ (((φ \land \neg \forall l \in A C = 1) \land l \in A) \land k \in A) \to B \in ℂ$
27	26	adantlr	$⊢ ((((φ \land \neg \forall l \in A C = 1) \land l \in A) \land C = 0) \land k \in A) \to B \in ℂ$
28		simplr	$⊢ (((φ \land \neg \forall l \in A C = 1) \land l \in A) \land C = 0) \to l \in A$
29		simpr	$⊢ (((φ \land \neg \forall l \in A C = 1) \land l \in A) \land C = 0) \to C = 0$
30	1 20 27 28 29	fprodeq02	$⊢ (((φ \land \neg \forall l \in A C = 1) \land l \in A) \land C = 0) \to \prod_{k \in A} B = 0$
31		rexnal	$⊢ \exists l \in A \neg C = 1 \leftrightarrow \neg \forall l \in A C = 1$
32	31	biimpri	$⊢ \neg \forall l \in A C = 1 \to \exists l \in A \neg C = 1$
33	32	adantl	$⊢ (φ \land \neg \forall l \in A C = 1) \to \exists l \in A \neg C = 1$
34	3	ralrimiva	$⊢ φ \to \forall k \in A B \in \{0, 1\}$
35	1	eleq1d	$⊢ k = l \to (B \in \{0, 1\} \leftrightarrow C \in \{0, 1\})$
36	35	cbvralvw	$⊢ \forall k \in A B \in \{0, 1\} \leftrightarrow \forall l \in A C \in \{0, 1\}$
37	34 36	sylib	$⊢ φ \to \forall l \in A C \in \{0, 1\}$
38	37	r19.21bi	$⊢ (φ \land l \in A) \to C \in \{0, 1\}$
39		c0ex	$⊢ 0 \in V$
40		1ex	$⊢ 1 \in V$
41	39 40	elpr2	$⊢ C \in \{0, 1\} \leftrightarrow (C = 0 \lor C = 1)$
42	38 41	sylib	$⊢ (φ \land l \in A) \to (C = 0 \lor C = 1)$
43	42	orcomd	$⊢ (φ \land l \in A) \to (C = 1 \lor C = 0)$
44	43	ord	$⊢ (φ \land l \in A) \to (\neg C = 1 \to C = 0)$
45	44	reximdva	$⊢ φ \to (\exists l \in A \neg C = 1 \to \exists l \in A C = 0)$
46	45	adantr	$⊢ (φ \land \neg \forall l \in A C = 1) \to (\exists l \in A \neg C = 1 \to \exists l \in A C = 0)$
47	33 46	mpd	$⊢ (φ \land \neg \forall l \in A C = 1) \to \exists l \in A C = 0$
48	17 18 30 47	r19.29af2	$⊢ (φ \land \neg \forall l \in A C = 1) \to \prod_{k \in A} B = 0$
49	48	eqcomd	$⊢ (φ \land \neg \forall l \in A C = 1) \to 0 = \prod_{k \in A} B$
50	13 49	ifeqda	$⊢ φ \to if (\forall l \in A C = 1, 1, 0) = \prod_{k \in A} B$
51	50	eqcomd	$⊢ φ \to \prod_{k \in A} B = if (\forall l \in A C = 1, 1, 0)$

Metamath Proof Explorer

Theorem fprodex01

Proof