Theorem fprodeq0g

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

	Ref	Expression
Hypotheses	fprodeq0g.kph	⊢ Ⅎ 𝑘 𝜑
	fprodeq0g.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprodeq0g.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	fprodeq0g.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
	fprodeq0g.b0	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐶 ) → 𝐵 = 0 )
Assertion	fprodeq0g	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = 0 )

Proof

Step	Hyp	Ref	Expression
1		fprodeq0g.kph	⊢ Ⅎ 𝑘 𝜑
2		fprodeq0g.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fprodeq0g.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4		fprodeq0g.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
5		fprodeq0g.b0	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐶 ) → 𝐵 = 0 )
6		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑘 0 )
7	1 6 2 3 4 5	fprodsplit1f	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = ( 0 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 ) )
8		diffi	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ { 𝐶 } ) ∈ Fin )
9	2 8	syl	⊢ ( 𝜑 → ( 𝐴 ∖ { 𝐶 } ) ∈ Fin )
10		eldifi	⊢ ( 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) → 𝑘 ∈ 𝐴 )
11	10 3	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) ) → 𝐵 ∈ ℂ )
12	1 9 11	fprodclf	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 ∈ ℂ )
13	12	mul02d	⊢ ( 𝜑 → ( 0 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 ) = 0 )
14	7 13	eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = 0 )