fprodeq02

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

	Ref	Expression
Hypotheses	fprodeq02.1	⊢ ( 𝑘 = 𝐾 → 𝐵 = 𝐶 )
	fprodeq02.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprodeq02.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	fprodeq02.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐴 )
	fprodeq02.c	⊢ ( 𝜑 → 𝐶 = 0 )
Assertion	fprodeq02	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = 0 )

Proof

Step	Hyp	Ref	Expression
1		fprodeq02.1	⊢ ( 𝑘 = 𝐾 → 𝐵 = 𝐶 )
2		fprodeq02.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fprodeq02.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4		fprodeq02.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐴 )
5		fprodeq02.c	⊢ ( 𝜑 → 𝐶 = 0 )
6		disjdif	⊢ ( { 𝐾 } ∩ ( 𝐴 ∖ { 𝐾 } ) ) = ∅
7	6	a1i	⊢ ( 𝜑 → ( { 𝐾 } ∩ ( 𝐴 ∖ { 𝐾 } ) ) = ∅ )
8	4	snssd	⊢ ( 𝜑 → { 𝐾 } ⊆ 𝐴 )
9		undif	⊢ ( { 𝐾 } ⊆ 𝐴 ↔ ( { 𝐾 } ∪ ( 𝐴 ∖ { 𝐾 } ) ) = 𝐴 )
10	8 9	sylib	⊢ ( 𝜑 → ( { 𝐾 } ∪ ( 𝐴 ∖ { 𝐾 } ) ) = 𝐴 )
11	10	eqcomd	⊢ ( 𝜑 → 𝐴 = ( { 𝐾 } ∪ ( 𝐴 ∖ { 𝐾 } ) ) )
12	7 11 2 3	fprodsplit	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = ( ∏ 𝑘 ∈ { 𝐾 } 𝐵 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) 𝐵 ) )
13		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
14	5 13	eqeltrd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
15	1	prodsn	⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝐶 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝐾 } 𝐵 = 𝐶 )
16	4 14 15	syl2anc	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐾 } 𝐵 = 𝐶 )
17	16 5	eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐾 } 𝐵 = 0 )
18	17	oveq1d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ { 𝐾 } 𝐵 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) 𝐵 ) = ( 0 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) 𝐵 ) )
19		diffi	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ { 𝐾 } ) ∈ Fin )
20	2 19	syl	⊢ ( 𝜑 → ( 𝐴 ∖ { 𝐾 } ) ∈ Fin )
21		difssd	⊢ ( 𝜑 → ( 𝐴 ∖ { 𝐾 } ) ⊆ 𝐴 )
22	21	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) ) → 𝑘 ∈ 𝐴 )
23	22 3	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) ) → 𝐵 ∈ ℂ )
24	20 23	fprodcl	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) 𝐵 ∈ ℂ )
25	24	mul02d	⊢ ( 𝜑 → ( 0 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐾 } ) 𝐵 ) = 0 )
26	12 18 25	3eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = 0 )

Metamath Proof Explorer

Theorem fprodeq02

Proof