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

Metamath Proof Explorer

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 )