Theorem fprodsplitf

Description: Split a finite product into two parts. A version of fprodsplit using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fprodsplitf.kph	|- F/ k ph
	fprodsplitf.in	|- ( ph -> ( A i^i B ) = (/) )
	fprodsplitf.un	|- ( ph -> U = ( A u. B ) )
	fprodsplitf.fi	|- ( ph -> U e. Fin )
	fprodsplitf.c	|- ( ( ph /\ k e. U ) -> C e. CC )
Assertion	fprodsplitf	|- ( ph -> prod_ k e. U C = ( prod_ k e. A C x. prod_ k e. B C ) )

Proof

Step	Hyp	Ref	Expression
1		fprodsplitf.kph	|- F/ k ph
2		fprodsplitf.in	|- ( ph -> ( A i^i B ) = (/) )
3		fprodsplitf.un	|- ( ph -> U = ( A u. B ) )
4		fprodsplitf.fi	|- ( ph -> U e. Fin )
5		fprodsplitf.c	|- ( ( ph /\ k e. U ) -> C e. CC )
6		nfv	|- F/ k j e. U
7	1 6	nfan	|- F/ k ( ph /\ j e. U )
8		nfcsb1v	|- F/_ k [_ j / k ]_ C
9	8	nfel1	|- F/ k [_ j / k ]_ C e. CC
10	7 9	nfim	|- F/ k ( ( ph /\ j e. U ) -> [_ j / k ]_ C e. CC )
11		eleq1w	|- ( k = j -> ( k e. U <-> j e. U ) )
12	11	anbi2d	|- ( k = j -> ( ( ph /\ k e. U ) <-> ( ph /\ j e. U ) ) )
13		csbeq1a	|- ( k = j -> C = [_ j / k ]_ C )
14	13	eleq1d	|- ( k = j -> ( C e. CC <-> [_ j / k ]_ C e. CC ) )
15	12 14	imbi12d	|- ( k = j -> ( ( ( ph /\ k e. U ) -> C e. CC ) <-> ( ( ph /\ j e. U ) -> [_ j / k ]_ C e. CC ) ) )
16	10 15 5	chvarfv	|- ( ( ph /\ j e. U ) -> [_ j / k ]_ C e. CC )
17	2 3 4 16	fprodsplit	|- ( ph -> prod_ j e. U [_ j / k ]_ C = ( prod_ j e. A [_ j / k ]_ C x. prod_ j e. B [_ j / k ]_ C ) )
18		nfcv	|- F/_ j C
19	18 8 13	cbvprodi	|- prod_ k e. U C = prod_ j e. U [_ j / k ]_ C
20	18 8 13	cbvprodi	|- prod_ k e. A C = prod_ j e. A [_ j / k ]_ C
21	18 8 13	cbvprodi	|- prod_ k e. B C = prod_ j e. B [_ j / k ]_ C
22	20 21	oveq12i	|- ( prod_ k e. A C x. prod_ k e. B C ) = ( prod_ j e. A [_ j / k ]_ C x. prod_ j e. B [_ j / k ]_ C )
23	17 19 22	3eqtr4g	|- ( ph -> prod_ k e. U C = ( prod_ k e. A C x. prod_ k e. B C ) )