Step | Hyp | Ref
| Expression |
1 | | unieq 4876 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∪ ∅) |
2 | | uni0 4896 |
. . . . . . . . . . 11
⊢ ∪ ∅ = ∅ |
3 | 1, 2 | eqtrdi 2792 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∅) |
4 | 3 | ineq2d 4172 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) =
(𝑏 ∩
∅)) |
5 | | in0 4351 |
. . . . . . . . 9
⊢ (𝑏 ∩ ∅) =
∅ |
6 | 4, 5 | eqtrdi 2792 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) =
∅) |
7 | 6 | fveq2d 6846 |
. . . . . . 7
⊢ (𝑥 = ∅ →
(♯‘(𝑏 ∩
∪ 𝑥)) =
(♯‘∅)) |
8 | | hash0 14267 |
. . . . . . 7
⊢
(♯‘∅) = 0 |
9 | 7, 8 | eqtrdi 2792 |
. . . . . 6
⊢ (𝑥 = ∅ →
(♯‘(𝑏 ∩
∪ 𝑥)) = 0) |
10 | 9 | oveq2d 7373 |
. . . . 5
⊢ (𝑥 = ∅ →
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑥))) = ((♯‘𝑏) − 0)) |
11 | | pweq 4574 |
. . . . . . 7
⊢ (𝑥 = ∅ → 𝒫
𝑥 = 𝒫
∅) |
12 | | pw0 4772 |
. . . . . . 7
⊢ 𝒫
∅ = {∅} |
13 | 11, 12 | eqtrdi 2792 |
. . . . . 6
⊢ (𝑥 = ∅ → 𝒫
𝑥 =
{∅}) |
14 | 13 | sumeq1d 15586 |
. . . . 5
⊢ (𝑥 = ∅ → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = Σ𝑠 ∈ {∅}
((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) |
15 | 10, 14 | eqeq12d 2752 |
. . . 4
⊢ (𝑥 = ∅ →
(((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑏)
− 0) = Σ𝑠
∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
16 | 15 | ralbidv 3174 |
. . 3
⊢ (𝑥 = ∅ → (∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑏 ∈ Fin
((♯‘𝑏) −
0) = Σ𝑠 ∈
{∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
17 | | unieq 4876 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ∪ 𝑥 = ∪
𝑦) |
18 | 17 | ineq2d 4172 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝑦)) |
19 | 18 | fveq2d 6846 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ ∪ 𝑦))) |
20 | 19 | oveq2d 7373 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))) |
21 | | pweq 4574 |
. . . . . 6
⊢ (𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦) |
22 | 21 | sumeq1d 15586 |
. . . . 5
⊢ (𝑥 = 𝑦 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) |
23 | 20, 22 | eqeq12d 2752 |
. . . 4
⊢ (𝑥 = 𝑦 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑏)
− (♯‘(𝑏
∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
24 | 23 | ralbidv 3174 |
. . 3
⊢ (𝑥 = 𝑦 → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥)))
= Σ𝑠 ∈ 𝒫
𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
25 | | unieq 4876 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = ∪
(𝑦 ∪ {𝑧})) |
26 | | uniun 4891 |
. . . . . . . . . 10
⊢ ∪ (𝑦
∪ {𝑧}) = (∪ 𝑦
∪ ∪ {𝑧}) |
27 | | unisnv 4888 |
. . . . . . . . . . 11
⊢ ∪ {𝑧}
= 𝑧 |
28 | 27 | uneq2i 4120 |
. . . . . . . . . 10
⊢ (∪ 𝑦
∪ ∪ {𝑧}) = (∪ 𝑦 ∪ 𝑧) |
29 | 26, 28 | eqtri 2764 |
. . . . . . . . 9
⊢ ∪ (𝑦
∪ {𝑧}) = (∪ 𝑦
∪ 𝑧) |
30 | 25, 29 | eqtrdi 2792 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = (∪
𝑦 ∪ 𝑧)) |
31 | 30 | ineq2d 4172 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ (∪ 𝑦 ∪ 𝑧))) |
32 | 31 | fveq2d 6846 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ (∪ 𝑦
∪ 𝑧)))) |
33 | 32 | oveq2d 7373 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦
∪ 𝑧))))) |
34 | | pweq 4574 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → 𝒫 𝑥 = 𝒫 (𝑦 ∪ {𝑧})) |
35 | 34 | sumeq1d 15586 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
(𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠)))) |
36 | 33, 35 | eqeq12d 2752 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑏)
− (♯‘(𝑏
∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
37 | 36 | ralbidv 3174 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥)))
= Σ𝑠 ∈ 𝒫
𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
(∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
38 | | unieq 4876 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪
𝐴) |
39 | 38 | ineq2d 4172 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝐴)) |
40 | 39 | fveq2d 6846 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ ∪ 𝐴))) |
41 | 40 | oveq2d 7373 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴)))) |
42 | | pweq 4574 |
. . . . . 6
⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴) |
43 | 42 | sumeq1d 15586 |
. . . . 5
⊢ (𝑥 = 𝐴 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) |
44 | 41, 43 | eqeq12d 2752 |
. . . 4
⊢ (𝑥 = 𝐴 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑏)
− (♯‘(𝑏
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
45 | 44 | ralbidv 3174 |
. . 3
⊢ (𝑥 = 𝐴 → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥)))
= Σ𝑠 ∈ 𝒫
𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
46 | | hashcl 14256 |
. . . . . . 7
⊢ (𝑏 ∈ Fin →
(♯‘𝑏) ∈
ℕ0) |
47 | 46 | nn0cnd 12475 |
. . . . . 6
⊢ (𝑏 ∈ Fin →
(♯‘𝑏) ∈
ℂ) |
48 | 47 | mulid2d 11173 |
. . . . 5
⊢ (𝑏 ∈ Fin → (1 ·
(♯‘𝑏)) =
(♯‘𝑏)) |
49 | | 0ex 5264 |
. . . . . 6
⊢ ∅
∈ V |
50 | 48, 47 | eqeltrd 2838 |
. . . . . 6
⊢ (𝑏 ∈ Fin → (1 ·
(♯‘𝑏)) ∈
ℂ) |
51 | | fveq2 6842 |
. . . . . . . . . . 11
⊢ (𝑠 = ∅ →
(♯‘𝑠) =
(♯‘∅)) |
52 | 51, 8 | eqtrdi 2792 |
. . . . . . . . . 10
⊢ (𝑠 = ∅ →
(♯‘𝑠) =
0) |
53 | 52 | oveq2d 7373 |
. . . . . . . . 9
⊢ (𝑠 = ∅ →
(-1↑(♯‘𝑠))
= (-1↑0)) |
54 | | neg1cn 12267 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
55 | | exp0 13971 |
. . . . . . . . . 10
⊢ (-1
∈ ℂ → (-1↑0) = 1) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . 9
⊢
(-1↑0) = 1 |
57 | 53, 56 | eqtrdi 2792 |
. . . . . . . 8
⊢ (𝑠 = ∅ →
(-1↑(♯‘𝑠))
= 1) |
58 | | rint0 4951 |
. . . . . . . . 9
⊢ (𝑠 = ∅ → (𝑏 ∩ ∩ 𝑠) =
𝑏) |
59 | 58 | fveq2d 6846 |
. . . . . . . 8
⊢ (𝑠 = ∅ →
(♯‘(𝑏 ∩
∩ 𝑠)) = (♯‘𝑏)) |
60 | 57, 59 | oveq12d 7375 |
. . . . . . 7
⊢ (𝑠 = ∅ →
((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= (1 · (♯‘𝑏))) |
61 | 60 | sumsn 15631 |
. . . . . 6
⊢ ((∅
∈ V ∧ (1 · (♯‘𝑏)) ∈ ℂ) → Σ𝑠 ∈ {∅}
((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= (1 · (♯‘𝑏))) |
62 | 49, 50, 61 | sylancr 587 |
. . . . 5
⊢ (𝑏 ∈ Fin → Σ𝑠 ∈ {∅}
((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= (1 · (♯‘𝑏))) |
63 | 47 | subid1d 11501 |
. . . . 5
⊢ (𝑏 ∈ Fin →
((♯‘𝑏) −
0) = (♯‘𝑏)) |
64 | 48, 62, 63 | 3eqtr4rd 2787 |
. . . 4
⊢ (𝑏 ∈ Fin →
((♯‘𝑏) −
0) = Σ𝑠 ∈
{∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) |
65 | 64 | rgen 3066 |
. . 3
⊢
∀𝑏 ∈ Fin
((♯‘𝑏) −
0) = Σ𝑠 ∈
{∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) |
66 | | fveq2 6842 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑥 → (♯‘𝑏) = (♯‘𝑥)) |
67 | | ineq1 4165 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ ∪ 𝑦)) |
68 | 67 | fveq2d 6846 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ ∪ 𝑦)) = (♯‘(𝑥 ∩ ∪ 𝑦))) |
69 | 66, 68 | oveq12d 7375 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑥 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))) |
70 | | simpl 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑏 = 𝑥) |
71 | 70 | ineq1d 4171 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠)) |
72 | 71 | fveq2d 6846 |
. . . . . . . . . . . . 13
⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ ∩ 𝑠))) |
73 | 72 | oveq2d 7373 |
. . . . . . . . . . . 12
⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠)))) |
74 | 73 | sumeq2dv 15588 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) |
75 | 69, 74 | eqeq12d 2752 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑥 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑥)
− (♯‘(𝑥
∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))) |
76 | 75 | rspcva 3579 |
. . . . . . . . 9
⊢ ((𝑥 ∈ Fin ∧ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) |
77 | 76 | adantll 712 |
. . . . . . . 8
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) |
78 | | simpr 485 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑥 ∈ Fin) |
79 | | inss1 4188 |
. . . . . . . . . 10
⊢ (𝑥 ∩ 𝑧) ⊆ 𝑥 |
80 | | ssfi 9117 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ 𝑧) ⊆ 𝑥) → (𝑥 ∩ 𝑧) ∈ Fin) |
81 | 78, 79, 80 | sylancl 586 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ 𝑧) ∈ Fin) |
82 | | fveq2 6842 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘𝑏) = (♯‘(𝑥 ∩ 𝑧))) |
83 | | ineq1 4165 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦)) |
84 | | in32 4181 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = ((𝑥 ∩ ∪ 𝑦) ∩ 𝑧) |
85 | | inass 4179 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∩ ∪ 𝑦)
∩ 𝑧) = (𝑥 ∩ (∪ 𝑦
∩ 𝑧)) |
86 | 84, 85 | eqtri 2764 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) |
87 | 83, 86 | eqtrdi 2792 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) |
88 | 87 | fveq2d 6846 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘(𝑏 ∩ ∪ 𝑦)) = (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧)))) |
89 | 82, 88 | oveq12d 7375 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))) |
90 | | ineq1 4165 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠)) |
91 | | in32 4181 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = ((𝑥 ∩ ∩ 𝑠) ∩ 𝑧) |
92 | | inass 4179 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∩ ∩ 𝑠)
∩ 𝑧) = (𝑥 ∩ (∩ 𝑠
∩ 𝑧)) |
93 | 91, 92 | eqtri 2764 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) |
94 | 90, 93 | eqtrdi 2792 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) |
95 | 94 | fveq2d 6846 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) |
96 | 95 | oveq2d 7373 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) |
97 | 96 | sumeq2sdv 15589 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑥 ∩ 𝑧) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) |
98 | 89, 97 | eqeq12d 2752 |
. . . . . . . . . 10
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘(𝑥
∩ 𝑧)) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) |
99 | 98 | rspcva 3579 |
. . . . . . . . 9
⊢ (((𝑥 ∩ 𝑧) ∈ Fin ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) |
100 | 81, 99 | sylan 580 |
. . . . . . . 8
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) |
101 | 77, 100 | oveq12d 7375 |
. . . . . . 7
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))
− ((♯‘(𝑥
∩ 𝑧)) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∩ 𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
− Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) |
102 | | inss1 4188 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∩ ∪ 𝑦)
⊆ 𝑥 |
103 | | ssfi 9117 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∪ 𝑦)
⊆ 𝑥) → (𝑥 ∩ ∪ 𝑦)
∈ Fin) |
104 | 78, 102, 103 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ ∪ 𝑦) ∈ Fin) |
105 | | hashcl 14256 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ ∪ 𝑦)
∈ Fin → (♯‘(𝑥 ∩ ∪ 𝑦)) ∈
ℕ0) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ ∪ 𝑦))
∈ ℕ0) |
107 | 106 | nn0cnd 12475 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ ∪ 𝑦))
∈ ℂ) |
108 | | hashcl 14256 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ 𝑧) ∈ Fin → (♯‘(𝑥 ∩ 𝑧)) ∈
ℕ0) |
109 | 81, 108 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ 𝑧)) ∈
ℕ0) |
110 | 109 | nn0cnd 12475 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ 𝑧)) ∈ ℂ) |
111 | | inss1 4188 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∩ (∪ 𝑦
∩ 𝑧)) ⊆ 𝑥 |
112 | | ssfi 9117 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∪ 𝑦
∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin) |
113 | 78, 111, 112 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin) |
114 | | hashcl 14256 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ (∪ 𝑦
∩ 𝑧)) ∈ Fin →
(♯‘(𝑥 ∩
(∪ 𝑦 ∩ 𝑧))) ∈
ℕ0) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧))) ∈
ℕ0) |
116 | 115 | nn0cnd 12475 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧))) ∈
ℂ) |
117 | | hashun3 14284 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∩ ∪ 𝑦)
∈ Fin ∧ (𝑥 ∩
𝑧) ∈ Fin) →
(♯‘((𝑥 ∩
∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦)
∩ (𝑥 ∩ 𝑧))))) |
118 | 104, 81, 117 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘((𝑥 ∩ ∪ 𝑦)
∪ (𝑥 ∩ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦))
+ (♯‘(𝑥 ∩
𝑧))) −
(♯‘((𝑥 ∩
∪ 𝑦) ∩ (𝑥 ∩ 𝑧))))) |
119 | | indi 4233 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∩ (∪ 𝑦
∪ 𝑧)) = ((𝑥 ∩ ∪ 𝑦)
∪ (𝑥 ∩ 𝑧)) |
120 | 119 | fveq2i 6845 |
. . . . . . . . . . . 12
⊢
(♯‘(𝑥
∩ (∪ 𝑦 ∪ 𝑧))) = (♯‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) |
121 | | inindi 4186 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∩ (∪ 𝑦
∩ 𝑧)) = ((𝑥 ∩ ∪ 𝑦)
∩ (𝑥 ∩ 𝑧)) |
122 | 121 | fveq2i 6845 |
. . . . . . . . . . . . 13
⊢
(♯‘(𝑥
∩ (∪ 𝑦 ∩ 𝑧))) = (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧))) |
123 | 122 | oveq2i 7368 |
. . . . . . . . . . . 12
⊢
(((♯‘(𝑥
∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧)))) =
(((♯‘(𝑥 ∩
∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦)
∩ (𝑥 ∩ 𝑧)))) |
124 | 118, 120,
123 | 3eqtr4g 2801 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧))) =
(((♯‘(𝑥 ∩
∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧))))) |
125 | 107, 110,
116, 124 | assraddsubd 11569 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧))) =
((♯‘(𝑥 ∩
∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))) |
126 | 125 | oveq2d 7373 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧)))) =
((♯‘𝑥) −
((♯‘(𝑥 ∩
∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))) |
127 | | hashcl 14256 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ Fin →
(♯‘𝑥) ∈
ℕ0) |
128 | 127 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘𝑥) ∈
ℕ0) |
129 | 128 | nn0cnd 12475 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘𝑥) ∈
ℂ) |
130 | 110, 116 | subcld 11512 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) ∈ ℂ) |
131 | 129, 107,
130 | subsub4d 11543 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))
− ((♯‘(𝑥
∩ 𝑧)) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∩ 𝑧))))) = ((♯‘𝑥) − ((♯‘(𝑥 ∩ ∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))) |
132 | 126, 131 | eqtr4d 2779 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧)))) =
(((♯‘𝑥) −
(♯‘(𝑥 ∩
∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))) |
133 | 132 | adantr 481 |
. . . . . . 7
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧)))) =
(((♯‘𝑥) −
(♯‘(𝑥 ∩
∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))) |
134 | | disjdif 4431 |
. . . . . . . . . . 11
⊢
(𝒫 𝑦 ∩
(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅ |
135 | 134 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅) |
136 | | ssun1 4132 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
137 | 136 | sspwi 4572 |
. . . . . . . . . . . . 13
⊢ 𝒫
𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}) |
138 | | undif 4441 |
. . . . . . . . . . . . 13
⊢
(𝒫 𝑦 ⊆
𝒫 (𝑦 ∪ {𝑧}) ↔ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧})) |
139 | 137, 138 | mpbi 229 |
. . . . . . . . . . . 12
⊢
(𝒫 𝑦 ∪
(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧}) |
140 | 139 | eqcomi 2745 |
. . . . . . . . . . 11
⊢ 𝒫
(𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) |
141 | 140 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) |
142 | | simpll 765 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑦 ∈ Fin) |
143 | | snfi 8988 |
. . . . . . . . . . . 12
⊢ {𝑧} ∈ Fin |
144 | | unfi 9116 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) |
145 | 142, 143,
144 | sylancl 586 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) |
146 | | pwfi 9122 |
. . . . . . . . . . 11
⊢ ((𝑦 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin) |
147 | 145, 146 | sylib 217 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin) |
148 | 54 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → -1 ∈
ℂ) |
149 | | elpwi 4567 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}) → 𝑠 ⊆ (𝑦 ∪ {𝑧})) |
150 | | ssfi 9117 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝑠 ⊆ (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin) |
151 | 145, 149,
150 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin) |
152 | | hashcl 14256 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ Fin →
(♯‘𝑠) ∈
ℕ0) |
153 | 151, 152 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘𝑠) ∈
ℕ0) |
154 | 148, 153 | expcld 14051 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (-1↑(♯‘𝑠)) ∈
ℂ) |
155 | | simplr 767 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑥 ∈ Fin) |
156 | | inss1 4188 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∩ ∩ 𝑠)
⊆ 𝑥 |
157 | | ssfi 9117 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∩ 𝑠)
⊆ 𝑥) → (𝑥 ∩ ∩ 𝑠)
∈ Fin) |
158 | 155, 156,
157 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ ∩ 𝑠) ∈ Fin) |
159 | | hashcl 14256 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ ∩ 𝑠)
∈ Fin → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈
ℕ0) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈
ℕ0) |
161 | 160 | nn0cnd 12475 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈
ℂ) |
162 | 154, 161 | mulcld 11175 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) ∈ ℂ) |
163 | 135, 141,
147, 162 | fsumsplit 15626 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= (Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
+ Σ𝑠 ∈
(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))))) |
164 | | fveq2 6842 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (♯‘𝑠) = (♯‘(𝑡 ∪ {𝑧}))) |
165 | 164 | oveq2d 7373 |
. . . . . . . . . . . . 13
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (-1↑(♯‘𝑠)) =
(-1↑(♯‘(𝑡
∪ {𝑧})))) |
166 | | inteq 4910 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = ∩
(𝑡 ∪ {𝑧})) |
167 | | vex 3449 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
168 | 167 | intunsn 4950 |
. . . . . . . . . . . . . . . 16
⊢ ∩ (𝑡
∪ {𝑧}) = (∩ 𝑡
∩ 𝑧) |
169 | 166, 168 | eqtrdi 2792 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = (∩
𝑡 ∩ 𝑧)) |
170 | 169 | ineq2d 4172 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (𝑥 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑡 ∩ 𝑧))) |
171 | 170 | fveq2d 6846 |
. . . . . . . . . . . . 13
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (♯‘(𝑥 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧)))) |
172 | 165, 171 | oveq12d 7375 |
. . . . . . . . . . . 12
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) = ((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧))))) |
173 | | pwfi 9122 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ Fin ↔ 𝒫
𝑦 ∈
Fin) |
174 | 142, 173 | sylib 217 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ∈ Fin) |
175 | | eqid 2736 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})) = (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})) |
176 | | elpwi 4567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ 𝒫 𝑦 → 𝑢 ⊆ 𝑦) |
177 | 176 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑢 ⊆ 𝑦) |
178 | | unss1 4139 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ⊆ 𝑦 → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧})) |
179 | 177, 178 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧})) |
180 | | vex 3449 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑢 ∈ V |
181 | | vsnex 5386 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑧} ∈ V |
182 | 180, 181 | unex 7680 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∪ {𝑧}) ∈ V |
183 | 182 | elpw 4564 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧})) |
184 | 179, 183 | sylibr 233 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧})) |
185 | | simpllr 774 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦) |
186 | | elpwi 4567 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → (𝑢 ∪ {𝑧}) ⊆ 𝑦) |
187 | | ssun2 4133 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧}) |
188 | 167 | snss 4746 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧})) |
189 | 187, 188 | mpbir 230 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ (𝑢 ∪ {𝑧}) |
190 | 189 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑧 ∈ (𝑢 ∪ {𝑧})) |
191 | | ssel 3937 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∪ {𝑧}) ⊆ 𝑦 → (𝑧 ∈ (𝑢 ∪ {𝑧}) → 𝑧 ∈ 𝑦)) |
192 | 186, 190,
191 | syl2imc 41 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → 𝑧 ∈ 𝑦)) |
193 | 185, 192 | mtod 197 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ (𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦) |
194 | 184, 193 | eldifd 3921 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) |
195 | | eldifi 4086 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) |
196 | 195 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) |
197 | 196 | elpwid 4569 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ (𝑦 ∪ {𝑧})) |
198 | | uncom 4113 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦) |
199 | 197, 198 | sseqtrdi 3994 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ ({𝑧} ∪ 𝑦)) |
200 | | ssundif 4445 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦) |
201 | 199, 200 | sylib 217 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ⊆ 𝑦) |
202 | | vex 3449 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
203 | 202 | elpw2 5302 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦 ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦) |
204 | 201, 203 | sylibr 233 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦) |
205 | | elpwunsn 4644 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑧 ∈ 𝑠) |
206 | 205 | ad2antll 727 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑧 ∈ 𝑠) |
207 | 206 | snssd 4769 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → {𝑧} ⊆ 𝑠) |
208 | | ssequn2 4143 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑧} ⊆ 𝑠 ↔ (𝑠 ∪ {𝑧}) = 𝑠) |
209 | 207, 208 | sylib 217 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 ∪ {𝑧}) = 𝑠) |
210 | 209 | eqcomd 2742 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑠 = (𝑠 ∪ {𝑧})) |
211 | | uneq1 4116 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = ((𝑠 ∖ {𝑧}) ∪ {𝑧})) |
212 | | undif1 4435 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∖ {𝑧}) ∪ {𝑧}) = (𝑠 ∪ {𝑧}) |
213 | 211, 212 | eqtrdi 2792 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = (𝑠 ∪ {𝑧})) |
214 | 213 | eqeq2d 2747 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑠 = (𝑢 ∪ {𝑧}) ↔ 𝑠 = (𝑠 ∪ {𝑧}))) |
215 | 210, 214 | syl5ibrcom 246 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) → 𝑠 = (𝑢 ∪ {𝑧}))) |
216 | 176 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 ⊆ 𝑦) |
217 | | simpllr 774 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑦) |
218 | 216, 217 | ssneldd 3947 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑢) |
219 | | difsnb 4766 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ 𝑢 ↔ (𝑢 ∖ {𝑧}) = 𝑢) |
220 | 218, 219 | sylib 217 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 ∖ {𝑧}) = 𝑢) |
221 | 220 | eqcomd 2742 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 = (𝑢 ∖ {𝑧})) |
222 | | difeq1 4075 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = ((𝑢 ∪ {𝑧}) ∖ {𝑧})) |
223 | | difun2 4440 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∪ {𝑧}) ∖ {𝑧}) = (𝑢 ∖ {𝑧}) |
224 | 222, 223 | eqtrdi 2792 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = (𝑢 ∖ {𝑧})) |
225 | 224 | eqeq2d 2747 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑢 = (𝑢 ∖ {𝑧}))) |
226 | 221, 225 | syl5ibrcom 246 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 = (𝑢 ∪ {𝑧}) → 𝑢 = (𝑠 ∖ {𝑧}))) |
227 | 215, 226 | impbid 211 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑠 = (𝑢 ∪ {𝑧}))) |
228 | 175, 194,
204, 227 | f1o2d 7607 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})):𝒫 𝑦–1-1-onto→(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) |
229 | | uneq1 4116 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑡 → (𝑢 ∪ {𝑧}) = (𝑡 ∪ {𝑧})) |
230 | | vex 3449 |
. . . . . . . . . . . . . . 15
⊢ 𝑡 ∈ V |
231 | 230, 181 | unex 7680 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∪ {𝑧}) ∈ V |
232 | 229, 175,
231 | fvmpt 6948 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝒫 𝑦 → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧})) |
233 | 232 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑡 ∈ 𝒫 𝑦) → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧})) |
234 | 195, 162 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) ∈ ℂ) |
235 | 172, 174,
228, 233, 234 | fsumf1o 15608 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= Σ𝑡 ∈ 𝒫
𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧))))) |
236 | | uneq1 4116 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑠 → (𝑡 ∪ {𝑧}) = (𝑠 ∪ {𝑧})) |
237 | 236 | fveq2d 6846 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑠 → (♯‘(𝑡 ∪ {𝑧})) = (♯‘(𝑠 ∪ {𝑧}))) |
238 | 237 | oveq2d 7373 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑠 → (-1↑(♯‘(𝑡 ∪ {𝑧}))) = (-1↑(♯‘(𝑠 ∪ {𝑧})))) |
239 | | inteq 4910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑠 → ∩ 𝑡 = ∩
𝑠) |
240 | 239 | ineq1d 4171 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑠 → (∩ 𝑡 ∩ 𝑧) = (∩ 𝑠 ∩ 𝑧)) |
241 | 240 | ineq2d 4172 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑠 → (𝑥 ∩ (∩ 𝑡 ∩ 𝑧)) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) |
242 | 241 | fveq2d 6846 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑠 → (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧))) = (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) |
243 | 238, 242 | oveq12d 7375 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑠 → ((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧)))) =
((-1↑(♯‘(𝑠
∪ {𝑧}))) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) |
244 | 243 | cbvsumv 15581 |
. . . . . . . . . . . 12
⊢
Σ𝑡 ∈
𝒫 𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) |
245 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → -1 ∈ ℂ) |
246 | | elpwi 4567 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ⊆ 𝑦) |
247 | | ssfi 9117 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ Fin ∧ 𝑠 ⊆ 𝑦) → 𝑠 ∈ Fin) |
248 | 142, 246,
247 | syl2an 596 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ Fin) |
249 | 248, 152 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘𝑠) ∈
ℕ0) |
250 | 245, 249 | expp1d 14052 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑((♯‘𝑠) + 1)) =
((-1↑(♯‘𝑠)) · -1)) |
251 | 246 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ⊆ 𝑦) |
252 | | simpllr 774 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦) |
253 | 251, 252 | ssneldd 3947 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑠) |
254 | | hashunsng 14292 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ V → ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1))) |
255 | 254 | elv 3451 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1)) |
256 | 248, 253,
255 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1)) |
257 | 256 | oveq2d 7373 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = (-1↑((♯‘𝑠) + 1))) |
258 | 137 | sseli 3940 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) |
259 | 258, 154 | sylan2 593 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘𝑠)) ∈
ℂ) |
260 | 245, 259 | mulcomd 11176 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 ·
(-1↑(♯‘𝑠))) = ((-1↑(♯‘𝑠)) ·
-1)) |
261 | 250, 257,
260 | 3eqtr4d 2786 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = (-1 ·
(-1↑(♯‘𝑠)))) |
262 | 259 | mulm1d 11607 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 ·
(-1↑(♯‘𝑠))) = -(-1↑(♯‘𝑠))) |
263 | 261, 262 | eqtrd 2776 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = -(-1↑(♯‘𝑠))) |
264 | 263 | oveq1d 7372 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) =
(-(-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) |
265 | | inss1 4188 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∩ (∩ 𝑠
∩ 𝑧)) ⊆ 𝑥 |
266 | | ssfi 9117 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∩ 𝑠
∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin) |
267 | 155, 265,
266 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin) |
268 | | hashcl 14256 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∩ (∩ 𝑠
∩ 𝑧)) ∈ Fin →
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))) ∈
ℕ0) |
269 | 267, 268 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈
ℕ0) |
270 | 269 | nn0cnd 12475 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ) |
271 | 258, 270 | sylan2 593 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ) |
272 | 259, 271 | mulneg1d 11608 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-(-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧)))) = -((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) |
273 | 264, 272 | eqtrd 2776 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) =
-((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) |
274 | 273 | sumeq2dv 15588 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) |
275 | 244, 274 | eqtrid 2788 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑡 ∈ 𝒫 𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) |
276 | 154, 270 | mulcld 11175 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧)))) ∈ ℂ) |
277 | 258, 276 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧)))) ∈ ℂ) |
278 | 174, 277 | fsumneg 15672 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) |
279 | 235, 275,
278 | 3eqtrd 2780 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= -Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) |
280 | 279 | oveq2d 7373 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
+ -Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) |
281 | 137 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧})) |
282 | 281 | sselda 3944 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) |
283 | 282, 162 | syldan 591 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) ∈ ℂ) |
284 | 174, 283 | fsumcl 15618 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
∈ ℂ) |
285 | 282, 276 | syldan 591 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧)))) ∈ ℂ) |
286 | 174, 285 | fsumcl 15618 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) ∈
ℂ) |
287 | 284, 286 | negsubd 11518 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) =
(Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
− Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) |
288 | 163, 280,
287 | 3eqtrd 2780 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= (Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
− Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) |
289 | 288 | adantr 481 |
. . . . . . 7
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= (Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
− Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) |
290 | 101, 133,
289 | 3eqtr4d 2786 |
. . . . . 6
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) |
291 | 290 | ex 413 |
. . . . 5
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
→ ((♯‘𝑥)
− (♯‘(𝑥
∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))) |
292 | 291 | ralrimdva 3151 |
. . . 4
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
→ ∀𝑥 ∈ Fin
((♯‘𝑥) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))) |
293 | | ineq1 4165 |
. . . . . . . 8
⊢ (𝑏 = 𝑥 → (𝑏 ∩ (∪ 𝑦 ∪ 𝑧)) = (𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) |
294 | 293 | fveq2d 6846 |
. . . . . . 7
⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧))) = (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) |
295 | 66, 294 | oveq12d 7375 |
. . . . . 6
⊢ (𝑏 = 𝑥 → ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))))) |
296 | | ineq1 4165 |
. . . . . . . . 9
⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠)) |
297 | 296 | fveq2d 6846 |
. . . . . . . 8
⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ ∩ 𝑠))) |
298 | 297 | oveq2d 7373 |
. . . . . . 7
⊢ (𝑏 = 𝑥 → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠)))) |
299 | 298 | sumeq2sdv 15589 |
. . . . . 6
⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
(𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠)))) |
300 | 295, 299 | eqeq12d 2752 |
. . . . 5
⊢ (𝑏 = 𝑥 → (((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑥)
− (♯‘(𝑥
∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))) |
301 | 300 | cbvralvw 3225 |
. . . 4
⊢
(∀𝑏 ∈
Fin ((♯‘𝑏)
− (♯‘(𝑏
∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑥 ∈ Fin
((♯‘𝑥) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) |
302 | 292, 301 | syl6ibr 251 |
. . 3
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
→ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
(∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
303 | 16, 24, 37, 45, 65, 302 | findcard2s 9109 |
. 2
⊢ (𝐴 ∈ Fin → ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) |
304 | | fveq2 6842 |
. . . . 5
⊢ (𝑏 = 𝐵 → (♯‘𝑏) = (♯‘𝐵)) |
305 | | ineq1 4165 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (𝑏 ∩ ∪ 𝐴) = (𝐵 ∩ ∪ 𝐴)) |
306 | 305 | fveq2d 6846 |
. . . . 5
⊢ (𝑏 = 𝐵 → (♯‘(𝑏 ∩ ∪ 𝐴)) = (♯‘(𝐵 ∩ ∪ 𝐴))) |
307 | 304, 306 | oveq12d 7375 |
. . . 4
⊢ (𝑏 = 𝐵 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴)))) |
308 | | simpl 483 |
. . . . . . . 8
⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑏 = 𝐵) |
309 | 308 | ineq1d 4171 |
. . . . . . 7
⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (𝑏 ∩ ∩ 𝑠) = (𝐵 ∩ ∩ 𝑠)) |
310 | 309 | fveq2d 6846 |
. . . . . 6
⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝐵 ∩ ∩ 𝑠))) |
311 | 310 | oveq2d 7373 |
. . . . 5
⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = ((-1↑(♯‘𝑠)) ·
(♯‘(𝐵 ∩
∩ 𝑠)))) |
312 | 311 | sumeq2dv 15588 |
. . . 4
⊢ (𝑏 = 𝐵 → Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))) |
313 | 307, 312 | eqeq12d 2752 |
. . 3
⊢ (𝑏 = 𝐵 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝐵)
− (♯‘(𝐵
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))) |
314 | 313 | rspccva 3580 |
. 2
⊢
((∀𝑏 ∈
Fin ((♯‘𝑏)
− (♯‘(𝑏
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
∧ 𝐵 ∈ Fin) →
((♯‘𝐵) −
(♯‘(𝐵 ∩
∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))) |
315 | 303, 314 | sylan 580 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐵) −
(♯‘(𝐵 ∩
∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))) |