fprod0

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

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

Metamath Proof Explorer