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\phi$$
6		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}kD$$
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$$