# Metamath Proof Explorer

## Theorem 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 ${⊢}{k}={K}\to {B}={C}$
fprodeq02.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fprodeq02.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
fprodeq02.k ${⊢}{\phi }\to {K}\in {A}$
fprodeq02.c ${⊢}{\phi }\to {C}=0$
Assertion fprodeq02 ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}=0$

### Proof

Step Hyp Ref Expression
1 fprodeq02.1 ${⊢}{k}={K}\to {B}={C}$
2 fprodeq02.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
3 fprodeq02.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
4 fprodeq02.k ${⊢}{\phi }\to {K}\in {A}$
5 fprodeq02.c ${⊢}{\phi }\to {C}=0$
6 disjdif ${⊢}\left\{{K}\right\}\cap \left({A}\setminus \left\{{K}\right\}\right)=\varnothing$
7 6 a1i ${⊢}{\phi }\to \left\{{K}\right\}\cap \left({A}\setminus \left\{{K}\right\}\right)=\varnothing$
8 4 snssd ${⊢}{\phi }\to \left\{{K}\right\}\subseteq {A}$
9 undif ${⊢}\left\{{K}\right\}\subseteq {A}↔\left\{{K}\right\}\cup \left({A}\setminus \left\{{K}\right\}\right)={A}$
10 8 9 sylib ${⊢}{\phi }\to \left\{{K}\right\}\cup \left({A}\setminus \left\{{K}\right\}\right)={A}$
11 10 eqcomd ${⊢}{\phi }\to {A}=\left\{{K}\right\}\cup \left({A}\setminus \left\{{K}\right\}\right)$
12 7 11 2 3 fprodsplit ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}=\prod _{{k}\in \left\{{K}\right\}}{B}\prod _{{k}\in {A}\setminus \left\{{K}\right\}}{B}$
13 0cnd ${⊢}{\phi }\to 0\in ℂ$
14 5 13 eqeltrd ${⊢}{\phi }\to {C}\in ℂ$
15 1 prodsn ${⊢}\left({K}\in {A}\wedge {C}\in ℂ\right)\to \prod _{{k}\in \left\{{K}\right\}}{B}={C}$
16 4 14 15 syl2anc ${⊢}{\phi }\to \prod _{{k}\in \left\{{K}\right\}}{B}={C}$
17 16 5 eqtrd ${⊢}{\phi }\to \prod _{{k}\in \left\{{K}\right\}}{B}=0$
18 17 oveq1d ${⊢}{\phi }\to \prod _{{k}\in \left\{{K}\right\}}{B}\prod _{{k}\in {A}\setminus \left\{{K}\right\}}{B}=0\cdot \prod _{{k}\in {A}\setminus \left\{{K}\right\}}{B}$
19 diffi ${⊢}{A}\in \mathrm{Fin}\to {A}\setminus \left\{{K}\right\}\in \mathrm{Fin}$
20 2 19 syl ${⊢}{\phi }\to {A}\setminus \left\{{K}\right\}\in \mathrm{Fin}$
21 difssd ${⊢}{\phi }\to {A}\setminus \left\{{K}\right\}\subseteq {A}$
22 21 sselda ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus \left\{{K}\right\}\right)\right)\to {k}\in {A}$
23 22 3 syldan ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus \left\{{K}\right\}\right)\right)\to {B}\in ℂ$
24 20 23 fprodcl ${⊢}{\phi }\to \prod _{{k}\in {A}\setminus \left\{{K}\right\}}{B}\in ℂ$
25 24 mul02d ${⊢}{\phi }\to 0\cdot \prod _{{k}\in {A}\setminus \left\{{K}\right\}}{B}=0$
26 12 18 25 3eqtrd ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}=0$