This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )