Metamath Proof Explorer

Theorem fprodsplit1

Description: Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fprodsplit1.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fprodsplit1.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
fprodsplit1.c ${⊢}{\phi }\to {C}\in {A}$
fprodsplit1.d ${⊢}\left({\phi }\wedge {k}={C}\right)\to {B}={D}$
Assertion fprodsplit1 ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}={D}\prod _{{k}\in {A}\setminus \left\{{C}\right\}}{B}$

Proof

Step Hyp Ref Expression
1 fprodsplit1.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
2 fprodsplit1.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
3 fprodsplit1.c ${⊢}{\phi }\to {C}\in {A}$
4 fprodsplit1.d ${⊢}\left({\phi }\wedge {k}={C}\right)\to {B}={D}$
5 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
6 nfcvd ${⊢}{\phi }\to \underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{D}$
7 5 6 1 2 3 4 fprodsplit1f ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}={D}\prod _{{k}\in {A}\setminus \left\{{C}\right\}}{B}$