Step | Hyp | Ref
| Expression |
1 | | prodeq1 11450 |
. . 3
⊢ (𝑤 = ∅ → ∏𝑘 ∈ 𝑤 𝐵 = ∏𝑘 ∈ ∅ 𝐵) |
2 | | fveq2 5468 |
. . . 4
⊢ (𝑤 = ∅ →
(♯‘𝑤) =
(♯‘∅)) |
3 | 2 | oveq2d 5840 |
. . 3
⊢ (𝑤 = ∅ → (𝐵↑(♯‘𝑤)) = (𝐵↑(♯‘∅))) |
4 | 1, 3 | eqeq12d 2172 |
. 2
⊢ (𝑤 = ∅ → (∏𝑘 ∈ 𝑤 𝐵 = (𝐵↑(♯‘𝑤)) ↔ ∏𝑘 ∈ ∅ 𝐵 = (𝐵↑(♯‘∅)))) |
5 | | prodeq1 11450 |
. . 3
⊢ (𝑤 = 𝑦 → ∏𝑘 ∈ 𝑤 𝐵 = ∏𝑘 ∈ 𝑦 𝐵) |
6 | | fveq2 5468 |
. . . 4
⊢ (𝑤 = 𝑦 → (♯‘𝑤) = (♯‘𝑦)) |
7 | 6 | oveq2d 5840 |
. . 3
⊢ (𝑤 = 𝑦 → (𝐵↑(♯‘𝑤)) = (𝐵↑(♯‘𝑦))) |
8 | 5, 7 | eqeq12d 2172 |
. 2
⊢ (𝑤 = 𝑦 → (∏𝑘 ∈ 𝑤 𝐵 = (𝐵↑(♯‘𝑤)) ↔ ∏𝑘 ∈ 𝑦 𝐵 = (𝐵↑(♯‘𝑦)))) |
9 | | prodeq1 11450 |
. . 3
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ∏𝑘 ∈ 𝑤 𝐵 = ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵) |
10 | | fveq2 5468 |
. . . 4
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (♯‘𝑤) = (♯‘(𝑦 ∪ {𝑧}))) |
11 | 10 | oveq2d 5840 |
. . 3
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝐵↑(♯‘𝑤)) = (𝐵↑(♯‘(𝑦 ∪ {𝑧})))) |
12 | 9, 11 | eqeq12d 2172 |
. 2
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∏𝑘 ∈ 𝑤 𝐵 = (𝐵↑(♯‘𝑤)) ↔ ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (𝐵↑(♯‘(𝑦 ∪ {𝑧}))))) |
13 | | prodeq1 11450 |
. . 3
⊢ (𝑤 = 𝐴 → ∏𝑘 ∈ 𝑤 𝐵 = ∏𝑘 ∈ 𝐴 𝐵) |
14 | | fveq2 5468 |
. . . 4
⊢ (𝑤 = 𝐴 → (♯‘𝑤) = (♯‘𝐴)) |
15 | 14 | oveq2d 5840 |
. . 3
⊢ (𝑤 = 𝐴 → (𝐵↑(♯‘𝑤)) = (𝐵↑(♯‘𝐴))) |
16 | 13, 15 | eqeq12d 2172 |
. 2
⊢ (𝑤 = 𝐴 → (∏𝑘 ∈ 𝑤 𝐵 = (𝐵↑(♯‘𝑤)) ↔ ∏𝑘 ∈ 𝐴 𝐵 = (𝐵↑(♯‘𝐴)))) |
17 | | prod0 11482 |
. . 3
⊢
∏𝑘 ∈
∅ 𝐵 =
1 |
18 | | hash0 10671 |
. . . . 5
⊢
(♯‘∅) = 0 |
19 | 18 | oveq2i 5835 |
. . . 4
⊢ (𝐵↑(♯‘∅)) =
(𝐵↑0) |
20 | | simpr 109 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) → 𝐵 ∈
ℂ) |
21 | 20 | exp0d 10545 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) → (𝐵↑0) = 1) |
22 | 19, 21 | syl5eq 2202 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) → (𝐵↑(♯‘∅)) =
1) |
23 | 17, 22 | eqtr4id 2209 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) →
∏𝑘 ∈ ∅
𝐵 = (𝐵↑(♯‘∅))) |
24 | | simpr 109 |
. . . . 5
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ ℂ)
∧ 𝑦 ∈ Fin) ∧
(𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 = (𝐵↑(♯‘𝑦))) → ∏𝑘 ∈ 𝑦 𝐵 = (𝐵↑(♯‘𝑦))) |
25 | 24 | oveq1d 5839 |
. . . 4
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ ℂ)
∧ 𝑦 ∈ Fin) ∧
(𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 = (𝐵↑(♯‘𝑦))) → (∏𝑘 ∈ 𝑦 𝐵 · 𝐵) = ((𝐵↑(♯‘𝑦)) · 𝐵)) |
26 | | nfcv 2299 |
. . . . . . 7
⊢
Ⅎ𝑘𝐵 |
27 | | simplr 520 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑦 ∈ Fin) |
28 | | simprr 522 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ (𝐴 ∖ 𝑦)) |
29 | 28 | eldifbd 3114 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ¬ 𝑧 ∈ 𝑦) |
30 | | simp-4r 532 |
. . . . . . 7
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ ℂ)
∧ 𝑦 ∈ Fin) ∧
(𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℂ) |
31 | | simpllr 524 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝐵 ∈ ℂ) |
32 | | eqidd 2158 |
. . . . . . 7
⊢ (𝑘 = 𝑧 → 𝐵 = 𝐵) |
33 | 26, 27, 28, 29, 30, 31, 32 | fprodunsn 11501 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (∏𝑘 ∈ 𝑦 𝐵 · 𝐵)) |
34 | 27, 29 | jca 304 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) |
35 | | hashunsng 10681 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))) |
36 | 28, 34, 35 | sylc 62 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)) |
37 | 36 | oveq2d 5840 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐵↑(♯‘(𝑦 ∪ {𝑧}))) = (𝐵↑((♯‘𝑦) + 1))) |
38 | | hashcl 10655 |
. . . . . . . . 9
⊢ (𝑦 ∈ Fin →
(♯‘𝑦) ∈
ℕ0) |
39 | 27, 38 | syl 14 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘𝑦) ∈
ℕ0) |
40 | 31, 39 | expp1d 10552 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐵↑((♯‘𝑦) + 1)) = ((𝐵↑(♯‘𝑦)) · 𝐵)) |
41 | 37, 40 | eqtrd 2190 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐵↑(♯‘(𝑦 ∪ {𝑧}))) = ((𝐵↑(♯‘𝑦)) · 𝐵)) |
42 | 33, 41 | eqeq12d 2172 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (𝐵↑(♯‘(𝑦 ∪ {𝑧}))) ↔ (∏𝑘 ∈ 𝑦 𝐵 · 𝐵) = ((𝐵↑(♯‘𝑦)) · 𝐵))) |
43 | 42 | adantr 274 |
. . . 4
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ ℂ)
∧ 𝑦 ∈ Fin) ∧
(𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 = (𝐵↑(♯‘𝑦))) → (∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (𝐵↑(♯‘(𝑦 ∪ {𝑧}))) ↔ (∏𝑘 ∈ 𝑦 𝐵 · 𝐵) = ((𝐵↑(♯‘𝑦)) · 𝐵))) |
44 | 25, 43 | mpbird 166 |
. . 3
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ ℂ)
∧ 𝑦 ∈ Fin) ∧
(𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 = (𝐵↑(♯‘𝑦))) → ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (𝐵↑(♯‘(𝑦 ∪ {𝑧})))) |
45 | 44 | ex 114 |
. 2
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (∏𝑘 ∈ 𝑦 𝐵 = (𝐵↑(♯‘𝑦)) → ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (𝐵↑(♯‘(𝑦 ∪ {𝑧}))))) |
46 | | simpl 108 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ Fin) |
47 | 4, 8, 12, 16, 23, 45, 46 | findcard2sd 6837 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) →
∏𝑘 ∈ 𝐴 𝐵 = (𝐵↑(♯‘𝐴))) |