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