Metamath Proof Explorer

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 
|- F/ k ph
fprodsplit1f.fk 
|- ( ph -> F/_ k D )
fprodsplit1f.a 
|- ( ph -> A e. Fin )
fprodsplit1f.b 
|- ( ( ph /\ k e. A ) -> B e. CC )
fprodsplit1f.c 
|- ( ph -> C e. A )
fprodsplit1f.d 
|- ( ( ph /\ k = C ) -> B = D )
Assertion fprodsplit1f 
|- ( ph -> prod_ k e. A B = ( D x. prod_ k e. ( A \ { C } ) B ) )

Proof

Step Hyp Ref Expression
1 fprodsplit1f.kph 
 |-  F/ k ph
2 fprodsplit1f.fk 
 |-  ( ph -> F/_ k D )
3 fprodsplit1f.a 
 |-  ( ph -> A e. Fin )
4 fprodsplit1f.b 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
5 fprodsplit1f.c 
 |-  ( ph -> C e. A )
6 fprodsplit1f.d 
 |-  ( ( ph /\ k = C ) -> B = D )
7 disjdif 
 |-  ( { C } i^i ( A \ { C } ) ) = (/)
8 7 a1i 
 |-  ( ph -> ( { C } i^i ( A \ { C } ) ) = (/) )
9 5 snssd 
 |-  ( ph -> { C } C_ A )
10 undif 
 |-  ( { C } C_ A <-> ( { C } u. ( A \ { C } ) ) = A )
11 9 10 sylib 
 |-  ( ph -> ( { C } u. ( A \ { C } ) ) = A )
12 11 eqcomd 
 |-  ( ph -> A = ( { C } u. ( A \ { C } ) ) )
13 1 8 12 3 4 fprodsplitf 
 |-  ( ph -> prod_ k e. A B = ( prod_ k e. { C } B x. prod_ k e. ( A \ { C } ) B ) )
14 5 ancli 
 |-  ( ph -> ( ph /\ C e. A ) )
15 nfv 
 |-  F/ k C e. A
16 1 15 nfan 
 |-  F/ k ( ph /\ C e. A )
17 nfcsb1v 
 |-  F/_ k [_ C / k ]_ B
18 17 nfel1 
 |-  F/ k [_ C / k ]_ B e. CC
19 16 18 nfim 
 |-  F/ k ( ( ph /\ C e. A ) -> [_ C / k ]_ B e. CC )
20 eleq1 
 |-  ( k = C -> ( k e. A <-> C e. A ) )
21 20 anbi2d 
 |-  ( k = C -> ( ( ph /\ k e. A ) <-> ( ph /\ C e. A ) ) )
22 csbeq1a 
 |-  ( k = C -> B = [_ C / k ]_ B )
23 22 eleq1d 
 |-  ( k = C -> ( B e. CC <-> [_ C / k ]_ B e. CC ) )
24 21 23 imbi12d 
 |-  ( k = C -> ( ( ( ph /\ k e. A ) -> B e. CC ) <-> ( ( ph /\ C e. A ) -> [_ C / k ]_ B e. CC ) ) )
25 19 24 4 vtoclg1f 
 |-  ( C e. A -> ( ( ph /\ C e. A ) -> [_ C / k ]_ B e. CC ) )
26 5 14 25 sylc 
 |-  ( ph -> [_ C / k ]_ B e. CC )
27 prodsns 
 |-  ( ( C e. A /\ [_ C / k ]_ B e. CC ) -> prod_ k e. { C } B = [_ C / k ]_ B )
28 5 26 27 syl2anc 
 |-  ( ph -> prod_ k e. { C } B = [_ C / k ]_ B )
29 1 2 5 6 csbiedf 
 |-  ( ph -> [_ C / k ]_ B = D )
30 28 29 eqtrd 
 |-  ( ph -> prod_ k e. { C } B = D )
31 30 oveq1d 
 |-  ( ph -> ( prod_ k e. { C } B x. prod_ k e. ( A \ { C } ) B ) = ( D x. prod_ k e. ( A \ { C } ) B ) )
32 13 31 eqtrd 
 |-  ( ph -> prod_ k e. A B = ( D x. prod_ k e. ( A \ { C } ) B ) )