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 φAFin
fprodsplit1.b φkAB
fprodsplit1.c φCA
fprodsplit1.d φk=CB=D
Assertion fprodsplit1 φkAB=DkACB

Proof

Step Hyp Ref Expression
1 fprodsplit1.a φAFin
2 fprodsplit1.b φkAB
3 fprodsplit1.c φCA
4 fprodsplit1.d φk=CB=D
5 nfv kφ
6 nfcvd φ_kD
7 5 6 1 2 3 4 fprodsplit1f φkAB=DkACB