Proof of Theorem fprodsplit
Step | Hyp | Ref
| Expression |
1 | | iftrue 4460 |
. . . . 5
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐶, 1) = 𝐶) |
2 | 1 | prodeq2i 15506 |
. . . 4
⊢
∏𝑘 ∈
𝐴 if(𝑘 ∈ 𝐴, 𝐶, 1) = ∏𝑘 ∈ 𝐴 𝐶 |
3 | | ssun1 4101 |
. . . . . 6
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
4 | | fprodsplit.2 |
. . . . . 6
⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) |
5 | 3, 4 | sseqtrrid 3969 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑈) |
6 | 1 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐶, 1) = 𝐶) |
7 | 5 | sselda 3916 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝑈) |
8 | | fprodsplit.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ) |
9 | 7, 8 | syldan 594 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
10 | 6, 9 | eqeltrd 2839 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐶, 1) ∈ ℂ) |
11 | | eldifn 4057 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑈 ∖ 𝐴) → ¬ 𝑘 ∈ 𝐴) |
12 | 11 | iffalsed 4465 |
. . . . . 6
⊢ (𝑘 ∈ (𝑈 ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐶, 1) = 1) |
13 | 12 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∖ 𝐴)) → if(𝑘 ∈ 𝐴, 𝐶, 1) = 1) |
14 | | fprodsplit.3 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ Fin) |
15 | 5, 10, 13, 14 | fprodss 15535 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 if(𝑘 ∈ 𝐴, 𝐶, 1) = ∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 1)) |
16 | 2, 15 | eqtr3id 2793 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 1)) |
17 | | iftrue 4460 |
. . . . 5
⊢ (𝑘 ∈ 𝐵 → if(𝑘 ∈ 𝐵, 𝐶, 1) = 𝐶) |
18 | 17 | prodeq2i 15506 |
. . . 4
⊢
∏𝑘 ∈
𝐵 if(𝑘 ∈ 𝐵, 𝐶, 1) = ∏𝑘 ∈ 𝐵 𝐶 |
19 | | ssun2 4102 |
. . . . . 6
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
20 | 19, 4 | sseqtrrid 3969 |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ 𝑈) |
21 | 17 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐵, 𝐶, 1) = 𝐶) |
22 | 20 | sselda 3916 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝑈) |
23 | 22, 8 | syldan 594 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
24 | 21, 23 | eqeltrd 2839 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐵, 𝐶, 1) ∈ ℂ) |
25 | | eldifn 4057 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑈 ∖ 𝐵) → ¬ 𝑘 ∈ 𝐵) |
26 | 25 | iffalsed 4465 |
. . . . . 6
⊢ (𝑘 ∈ (𝑈 ∖ 𝐵) → if(𝑘 ∈ 𝐵, 𝐶, 1) = 1) |
27 | 26 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∖ 𝐵)) → if(𝑘 ∈ 𝐵, 𝐶, 1) = 1) |
28 | 20, 24, 27, 14 | fprodss 15535 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ 𝐵 if(𝑘 ∈ 𝐵, 𝐶, 1) = ∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 1)) |
29 | 18, 28 | eqtr3id 2793 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 1)) |
30 | 16, 29 | oveq12d 7250 |
. 2
⊢ (𝜑 → (∏𝑘 ∈ 𝐴 𝐶 · ∏𝑘 ∈ 𝐵 𝐶) = (∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 1) · ∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 1))) |
31 | | ax-1cn 10812 |
. . . 4
⊢ 1 ∈
ℂ |
32 | | ifcl 4499 |
. . . 4
⊢ ((𝐶 ∈ ℂ ∧ 1 ∈
ℂ) → if(𝑘 ∈
𝐴, 𝐶, 1) ∈ ℂ) |
33 | 8, 31, 32 | sylancl 589 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → if(𝑘 ∈ 𝐴, 𝐶, 1) ∈ ℂ) |
34 | | ifcl 4499 |
. . . 4
⊢ ((𝐶 ∈ ℂ ∧ 1 ∈
ℂ) → if(𝑘 ∈
𝐵, 𝐶, 1) ∈ ℂ) |
35 | 8, 31, 34 | sylancl 589 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → if(𝑘 ∈ 𝐵, 𝐶, 1) ∈ ℂ) |
36 | 14, 33, 35 | fprodmul 15547 |
. 2
⊢ (𝜑 → ∏𝑘 ∈ 𝑈 (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = (∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 1) · ∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 1))) |
37 | 4 | eleq2d 2824 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ 𝑈 ↔ 𝑘 ∈ (𝐴 ∪ 𝐵))) |
38 | | elun 4078 |
. . . . . 6
⊢ (𝑘 ∈ (𝐴 ∪ 𝐵) ↔ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) |
39 | 37, 38 | bitrdi 290 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝑈 ↔ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵))) |
40 | 39 | biimpa 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) |
41 | | fprodsplit.1 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) |
42 | | disjel 4386 |
. . . . . . . . 9
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 ∈ 𝐵) |
43 | 41, 42 | sylan 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 ∈ 𝐵) |
44 | 43 | iffalsed 4465 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐵, 𝐶, 1) = 1) |
45 | 6, 44 | oveq12d 7250 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = (𝐶 · 1)) |
46 | 9 | mulid1d 10875 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐶 · 1) = 𝐶) |
47 | 45, 46 | eqtrd 2778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = 𝐶) |
48 | 43 | ex 416 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵)) |
49 | 48 | con2d 136 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ 𝐵 → ¬ 𝑘 ∈ 𝐴)) |
50 | 49 | imp 410 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → ¬ 𝑘 ∈ 𝐴) |
51 | 50 | iffalsed 4465 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐴, 𝐶, 1) = 1) |
52 | 51, 21 | oveq12d 7250 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = (1 · 𝐶)) |
53 | 23 | mulid2d 10876 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (1 · 𝐶) = 𝐶) |
54 | 52, 53 | eqtrd 2778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = 𝐶) |
55 | 47, 54 | jaodan 958 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) → (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = 𝐶) |
56 | 40, 55 | syldan 594 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = 𝐶) |
57 | 56 | prodeq2dv 15510 |
. 2
⊢ (𝜑 → ∏𝑘 ∈ 𝑈 (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = ∏𝑘 ∈ 𝑈 𝐶) |
58 | 30, 36, 57 | 3eqtr2rd 2785 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝑈 𝐶 = (∏𝑘 ∈ 𝐴 𝐶 · ∏𝑘 ∈ 𝐵 𝐶)) |