# 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 ${⊢}{\phi }\to {A}\cap {B}=\varnothing$
fprodsplit.2 ${⊢}{\phi }\to {U}={A}\cup {B}$
fprodsplit.3 ${⊢}{\phi }\to {U}\in \mathrm{Fin}$
fprodsplit.4 ${⊢}\left({\phi }\wedge {k}\in {U}\right)\to {C}\in ℂ$
Assertion fprodsplit ${⊢}{\phi }\to \prod _{{k}\in {U}}{C}=\prod _{{k}\in {A}}{C}\prod _{{k}\in {B}}{C}$

### Proof

Step Hyp Ref Expression
1 fprodsplit.1 ${⊢}{\phi }\to {A}\cap {B}=\varnothing$
2 fprodsplit.2 ${⊢}{\phi }\to {U}={A}\cup {B}$
3 fprodsplit.3 ${⊢}{\phi }\to {U}\in \mathrm{Fin}$
4 fprodsplit.4 ${⊢}\left({\phi }\wedge {k}\in {U}\right)\to {C}\in ℂ$
5 iftrue ${⊢}{k}\in {A}\to if\left({k}\in {A},{C},1\right)={C}$
6 5 prodeq2i ${⊢}\prod _{{k}\in {A}}if\left({k}\in {A},{C},1\right)=\prod _{{k}\in {A}}{C}$
7 ssun1 ${⊢}{A}\subseteq {A}\cup {B}$
8 7 2 sseqtrrid ${⊢}{\phi }\to {A}\subseteq {U}$
9 5 adantl ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to if\left({k}\in {A},{C},1\right)={C}$
10 8 sselda ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {k}\in {U}$
11 10 4 syldan ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in ℂ$
12 9 11 eqeltrd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to if\left({k}\in {A},{C},1\right)\in ℂ$
13 eldifn ${⊢}{k}\in \left({U}\setminus {A}\right)\to ¬{k}\in {A}$
14 13 iffalsed ${⊢}{k}\in \left({U}\setminus {A}\right)\to if\left({k}\in {A},{C},1\right)=1$
15 14 adantl ${⊢}\left({\phi }\wedge {k}\in \left({U}\setminus {A}\right)\right)\to if\left({k}\in {A},{C},1\right)=1$
16 8 12 15 3 fprodss ${⊢}{\phi }\to \prod _{{k}\in {A}}if\left({k}\in {A},{C},1\right)=\prod _{{k}\in {U}}if\left({k}\in {A},{C},1\right)$
17 6 16 syl5eqr ${⊢}{\phi }\to \prod _{{k}\in {A}}{C}=\prod _{{k}\in {U}}if\left({k}\in {A},{C},1\right)$
18 iftrue ${⊢}{k}\in {B}\to if\left({k}\in {B},{C},1\right)={C}$
19 18 prodeq2i ${⊢}\prod _{{k}\in {B}}if\left({k}\in {B},{C},1\right)=\prod _{{k}\in {B}}{C}$
20 ssun2 ${⊢}{B}\subseteq {A}\cup {B}$
21 20 2 sseqtrrid ${⊢}{\phi }\to {B}\subseteq {U}$
22 18 adantl ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to if\left({k}\in {B},{C},1\right)={C}$
23 21 sselda ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to {k}\in {U}$
24 23 4 syldan ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to {C}\in ℂ$
25 22 24 eqeltrd ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to if\left({k}\in {B},{C},1\right)\in ℂ$
26 eldifn ${⊢}{k}\in \left({U}\setminus {B}\right)\to ¬{k}\in {B}$
27 26 iffalsed ${⊢}{k}\in \left({U}\setminus {B}\right)\to if\left({k}\in {B},{C},1\right)=1$
28 27 adantl ${⊢}\left({\phi }\wedge {k}\in \left({U}\setminus {B}\right)\right)\to if\left({k}\in {B},{C},1\right)=1$
29 21 25 28 3 fprodss ${⊢}{\phi }\to \prod _{{k}\in {B}}if\left({k}\in {B},{C},1\right)=\prod _{{k}\in {U}}if\left({k}\in {B},{C},1\right)$
30 19 29 syl5eqr ${⊢}{\phi }\to \prod _{{k}\in {B}}{C}=\prod _{{k}\in {U}}if\left({k}\in {B},{C},1\right)$
31 17 30 oveq12d ${⊢}{\phi }\to \prod _{{k}\in {A}}{C}\prod _{{k}\in {B}}{C}=\prod _{{k}\in {U}}if\left({k}\in {A},{C},1\right)\prod _{{k}\in {U}}if\left({k}\in {B},{C},1\right)$
32 ax-1cn ${⊢}1\in ℂ$
33 ifcl ${⊢}\left({C}\in ℂ\wedge 1\in ℂ\right)\to if\left({k}\in {A},{C},1\right)\in ℂ$
34 4 32 33 sylancl ${⊢}\left({\phi }\wedge {k}\in {U}\right)\to if\left({k}\in {A},{C},1\right)\in ℂ$
35 ifcl ${⊢}\left({C}\in ℂ\wedge 1\in ℂ\right)\to if\left({k}\in {B},{C},1\right)\in ℂ$
36 4 32 35 sylancl ${⊢}\left({\phi }\wedge {k}\in {U}\right)\to if\left({k}\in {B},{C},1\right)\in ℂ$
37 3 34 36 fprodmul ${⊢}{\phi }\to \prod _{{k}\in {U}}if\left({k}\in {A},{C},1\right)if\left({k}\in {B},{C},1\right)=\prod _{{k}\in {U}}if\left({k}\in {A},{C},1\right)\prod _{{k}\in {U}}if\left({k}\in {B},{C},1\right)$
38 2 eleq2d ${⊢}{\phi }\to \left({k}\in {U}↔{k}\in \left({A}\cup {B}\right)\right)$
39 elun ${⊢}{k}\in \left({A}\cup {B}\right)↔\left({k}\in {A}\vee {k}\in {B}\right)$
40 38 39 syl6bb ${⊢}{\phi }\to \left({k}\in {U}↔\left({k}\in {A}\vee {k}\in {B}\right)\right)$
41 40 biimpa ${⊢}\left({\phi }\wedge {k}\in {U}\right)\to \left({k}\in {A}\vee {k}\in {B}\right)$
42 disjel ${⊢}\left({A}\cap {B}=\varnothing \wedge {k}\in {A}\right)\to ¬{k}\in {B}$
43 1 42 sylan ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to ¬{k}\in {B}$
44 43 iffalsed ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to if\left({k}\in {B},{C},1\right)=1$
45 9 44 oveq12d ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to if\left({k}\in {A},{C},1\right)if\left({k}\in {B},{C},1\right)={C}\cdot 1$
46 11 mulid1d ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\cdot 1={C}$
47 45 46 eqtrd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to if\left({k}\in {A},{C},1\right)if\left({k}\in {B},{C},1\right)={C}$
48 43 ex ${⊢}{\phi }\to \left({k}\in {A}\to ¬{k}\in {B}\right)$
49 48 con2d ${⊢}{\phi }\to \left({k}\in {B}\to ¬{k}\in {A}\right)$
50 49 imp ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to ¬{k}\in {A}$
51 50 iffalsed ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to if\left({k}\in {A},{C},1\right)=1$
52 51 22 oveq12d ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to if\left({k}\in {A},{C},1\right)if\left({k}\in {B},{C},1\right)=1{C}$
53 24 mulid2d ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to 1{C}={C}$
54 52 53 eqtrd ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to if\left({k}\in {A},{C},1\right)if\left({k}\in {B},{C},1\right)={C}$
55 47 54 jaodan ${⊢}\left({\phi }\wedge \left({k}\in {A}\vee {k}\in {B}\right)\right)\to if\left({k}\in {A},{C},1\right)if\left({k}\in {B},{C},1\right)={C}$
56 41 55 syldan ${⊢}\left({\phi }\wedge {k}\in {U}\right)\to if\left({k}\in {A},{C},1\right)if\left({k}\in {B},{C},1\right)={C}$
57 56 prodeq2dv ${⊢}{\phi }\to \prod _{{k}\in {U}}if\left({k}\in {A},{C},1\right)if\left({k}\in {B},{C},1\right)=\prod _{{k}\in {U}}{C}$
58 31 37 57 3eqtr2rd ${⊢}{\phi }\to \prod _{{k}\in {U}}{C}=\prod _{{k}\in {A}}{C}\prod _{{k}\in {B}}{C}$