Metamath Proof Explorer

Theorem fprodsplit

Description: Split a finite product into two parts. (Contributed by Scott Fenton, 16-Dec-2017)

Ref Expression
Hypotheses fprodsplit.1 
|- ( ph -> ( A i^i B ) = (/) )
fprodsplit.2 
|- ( ph -> U = ( A u. B ) )
fprodsplit.3 
|- ( ph -> U e. Fin )
fprodsplit.4 
|- ( ( ph /\ k e. U ) -> C e. CC )
Assertion fprodsplit 
|- ( ph -> prod_ k e. U C = ( prod_ k e. A C x. prod_ k e. B C ) )

Proof

Step Hyp Ref Expression
1 fprodsplit.1 
 |-  ( ph -> ( A i^i B ) = (/) )
2 fprodsplit.2 
 |-  ( ph -> U = ( A u. B ) )
3 fprodsplit.3 
 |-  ( ph -> U e. Fin )
4 fprodsplit.4 
 |-  ( ( ph /\ k e. U ) -> C e. CC )
5 iftrue 
 |-  ( k e. A -> if ( k e. A , C , 1 ) = C )
6 5 prodeq2i 
 |-  prod_ k e. A if ( k e. A , C , 1 ) = prod_ k e. A C
7 ssun1 
 |-  A C_ ( A u. B )
8 7 2 sseqtrrid 
 |-  ( ph -> A C_ U )
9 5 adantl 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , C , 1 ) = C )
10 8 sselda 
 |-  ( ( ph /\ k e. A ) -> k e. U )
11 10 4 syldan 
 |-  ( ( ph /\ k e. A ) -> C e. CC )
12 9 11 eqeltrd 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , C , 1 ) e. CC )
13 eldifn 
 |-  ( k e. ( U \ A ) -> -. k e. A )
14 13 iffalsed 
 |-  ( k e. ( U \ A ) -> if ( k e. A , C , 1 ) = 1 )
15 14 adantl 
 |-  ( ( ph /\ k e. ( U \ A ) ) -> if ( k e. A , C , 1 ) = 1 )
16 8 12 15 3 fprodss 
 |-  ( ph -> prod_ k e. A if ( k e. A , C , 1 ) = prod_ k e. U if ( k e. A , C , 1 ) )
17 6 16 eqtr3id 
 |-  ( ph -> prod_ k e. A C = prod_ k e. U if ( k e. A , C , 1 ) )
18 iftrue 
 |-  ( k e. B -> if ( k e. B , C , 1 ) = C )
19 18 prodeq2i 
 |-  prod_ k e. B if ( k e. B , C , 1 ) = prod_ k e. B C
20 ssun2 
 |-  B C_ ( A u. B )
21 20 2 sseqtrrid 
 |-  ( ph -> B C_ U )
22 18 adantl 
 |-  ( ( ph /\ k e. B ) -> if ( k e. B , C , 1 ) = C )
23 21 sselda 
 |-  ( ( ph /\ k e. B ) -> k e. U )
24 23 4 syldan 
 |-  ( ( ph /\ k e. B ) -> C e. CC )
25 22 24 eqeltrd 
 |-  ( ( ph /\ k e. B ) -> if ( k e. B , C , 1 ) e. CC )
26 eldifn 
 |-  ( k e. ( U \ B ) -> -. k e. B )
27 26 iffalsed 
 |-  ( k e. ( U \ B ) -> if ( k e. B , C , 1 ) = 1 )
28 27 adantl 
 |-  ( ( ph /\ k e. ( U \ B ) ) -> if ( k e. B , C , 1 ) = 1 )
29 21 25 28 3 fprodss 
 |-  ( ph -> prod_ k e. B if ( k e. B , C , 1 ) = prod_ k e. U if ( k e. B , C , 1 ) )
30 19 29 eqtr3id 
 |-  ( ph -> prod_ k e. B C = prod_ k e. U if ( k e. B , C , 1 ) )
31 17 30 oveq12d 
 |-  ( ph -> ( prod_ k e. A C x. prod_ k e. B C ) = ( prod_ k e. U if ( k e. A , C , 1 ) x. prod_ k e. U if ( k e. B , C , 1 ) ) )
32 ax-1cn 
 |-  1 e. CC
33 ifcl 
 |-  ( ( C e. CC /\ 1 e. CC ) -> if ( k e. A , C , 1 ) e. CC )
34 4 32 33 sylancl 
 |-  ( ( ph /\ k e. U ) -> if ( k e. A , C , 1 ) e. CC )
35 ifcl 
 |-  ( ( C e. CC /\ 1 e. CC ) -> if ( k e. B , C , 1 ) e. CC )
36 4 32 35 sylancl 
 |-  ( ( ph /\ k e. U ) -> if ( k e. B , C , 1 ) e. CC )
37 3 34 36 fprodmul 
 |-  ( ph -> prod_ k e. U ( if ( k e. A , C , 1 ) x. if ( k e. B , C , 1 ) ) = ( prod_ k e. U if ( k e. A , C , 1 ) x. prod_ k e. U if ( k e. B , C , 1 ) ) )
38 2 eleq2d 
 |-  ( ph -> ( k e. U <-> k e. ( A u. B ) ) )
39 elun 
 |-  ( k e. ( A u. B ) <-> ( k e. A \/ k e. B ) )
40 38 39 bitrdi 
 |-  ( ph -> ( k e. U <-> ( k e. A \/ k e. B ) ) )
41 40 biimpa 
 |-  ( ( ph /\ k e. U ) -> ( k e. A \/ k e. B ) )
42 disjel 
 |-  ( ( ( A i^i B ) = (/) /\ k e. A ) -> -. k e. B )
43 1 42 sylan 
 |-  ( ( ph /\ k e. A ) -> -. k e. B )
44 43 iffalsed 
 |-  ( ( ph /\ k e. A ) -> if ( k e. B , C , 1 ) = 1 )
45 9 44 oveq12d 
 |-  ( ( ph /\ k e. A ) -> ( if ( k e. A , C , 1 ) x. if ( k e. B , C , 1 ) ) = ( C x. 1 ) )
46 11 mulid1d 
 |-  ( ( ph /\ k e. A ) -> ( C x. 1 ) = C )
47 45 46 eqtrd 
 |-  ( ( ph /\ k e. A ) -> ( if ( k e. A , C , 1 ) x. if ( k e. B , C , 1 ) ) = C )
48 43 ex 
 |-  ( ph -> ( k e. A -> -. k e. B ) )
49 48 con2d 
 |-  ( ph -> ( k e. B -> -. k e. A ) )
50 49 imp 
 |-  ( ( ph /\ k e. B ) -> -. k e. A )
51 50 iffalsed 
 |-  ( ( ph /\ k e. B ) -> if ( k e. A , C , 1 ) = 1 )
52 51 22 oveq12d 
 |-  ( ( ph /\ k e. B ) -> ( if ( k e. A , C , 1 ) x. if ( k e. B , C , 1 ) ) = ( 1 x. C ) )
53 24 mulid2d 
 |-  ( ( ph /\ k e. B ) -> ( 1 x. C ) = C )
54 52 53 eqtrd 
 |-  ( ( ph /\ k e. B ) -> ( if ( k e. A , C , 1 ) x. if ( k e. B , C , 1 ) ) = C )
55 47 54 jaodan 
 |-  ( ( ph /\ ( k e. A \/ k e. B ) ) -> ( if ( k e. A , C , 1 ) x. if ( k e. B , C , 1 ) ) = C )
56 41 55 syldan 
 |-  ( ( ph /\ k e. U ) -> ( if ( k e. A , C , 1 ) x. if ( k e. B , C , 1 ) ) = C )
57 56 prodeq2dv 
 |-  ( ph -> prod_ k e. U ( if ( k e. A , C , 1 ) x. if ( k e. B , C , 1 ) ) = prod_ k e. U C )
58 31 37 57 3eqtr2rd 
 |-  ( ph -> prod_ k e. U C = ( prod_ k e. A C x. prod_ k e. B C ) )