Metamath Proof Explorer

Theorem fprodsplitsn

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

Ref Expression
Hypotheses fprodsplitsn.ph 
|- F/ k ph
fprodsplitsn.kd 
|- F/_ k D
fprodsplitsn.a 
|- ( ph -> A e. Fin )
fprodsplitsn.b 
|- ( ph -> B e. V )
fprodsplitsn.ba 
|- ( ph -> -. B e. A )
fprodsplitsn.c 
|- ( ( ph /\ k e. A ) -> C e. CC )
fprodsplitsn.d 
|- ( k = B -> C = D )
fprodsplitsn.dcn 
|- ( ph -> D e. CC )
Assertion fprodsplitsn 
|- ( ph -> prod_ k e. ( A u. { B } ) C = ( prod_ k e. A C x. D ) )

Proof

Step Hyp Ref Expression
1 fprodsplitsn.ph 
 |-  F/ k ph
2 fprodsplitsn.kd 
 |-  F/_ k D
3 fprodsplitsn.a 
 |-  ( ph -> A e. Fin )
4 fprodsplitsn.b 
 |-  ( ph -> B e. V )
5 fprodsplitsn.ba 
 |-  ( ph -> -. B e. A )
6 fprodsplitsn.c 
 |-  ( ( ph /\ k e. A ) -> C e. CC )
7 fprodsplitsn.d 
 |-  ( k = B -> C = D )
8 fprodsplitsn.dcn 
 |-  ( ph -> D e. CC )
9 disjsn 
 |-  ( ( A i^i { B } ) = (/) <-> -. B e. A )
10 5 9 sylibr 
 |-  ( ph -> ( A i^i { B } ) = (/) )
11 eqidd 
 |-  ( ph -> ( A u. { B } ) = ( A u. { B } ) )
12 snfi 
 |-  { B } e. Fin
13 unfi 
 |-  ( ( A e. Fin /\ { B } e. Fin ) -> ( A u. { B } ) e. Fin )
14 3 12 13 sylancl 
 |-  ( ph -> ( A u. { B } ) e. Fin )
15 6 adantlr 
 |-  ( ( ( ph /\ k e. ( A u. { B } ) ) /\ k e. A ) -> C e. CC )
16 elunnel1 
 |-  ( ( k e. ( A u. { B } ) /\ -. k e. A ) -> k e. { B } )
17 elsni 
 |-  ( k e. { B } -> k = B )
18 16 17 syl 
 |-  ( ( k e. ( A u. { B } ) /\ -. k e. A ) -> k = B )
19 18 adantll 
 |-  ( ( ( ph /\ k e. ( A u. { B } ) ) /\ -. k e. A ) -> k = B )
20 19 7 syl 
 |-  ( ( ( ph /\ k e. ( A u. { B } ) ) /\ -. k e. A ) -> C = D )
21 8 ad2antrr 
 |-  ( ( ( ph /\ k e. ( A u. { B } ) ) /\ -. k e. A ) -> D e. CC )
22 20 21 eqeltrd 
 |-  ( ( ( ph /\ k e. ( A u. { B } ) ) /\ -. k e. A ) -> C e. CC )
23 15 22 pm2.61dan 
 |-  ( ( ph /\ k e. ( A u. { B } ) ) -> C e. CC )
24 1 10 11 14 23 fprodsplitf 
 |-  ( ph -> prod_ k e. ( A u. { B } ) C = ( prod_ k e. A C x. prod_ k e. { B } C ) )
25 2 7 prodsnf 
 |-  ( ( B e. V /\ D e. CC ) -> prod_ k e. { B } C = D )
26 4 8 25 syl2anc 
 |-  ( ph -> prod_ k e. { B } C = D )
27 26 oveq2d 
 |-  ( ph -> ( prod_ k e. A C x. prod_ k e. { B } C ) = ( prod_ k e. A C x. D ) )
28 24 27 eqtrd 
 |-  ( ph -> prod_ k e. ( A u. { B } ) C = ( prod_ k e. A C x. D ) )