Theorem fprodsplit1f

Description: Separate out a term in a finite product. A version of fprodsplit1 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		fprodsplit1f.kph	$$⊢Ⅎk\phi$$
2		fprodsplit1f.fk	$$⊢\phi \to \underset{\_}{Ⅎ}kD$$
3		fprodsplit1f.a	$$⊢\phi \to A\in \mathrm{Fin}$$
4		fprodsplit1f.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
5		fprodsplit1f.c	$$⊢\phi \to C\in A$$
6		fprodsplit1f.d	$$⊢\left(\phi \wedge k=C\right)\to B=D$$
7		disjdif	$$⊢\left\{C\right\}\cap \left(A\setminus \left\{C\right\}\right)=\varnothing$$
8	7	a1i	$$⊢\phi \to \left\{C\right\}\cap \left(A\setminus \left\{C\right\}\right)=\varnothing$$
9	5	snssd	$$⊢\phi \to \left\{C\right\}\subseteq A$$
10		undif	$$⊢\left\{C\right\}\subseteq A\leftrightarrow \left\{C\right\}\cup \left(A\setminus \left\{C\right\}\right)=A$$
11	9 10	sylib	$$⊢\phi \to \left\{C\right\}\cup \left(A\setminus \left\{C\right\}\right)=A$$
12	11	eqcomd	$$⊢\phi \to A=\left\{C\right\}\cup \left(A\setminus \left\{C\right\}\right)$$
13	1 8 12 3 4	fprodsplitf	$$⊢\phi \to \prod _{k\in A}B=\prod _{k\in \left\{C\right\}}B\prod _{k\in A\setminus \left\{C\right\}}B$$
14	5	ancli	$$⊢\phi \to \left(\phi \wedge C\in A\right)$$
15		nfv	$$⊢ℲkC\in A$$
16	1 15	nfan	$$⊢Ⅎk\left(\phi \wedge C\in A\right)$$
17		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋C/k⦌B$$
18	17	nfel1	$$⊢Ⅎk⦋C/k⦌B\in ℂ$$
19	16 18	nfim	$$⊢Ⅎk\left(\left(\phi \wedge C\in A\right)\to ⦋C/k⦌B\in ℂ\right)$$
20		eleq1	$$⊢k=C\to \left(k\in A\leftrightarrow C\in A\right)$$
21	20	anbi2d	$$⊢k=C\to \left(\left(\phi \wedge k\in A\right)\leftrightarrow \left(\phi \wedge C\in A\right)\right)$$
22		csbeq1a	$$⊢k=C\to B=⦋C/k⦌B$$
23	22	eleq1d	$$⊢k=C\to \left(B\in ℂ\leftrightarrow ⦋C/k⦌B\in ℂ\right)$$
24	21 23	imbi12d	$$⊢k=C\to \left(\left(\left(\phi \wedge k\in A\right)\to B\in ℂ\right)\leftrightarrow \left(\left(\phi \wedge C\in A\right)\to ⦋C/k⦌B\in ℂ\right)\right)$$
25	19 24 4	vtoclg1f	$$⊢C\in A\to \left(\left(\phi \wedge C\in A\right)\to ⦋C/k⦌B\in ℂ\right)$$
26	5 14 25	sylc	$$⊢\phi \to ⦋C/k⦌B\in ℂ$$
27		prodsns	$$⊢\left(C\in A\wedge ⦋C/k⦌B\in ℂ\right)\to \prod _{k\in \left\{C\right\}}B=⦋C/k⦌B$$
28	5 26 27	syl2anc	$$⊢\phi \to \prod _{k\in \left\{C\right\}}B=⦋C/k⦌B$$
29	1 2 5 6	csbiedf	$$⊢\phi \to ⦋C/k⦌B=D$$
30	28 29	eqtrd	$$⊢\phi \to \prod _{k\in \left\{C\right\}}B=D$$
31	30	oveq1d	$$⊢\phi \to \prod _{k\in \left\{C\right\}}B\prod _{k\in A\setminus \left\{C\right\}}B=D\prod _{k\in A\setminus \left\{C\right\}}B$$
32	13 31	eqtrd	$$⊢\phi \to \prod _{k\in A}B=D\prod _{k\in A\setminus \left\{C\right\}}B$$