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 ⊢ φ → A ∩ B = ∅
fprodsplit.2 ⊢ φ → U = A ∪ B
fprodsplit.3 ⊢ φ → U ∈ Fin
fprodsplit.4 ⊢ φ ∧ k ∈ U → C ∈ ℂ
Assertion fprodsplit ⊢ φ → ∏ k ∈ U C = ∏ k ∈ A C ⁢ ∏ k ∈ B C

Proof

Step Hyp Ref Expression
1 fprodsplit.1 ⊢ φ → A ∩ B = ∅
2 fprodsplit.2 ⊢ φ → U = A ∪ B
3 fprodsplit.3 ⊢ φ → U ∈ Fin
4 fprodsplit.4 ⊢ φ ∧ k ∈ U → C ∈ ℂ
5 iftrue ⊢ k ∈ A → if k ∈ A C 1 = C
6 5 prodeq2i ⊢ ∏ k ∈ A if k ∈ A C 1 = ∏ k ∈ A C
7 ssun1 ⊢ A ⊆ A ∪ B
8 7 2 sseqtrrid ⊢ φ → A ⊆ U
9 5 adantl ⊢ φ ∧ k ∈ A → if k ∈ A C 1 = C
10 8 sselda ⊢ φ ∧ k ∈ A → k ∈ U
11 10 4 syldan ⊢ φ ∧ k ∈ A → C ∈ ℂ
12 9 11 eqeltrd ⊢ φ ∧ k ∈ A → if k ∈ A C 1 ∈ ℂ
13 eldifn ⊢ k ∈ U ∖ A → ¬ k ∈ A
14 13 iffalsed ⊢ k ∈ U ∖ A → if k ∈ A C 1 = 1
15 14 adantl ⊢ φ ∧ k ∈ U ∖ A → if k ∈ A C 1 = 1
16 8 12 15 3 fprodss ⊢ φ → ∏ k ∈ A if k ∈ A C 1 = ∏ k ∈ U if k ∈ A C 1
17 6 16 eqtr3id ⊢ φ → ∏ k ∈ A C = ∏ k ∈ U if k ∈ A C 1
18 iftrue ⊢ k ∈ B → if k ∈ B C 1 = C
19 18 prodeq2i ⊢ ∏ k ∈ B if k ∈ B C 1 = ∏ k ∈ B C
20 ssun2 ⊢ B ⊆ A ∪ B
21 20 2 sseqtrrid ⊢ φ → B ⊆ U
22 18 adantl ⊢ φ ∧ k ∈ B → if k ∈ B C 1 = C
23 21 sselda ⊢ φ ∧ k ∈ B → k ∈ U
24 23 4 syldan ⊢ φ ∧ k ∈ B → C ∈ ℂ
25 22 24 eqeltrd ⊢ φ ∧ k ∈ B → if k ∈ B C 1 ∈ ℂ
26 eldifn ⊢ k ∈ U ∖ B → ¬ k ∈ B
27 26 iffalsed ⊢ k ∈ U ∖ B → if k ∈ B C 1 = 1
28 27 adantl ⊢ φ ∧ k ∈ U ∖ B → if k ∈ B C 1 = 1
29 21 25 28 3 fprodss ⊢ φ → ∏ k ∈ B if k ∈ B C 1 = ∏ k ∈ U if k ∈ B C 1
30 19 29 eqtr3id ⊢ φ → ∏ k ∈ B C = ∏ k ∈ U if k ∈ B C 1
31 17 30 oveq12d ⊢ φ → ∏ k ∈ A C ⁢ ∏ k ∈ B C = ∏ k ∈ U if k ∈ A C 1 ⁢ ∏ k ∈ U if k ∈ B C 1
32 ax-1cn ⊢ 1 ∈ ℂ
33 ifcl ⊢ C ∈ ℂ ∧ 1 ∈ ℂ → if k ∈ A C 1 ∈ ℂ
34 4 32 33 sylancl ⊢ φ ∧ k ∈ U → if k ∈ A C 1 ∈ ℂ
35 ifcl ⊢ C ∈ ℂ ∧ 1 ∈ ℂ → if k ∈ B C 1 ∈ ℂ
36 4 32 35 sylancl ⊢ φ ∧ k ∈ U → if k ∈ B C 1 ∈ ℂ
37 3 34 36 fprodmul ⊢ φ → ∏ k ∈ U if k ∈ A C 1 ⁢ if k ∈ B C 1 = ∏ k ∈ U if k ∈ A C 1 ⁢ ∏ k ∈ U if k ∈ B C 1
38 2 eleq2d ⊢ φ → k ∈ U ↔ k ∈ A ∪ B
39 elun ⊢ k ∈ A ∪ B ↔ k ∈ A ∨ k ∈ B
40 38 39 bitrdi ⊢ φ → k ∈ U ↔ k ∈ A ∨ k ∈ B
41 40 biimpa ⊢ φ ∧ k ∈ U → k ∈ A ∨ k ∈ B
42 disjel ⊢ A ∩ B = ∅ ∧ k ∈ A → ¬ k ∈ B
43 1 42 sylan ⊢ φ ∧ k ∈ A → ¬ k ∈ B
44 43 iffalsed ⊢ φ ∧ k ∈ A → if k ∈ B C 1 = 1
45 9 44 oveq12d ⊢ φ ∧ k ∈ A → if k ∈ A C 1 ⁢ if k ∈ B C 1 = C ⋅ 1
46 11 mulid1d ⊢ φ ∧ k ∈ A → C ⋅ 1 = C
47 45 46 eqtrd ⊢ φ ∧ k ∈ A → if k ∈ A C 1 ⁢ if k ∈ B C 1 = C
48 43 ex ⊢ φ → k ∈ A → ¬ k ∈ B
49 48 con2d ⊢ φ → k ∈ B → ¬ k ∈ A
50 49 imp ⊢ φ ∧ k ∈ B → ¬ k ∈ A
51 50 iffalsed ⊢ φ ∧ k ∈ B → if k ∈ A C 1 = 1
52 51 22 oveq12d ⊢ φ ∧ k ∈ B → if k ∈ A C 1 ⁢ if k ∈ B C 1 = 1 ⁢ C
53 24 mulid2d ⊢ φ ∧ k ∈ B → 1 ⁢ C = C
54 52 53 eqtrd ⊢ φ ∧ k ∈ B → if k ∈ A C 1 ⁢ if k ∈ B C 1 = C
55 47 54 jaodan ⊢ φ ∧ k ∈ A ∨ k ∈ B → if k ∈ A C 1 ⁢ if k ∈ B C 1 = C
56 41 55 syldan ⊢ φ ∧ k ∈ U → if k ∈ A C 1 ⁢ if k ∈ B C 1 = C
57 56 prodeq2dv ⊢ φ → ∏ k ∈ U if k ∈ A C 1 ⁢ if k ∈ B C 1 = ∏ k ∈ U C
58 31 37 57 3eqtr2rd ⊢ φ → ∏ k ∈ U C = ∏ k ∈ A C ⁢ ∏ k ∈ B C