Proof of Theorem fprodsplitdc
Step | Hyp | Ref
| Expression |
1 | | iftrue 3511 |
. . . . 5
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐶, 1) = 𝐶) |
2 | 1 | prodeq2i 11471 |
. . . 4
⊢
∏𝑘 ∈
𝐴 if(𝑘 ∈ 𝐴, 𝐶, 1) = ∏𝑘 ∈ 𝐴 𝐶 |
3 | | ssun1 3271 |
. . . . . 6
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
4 | | fprodsplitdc.2 |
. . . . . 6
⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) |
5 | 3, 4 | sseqtrrid 3179 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑈) |
6 | 1 | adantl 275 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐶, 1) = 𝐶) |
7 | 5 | sselda 3128 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝑈) |
8 | | fprodsplitdc.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ) |
9 | 7, 8 | syldan 280 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
10 | 6, 9 | eqeltrd 2234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐶, 1) ∈ ℂ) |
11 | | fprodsplitdc.a |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ 𝑈 DECID 𝑗 ∈ 𝐴) |
12 | | eldifn 3231 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑈 ∖ 𝐴) → ¬ 𝑘 ∈ 𝐴) |
13 | 12 | iffalsed 3516 |
. . . . . 6
⊢ (𝑘 ∈ (𝑈 ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐶, 1) = 1) |
14 | 13 | adantl 275 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∖ 𝐴)) → if(𝑘 ∈ 𝐴, 𝐶, 1) = 1) |
15 | | fprodsplitdc.3 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ Fin) |
16 | 5, 10, 11, 14, 15 | fprodssdc 11499 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 if(𝑘 ∈ 𝐴, 𝐶, 1) = ∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 1)) |
17 | 2, 16 | eqtr3id 2204 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 1)) |
18 | | iftrue 3511 |
. . . . 5
⊢ (𝑘 ∈ 𝐵 → if(𝑘 ∈ 𝐵, 𝐶, 1) = 𝐶) |
19 | 18 | prodeq2i 11471 |
. . . 4
⊢
∏𝑘 ∈
𝐵 if(𝑘 ∈ 𝐵, 𝐶, 1) = ∏𝑘 ∈ 𝐵 𝐶 |
20 | | ssun2 3272 |
. . . . . 6
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
21 | 20, 4 | sseqtrrid 3179 |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ 𝑈) |
22 | 18 | adantl 275 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐵, 𝐶, 1) = 𝐶) |
23 | 21 | sselda 3128 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝑈) |
24 | 23, 8 | syldan 280 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
25 | 22, 24 | eqeltrd 2234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐵, 𝐶, 1) ∈ ℂ) |
26 | | fprodsplitdc.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) |
27 | | disj 3443 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑗 ∈ 𝐴 ¬ 𝑗 ∈ 𝐵) |
28 | 26, 27 | sylib 121 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ¬ 𝑗 ∈ 𝐵) |
29 | 28 | ad2antrr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) → ∀𝑗 ∈ 𝐴 ¬ 𝑗 ∈ 𝐵) |
30 | 29 | r19.21bi 2545 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) ∧ 𝑗 ∈ 𝐴) → ¬ 𝑗 ∈ 𝐵) |
31 | 30 | olcd 724 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) ∧ 𝑗 ∈ 𝐴) → (𝑗 ∈ 𝐵 ∨ ¬ 𝑗 ∈ 𝐵)) |
32 | | df-dc 821 |
. . . . . . . . . 10
⊢
(DECID 𝑗 ∈ 𝐵 ↔ (𝑗 ∈ 𝐵 ∨ ¬ 𝑗 ∈ 𝐵)) |
33 | 31, 32 | sylibr 133 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) ∧ 𝑗 ∈ 𝐴) → DECID 𝑗 ∈ 𝐵) |
34 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) ∧ ¬ 𝑗 ∈ 𝐴) → ¬ 𝑗 ∈ 𝐴) |
35 | | simpllr 524 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) ∧ ¬ 𝑗 ∈ 𝐴) → 𝑗 ∈ 𝑈) |
36 | 4 | eleq2d 2227 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑗 ∈ 𝑈 ↔ 𝑗 ∈ (𝐴 ∪ 𝐵))) |
37 | 36 | ad3antrrr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) ∧ ¬ 𝑗 ∈ 𝐴) → (𝑗 ∈ 𝑈 ↔ 𝑗 ∈ (𝐴 ∪ 𝐵))) |
38 | 35, 37 | mpbid 146 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) ∧ ¬ 𝑗 ∈ 𝐴) → 𝑗 ∈ (𝐴 ∪ 𝐵)) |
39 | | elun 3249 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (𝐴 ∪ 𝐵) ↔ (𝑗 ∈ 𝐴 ∨ 𝑗 ∈ 𝐵)) |
40 | 38, 39 | sylib 121 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) ∧ ¬ 𝑗 ∈ 𝐴) → (𝑗 ∈ 𝐴 ∨ 𝑗 ∈ 𝐵)) |
41 | 40 | orcomd 719 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) ∧ ¬ 𝑗 ∈ 𝐴) → (𝑗 ∈ 𝐵 ∨ 𝑗 ∈ 𝐴)) |
42 | 34, 41 | ecased 1331 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) ∧ ¬ 𝑗 ∈ 𝐴) → 𝑗 ∈ 𝐵) |
43 | 42 | orcd 723 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) ∧ ¬ 𝑗 ∈ 𝐴) → (𝑗 ∈ 𝐵 ∨ ¬ 𝑗 ∈ 𝐵)) |
44 | 43, 32 | sylibr 133 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) ∧ ¬ 𝑗 ∈ 𝐴) → DECID 𝑗 ∈ 𝐵) |
45 | | exmiddc 822 |
. . . . . . . . . 10
⊢
(DECID 𝑗 ∈ 𝐴 → (𝑗 ∈ 𝐴 ∨ ¬ 𝑗 ∈ 𝐴)) |
46 | 45 | adantl 275 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) → (𝑗 ∈ 𝐴 ∨ ¬ 𝑗 ∈ 𝐴)) |
47 | 33, 44, 46 | mpjaodan 788 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑈) ∧ DECID 𝑗 ∈ 𝐴) → DECID 𝑗 ∈ 𝐵) |
48 | 47 | ex 114 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑈) → (DECID 𝑗 ∈ 𝐴 → DECID 𝑗 ∈ 𝐵)) |
49 | 48 | ralimdva 2524 |
. . . . . 6
⊢ (𝜑 → (∀𝑗 ∈ 𝑈 DECID 𝑗 ∈ 𝐴 → ∀𝑗 ∈ 𝑈 DECID 𝑗 ∈ 𝐵)) |
50 | 11, 49 | mpd 13 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ 𝑈 DECID 𝑗 ∈ 𝐵) |
51 | | eldifn 3231 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑈 ∖ 𝐵) → ¬ 𝑘 ∈ 𝐵) |
52 | 51 | iffalsed 3516 |
. . . . . 6
⊢ (𝑘 ∈ (𝑈 ∖ 𝐵) → if(𝑘 ∈ 𝐵, 𝐶, 1) = 1) |
53 | 52 | adantl 275 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∖ 𝐵)) → if(𝑘 ∈ 𝐵, 𝐶, 1) = 1) |
54 | 21, 25, 50, 53, 15 | fprodssdc 11499 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ 𝐵 if(𝑘 ∈ 𝐵, 𝐶, 1) = ∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 1)) |
55 | 19, 54 | eqtr3id 2204 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 1)) |
56 | 17, 55 | oveq12d 5845 |
. 2
⊢ (𝜑 → (∏𝑘 ∈ 𝐴 𝐶 · ∏𝑘 ∈ 𝐵 𝐶) = (∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 1) · ∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 1))) |
57 | | 1cnd 7897 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 1 ∈ ℂ) |
58 | | eleq1w 2218 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴)) |
59 | 58 | dcbid 824 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑘 ∈ 𝐴)) |
60 | 59 | cbvralv 2680 |
. . . . . 6
⊢
(∀𝑗 ∈
𝑈 DECID
𝑗 ∈ 𝐴 ↔ ∀𝑘 ∈ 𝑈 DECID 𝑘 ∈ 𝐴) |
61 | 11, 60 | sylib 121 |
. . . . 5
⊢ (𝜑 → ∀𝑘 ∈ 𝑈 DECID 𝑘 ∈ 𝐴) |
62 | 61 | r19.21bi 2545 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → DECID 𝑘 ∈ 𝐴) |
63 | 8, 57, 62 | ifcldcd 3541 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → if(𝑘 ∈ 𝐴, 𝐶, 1) ∈ ℂ) |
64 | | eleq1w 2218 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐵 ↔ 𝑘 ∈ 𝐵)) |
65 | 64 | dcbid 824 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (DECID 𝑗 ∈ 𝐵 ↔ DECID 𝑘 ∈ 𝐵)) |
66 | 65 | cbvralv 2680 |
. . . . . 6
⊢
(∀𝑗 ∈
𝑈 DECID
𝑗 ∈ 𝐵 ↔ ∀𝑘 ∈ 𝑈 DECID 𝑘 ∈ 𝐵) |
67 | 50, 66 | sylib 121 |
. . . . 5
⊢ (𝜑 → ∀𝑘 ∈ 𝑈 DECID 𝑘 ∈ 𝐵) |
68 | 67 | r19.21bi 2545 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → DECID 𝑘 ∈ 𝐵) |
69 | 8, 57, 68 | ifcldcd 3541 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → if(𝑘 ∈ 𝐵, 𝐶, 1) ∈ ℂ) |
70 | 15, 63, 69 | fprodmul 11500 |
. 2
⊢ (𝜑 → ∏𝑘 ∈ 𝑈 (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = (∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 1) · ∏𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 1))) |
71 | 4 | eleq2d 2227 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ 𝑈 ↔ 𝑘 ∈ (𝐴 ∪ 𝐵))) |
72 | | elun 3249 |
. . . . . 6
⊢ (𝑘 ∈ (𝐴 ∪ 𝐵) ↔ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) |
73 | 71, 72 | bitrdi 195 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝑈 ↔ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵))) |
74 | 73 | biimpa 294 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) |
75 | | disjel 3449 |
. . . . . . . . 9
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 ∈ 𝐵) |
76 | 26, 75 | sylan 281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 ∈ 𝐵) |
77 | 76 | iffalsed 3516 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐵, 𝐶, 1) = 1) |
78 | 6, 77 | oveq12d 5845 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = (𝐶 · 1)) |
79 | 9 | mulid1d 7898 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐶 · 1) = 𝐶) |
80 | 78, 79 | eqtrd 2190 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = 𝐶) |
81 | 76 | ex 114 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵)) |
82 | 81 | con2d 614 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ 𝐵 → ¬ 𝑘 ∈ 𝐴)) |
83 | 82 | imp 123 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → ¬ 𝑘 ∈ 𝐴) |
84 | 83 | iffalsed 3516 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐴, 𝐶, 1) = 1) |
85 | 84, 22 | oveq12d 5845 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = (1 · 𝐶)) |
86 | 24 | mulid2d 7899 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (1 · 𝐶) = 𝐶) |
87 | 85, 86 | eqtrd 2190 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = 𝐶) |
88 | 80, 87 | jaodan 787 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) → (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = 𝐶) |
89 | 74, 88 | syldan 280 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = 𝐶) |
90 | 89 | prodeq2dv 11475 |
. 2
⊢ (𝜑 → ∏𝑘 ∈ 𝑈 (if(𝑘 ∈ 𝐴, 𝐶, 1) · if(𝑘 ∈ 𝐵, 𝐶, 1)) = ∏𝑘 ∈ 𝑈 𝐶) |
91 | 56, 70, 90 | 3eqtr2rd 2197 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝑈 𝐶 = (∏𝑘 ∈ 𝐴 𝐶 · ∏𝑘 ∈ 𝐵 𝐶)) |