Theorem fprod0

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

	Ref	Expression
Hypotheses	fprod0.kph	⊢ Ⅎ 𝑘 𝜑
	fprod0.kc	⊢ Ⅎ 𝑘 𝐶
	fprod0.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprod0.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	fprod0.bc	⊢ ( 𝑘 = 𝐾 → 𝐵 = 𝐶 )
	fprod0.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐴 )
	fprod0.c	⊢ ( 𝜑 → 𝐶 = 0 )
Assertion	fprod0	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = 0 )

Proof

Step	Hyp	Ref	Expression
1		fprod0.kph	⊢ Ⅎ 𝑘 𝜑
2		fprod0.kc	⊢ Ⅎ 𝑘 𝐶
3		fprod0.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
4		fprod0.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
5		fprod0.bc	⊢ ( 𝑘 = 𝐾 → 𝐵 = 𝐶 )
6		fprod0.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐴 )
7		fprod0.c	⊢ ( 𝜑 → 𝐶 = 0 )
8	2	a1i	⊢ ( 𝜑 → Ⅎ 𝑘 𝐶 )
9	5	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐾 ) → 𝐵 = 𝐶 )
10	1 8 3 4 6 9	fprodsplit1f	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = ( 𝐶 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) 𝐵 ) )
11	7	oveq1d	⊢ ( 𝜑 → ( 𝐶 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) 𝐵 ) = ( 0 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) 𝐵 ) )
12		diffi	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ { 𝐾 } ) ∈ Fin )
13	3 12	syl	⊢ ( 𝜑 → ( 𝐴 ∖ { 𝐾 } ) ∈ Fin )
14		simpl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) ) → 𝜑 )
15		eldifi	⊢ ( 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) → 𝑘 ∈ 𝐴 )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) ) → 𝑘 ∈ 𝐴 )
17	14 16 4	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) ) → 𝐵 ∈ ℂ )
18	1 13 17	fprodclf	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) 𝐵 ∈ ℂ )
19	18	mul02d	⊢ ( 𝜑 → ( 0 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) 𝐵 ) = 0 )
20	10 11 19	3eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = 0 )