Theorem fprodsplit1

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

	Ref	Expression
Hypotheses	fprodsplit1.a	|- ( ph -> A e. Fin )
	fprodsplit1.b	|- ( ( ph /\ k e. A ) -> B e. CC )
	fprodsplit1.c	|- ( ph -> C e. A )
	fprodsplit1.d	|- ( ( ph /\ k = C ) -> B = D )
Assertion	fprodsplit1	|- ( ph -> prod_ k e. A B = ( D x. prod_ k e. ( A \ { C } ) B ) )

Proof

Step	Hyp	Ref	Expression
1		fprodsplit1.a	|- ( ph -> A e. Fin )
2		fprodsplit1.b	|- ( ( ph /\ k e. A ) -> B e. CC )
3		fprodsplit1.c	|- ( ph -> C e. A )
4		fprodsplit1.d	|- ( ( ph /\ k = C ) -> B = D )
5		nfv	|- F/ k ph
6		nfcvd	|- ( ph -> F/_ k D )
7	5 6 1 2 3 4	fprodsplit1f	|- ( ph -> prod_ k e. A B = ( D x. prod_ k e. ( A \ { C } ) B ) )