This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )