Step | Hyp | Ref
| Expression |
1 | | unieq 4679 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∪ ∅) |
2 | | uni0 4700 |
. . . . . . . . . . 11
⊢ ∪ ∅ = ∅ |
3 | 1, 2 | syl6eq 2830 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∅) |
4 | 3 | ineq2d 4037 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) =
(𝑏 ∩
∅)) |
5 | | in0 4194 |
. . . . . . . . 9
⊢ (𝑏 ∩ ∅) =
∅ |
6 | 4, 5 | syl6eq 2830 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) =
∅) |
7 | 6 | fveq2d 6450 |
. . . . . . 7
⊢ (𝑥 = ∅ →
(♯‘(𝑏 ∩
∪ 𝑥)) =
(♯‘∅)) |
8 | | hash0 13473 |
. . . . . . 7
⊢
(♯‘∅) = 0 |
9 | 7, 8 | syl6eq 2830 |
. . . . . 6
⊢ (𝑥 = ∅ →
(♯‘(𝑏 ∩
∪ 𝑥)) = 0) |
10 | 9 | oveq2d 6938 |
. . . . 5
⊢ (𝑥 = ∅ →
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑥))) = ((♯‘𝑏) − 0)) |
11 | | pweq 4382 |
. . . . . . 7
⊢ (𝑥 = ∅ → 𝒫
𝑥 = 𝒫
∅) |
12 | | pw0 4574 |
. . . . . . 7
⊢ 𝒫
∅ = {∅} |
13 | 11, 12 | syl6eq 2830 |
. . . . . 6
⊢ (𝑥 = ∅ → 𝒫
𝑥 =
{∅}) |
14 | 13 | sumeq1d 14839 |
. . . . 5
⊢ (𝑥 = ∅ → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = Σ𝑠 ∈ {∅}
((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) |
15 | 10, 14 | eqeq12d 2793 |
. . . 4
⊢ (𝑥 = ∅ →
(((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑏)
− 0) = Σ𝑠
∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
16 | 15 | ralbidv 3168 |
. . 3
⊢ (𝑥 = ∅ → (∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑏 ∈ Fin
((♯‘𝑏) −
0) = Σ𝑠 ∈
{∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
17 | | unieq 4679 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ∪ 𝑥 = ∪
𝑦) |
18 | 17 | ineq2d 4037 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝑦)) |
19 | 18 | fveq2d 6450 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ ∪ 𝑦))) |
20 | 19 | oveq2d 6938 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))) |
21 | | pweq 4382 |
. . . . . 6
⊢ (𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦) |
22 | 21 | sumeq1d 14839 |
. . . . 5
⊢ (𝑥 = 𝑦 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) |
23 | 20, 22 | eqeq12d 2793 |
. . . 4
⊢ (𝑥 = 𝑦 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑏)
− (♯‘(𝑏
∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
24 | 23 | ralbidv 3168 |
. . 3
⊢ (𝑥 = 𝑦 → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥)))
= Σ𝑠 ∈ 𝒫
𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
25 | | unieq 4679 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = ∪
(𝑦 ∪ {𝑧})) |
26 | | uniun 4692 |
. . . . . . . . . 10
⊢ ∪ (𝑦
∪ {𝑧}) = (∪ 𝑦
∪ ∪ {𝑧}) |
27 | | vex 3401 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
28 | 27 | unisn 4687 |
. . . . . . . . . . 11
⊢ ∪ {𝑧}
= 𝑧 |
29 | 28 | uneq2i 3987 |
. . . . . . . . . 10
⊢ (∪ 𝑦
∪ ∪ {𝑧}) = (∪ 𝑦 ∪ 𝑧) |
30 | 26, 29 | eqtri 2802 |
. . . . . . . . 9
⊢ ∪ (𝑦
∪ {𝑧}) = (∪ 𝑦
∪ 𝑧) |
31 | 25, 30 | syl6eq 2830 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = (∪
𝑦 ∪ 𝑧)) |
32 | 31 | ineq2d 4037 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ (∪ 𝑦 ∪ 𝑧))) |
33 | 32 | fveq2d 6450 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ (∪ 𝑦
∪ 𝑧)))) |
34 | 33 | oveq2d 6938 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦
∪ 𝑧))))) |
35 | | pweq 4382 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → 𝒫 𝑥 = 𝒫 (𝑦 ∪ {𝑧})) |
36 | 35 | sumeq1d 14839 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
(𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠)))) |
37 | 34, 36 | eqeq12d 2793 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑏)
− (♯‘(𝑏
∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
38 | 37 | ralbidv 3168 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥)))
= Σ𝑠 ∈ 𝒫
𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
(∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
39 | | unieq 4679 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪
𝐴) |
40 | 39 | ineq2d 4037 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝐴)) |
41 | 40 | fveq2d 6450 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ ∪ 𝐴))) |
42 | 41 | oveq2d 6938 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴)))) |
43 | | pweq 4382 |
. . . . . 6
⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴) |
44 | 43 | sumeq1d 14839 |
. . . . 5
⊢ (𝑥 = 𝐴 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) |
45 | 42, 44 | eqeq12d 2793 |
. . . 4
⊢ (𝑥 = 𝐴 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑏)
− (♯‘(𝑏
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
46 | 45 | ralbidv 3168 |
. . 3
⊢ (𝑥 = 𝐴 → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥)))
= Σ𝑠 ∈ 𝒫
𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
47 | | hashcl 13462 |
. . . . . . 7
⊢ (𝑏 ∈ Fin →
(♯‘𝑏) ∈
ℕ0) |
48 | 47 | nn0cnd 11704 |
. . . . . 6
⊢ (𝑏 ∈ Fin →
(♯‘𝑏) ∈
ℂ) |
49 | 48 | mulid2d 10395 |
. . . . 5
⊢ (𝑏 ∈ Fin → (1 ·
(♯‘𝑏)) =
(♯‘𝑏)) |
50 | | 0ex 5026 |
. . . . . 6
⊢ ∅
∈ V |
51 | 49, 48 | eqeltrd 2859 |
. . . . . 6
⊢ (𝑏 ∈ Fin → (1 ·
(♯‘𝑏)) ∈
ℂ) |
52 | | fveq2 6446 |
. . . . . . . . . . 11
⊢ (𝑠 = ∅ →
(♯‘𝑠) =
(♯‘∅)) |
53 | 52, 8 | syl6eq 2830 |
. . . . . . . . . 10
⊢ (𝑠 = ∅ →
(♯‘𝑠) =
0) |
54 | 53 | oveq2d 6938 |
. . . . . . . . 9
⊢ (𝑠 = ∅ →
(-1↑(♯‘𝑠))
= (-1↑0)) |
55 | | neg1cn 11496 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
56 | | exp0 13182 |
. . . . . . . . . 10
⊢ (-1
∈ ℂ → (-1↑0) = 1) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . 9
⊢
(-1↑0) = 1 |
58 | 54, 57 | syl6eq 2830 |
. . . . . . . 8
⊢ (𝑠 = ∅ →
(-1↑(♯‘𝑠))
= 1) |
59 | | rint0 4750 |
. . . . . . . . 9
⊢ (𝑠 = ∅ → (𝑏 ∩ ∩ 𝑠) =
𝑏) |
60 | 59 | fveq2d 6450 |
. . . . . . . 8
⊢ (𝑠 = ∅ →
(♯‘(𝑏 ∩
∩ 𝑠)) = (♯‘𝑏)) |
61 | 58, 60 | oveq12d 6940 |
. . . . . . 7
⊢ (𝑠 = ∅ →
((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= (1 · (♯‘𝑏))) |
62 | 61 | sumsn 14882 |
. . . . . 6
⊢ ((∅
∈ V ∧ (1 · (♯‘𝑏)) ∈ ℂ) → Σ𝑠 ∈ {∅}
((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= (1 · (♯‘𝑏))) |
63 | 50, 51, 62 | sylancr 581 |
. . . . 5
⊢ (𝑏 ∈ Fin → Σ𝑠 ∈ {∅}
((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= (1 · (♯‘𝑏))) |
64 | 48 | subid1d 10723 |
. . . . 5
⊢ (𝑏 ∈ Fin →
((♯‘𝑏) −
0) = (♯‘𝑏)) |
65 | 49, 63, 64 | 3eqtr4rd 2825 |
. . . 4
⊢ (𝑏 ∈ Fin →
((♯‘𝑏) −
0) = Σ𝑠 ∈
{∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) |
66 | 65 | rgen 3104 |
. . 3
⊢
∀𝑏 ∈ Fin
((♯‘𝑏) −
0) = Σ𝑠 ∈
{∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) |
67 | | fveq2 6446 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑥 → (♯‘𝑏) = (♯‘𝑥)) |
68 | | ineq1 4030 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ ∪ 𝑦)) |
69 | 68 | fveq2d 6450 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ ∪ 𝑦)) = (♯‘(𝑥 ∩ ∪ 𝑦))) |
70 | 67, 69 | oveq12d 6940 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑥 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))) |
71 | | simpl 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑏 = 𝑥) |
72 | 71 | ineq1d 4036 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠)) |
73 | 72 | fveq2d 6450 |
. . . . . . . . . . . . 13
⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ ∩ 𝑠))) |
74 | 73 | oveq2d 6938 |
. . . . . . . . . . . 12
⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠)))) |
75 | 74 | sumeq2dv 14841 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) |
76 | 70, 75 | eqeq12d 2793 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑥 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑥)
− (♯‘(𝑥
∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))) |
77 | 76 | rspcva 3509 |
. . . . . . . . 9
⊢ ((𝑥 ∈ Fin ∧ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) |
78 | 77 | adantll 704 |
. . . . . . . 8
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) |
79 | | simpr 479 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑥 ∈ Fin) |
80 | | inss1 4053 |
. . . . . . . . . 10
⊢ (𝑥 ∩ 𝑧) ⊆ 𝑥 |
81 | | ssfi 8468 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ 𝑧) ⊆ 𝑥) → (𝑥 ∩ 𝑧) ∈ Fin) |
82 | 79, 80, 81 | sylancl 580 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ 𝑧) ∈ Fin) |
83 | | fveq2 6446 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘𝑏) = (♯‘(𝑥 ∩ 𝑧))) |
84 | | ineq1 4030 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦)) |
85 | | in32 4046 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = ((𝑥 ∩ ∪ 𝑦) ∩ 𝑧) |
86 | | inass 4044 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∩ ∪ 𝑦)
∩ 𝑧) = (𝑥 ∩ (∪ 𝑦
∩ 𝑧)) |
87 | 85, 86 | eqtri 2802 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) |
88 | 84, 87 | syl6eq 2830 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) |
89 | 88 | fveq2d 6450 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘(𝑏 ∩ ∪ 𝑦)) = (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧)))) |
90 | 83, 89 | oveq12d 6940 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))) |
91 | | ineq1 4030 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠)) |
92 | | in32 4046 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = ((𝑥 ∩ ∩ 𝑠) ∩ 𝑧) |
93 | | inass 4044 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∩ ∩ 𝑠)
∩ 𝑧) = (𝑥 ∩ (∩ 𝑠
∩ 𝑧)) |
94 | 92, 93 | eqtri 2802 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) |
95 | 91, 94 | syl6eq 2830 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) |
96 | 95 | fveq2d 6450 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) |
97 | 96 | oveq2d 6938 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) |
98 | 97 | sumeq2sdv 14842 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑥 ∩ 𝑧) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) |
99 | 90, 98 | eqeq12d 2793 |
. . . . . . . . . 10
⊢ (𝑏 = (𝑥 ∩ 𝑧) → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘(𝑥
∩ 𝑧)) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) |
100 | 99 | rspcva 3509 |
. . . . . . . . 9
⊢ (((𝑥 ∩ 𝑧) ∈ Fin ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) |
101 | 82, 100 | sylan 575 |
. . . . . . . 8
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) |
102 | 78, 101 | oveq12d 6940 |
. . . . . . 7
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))
− ((♯‘(𝑥
∩ 𝑧)) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∩ 𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
− Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) |
103 | | inss1 4053 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∩ ∪ 𝑦)
⊆ 𝑥 |
104 | | ssfi 8468 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∪ 𝑦)
⊆ 𝑥) → (𝑥 ∩ ∪ 𝑦)
∈ Fin) |
105 | 79, 103, 104 | sylancl 580 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ ∪ 𝑦) ∈ Fin) |
106 | | hashcl 13462 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ ∪ 𝑦)
∈ Fin → (♯‘(𝑥 ∩ ∪ 𝑦)) ∈
ℕ0) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ ∪ 𝑦))
∈ ℕ0) |
108 | 107 | nn0cnd 11704 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ ∪ 𝑦))
∈ ℂ) |
109 | | hashcl 13462 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ 𝑧) ∈ Fin → (♯‘(𝑥 ∩ 𝑧)) ∈
ℕ0) |
110 | 82, 109 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ 𝑧)) ∈
ℕ0) |
111 | 110 | nn0cnd 11704 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ 𝑧)) ∈ ℂ) |
112 | | inss1 4053 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∩ (∪ 𝑦
∩ 𝑧)) ⊆ 𝑥 |
113 | | ssfi 8468 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∪ 𝑦
∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin) |
114 | 79, 112, 113 | sylancl 580 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin) |
115 | | hashcl 13462 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ (∪ 𝑦
∩ 𝑧)) ∈ Fin →
(♯‘(𝑥 ∩
(∪ 𝑦 ∩ 𝑧))) ∈
ℕ0) |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧))) ∈
ℕ0) |
117 | 116 | nn0cnd 11704 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧))) ∈
ℂ) |
118 | | hashun3 13488 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∩ ∪ 𝑦)
∈ Fin ∧ (𝑥 ∩
𝑧) ∈ Fin) →
(♯‘((𝑥 ∩
∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦)
∩ (𝑥 ∩ 𝑧))))) |
119 | 105, 82, 118 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘((𝑥 ∩ ∪ 𝑦)
∪ (𝑥 ∩ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦))
+ (♯‘(𝑥 ∩
𝑧))) −
(♯‘((𝑥 ∩
∪ 𝑦) ∩ (𝑥 ∩ 𝑧))))) |
120 | | indi 4100 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∩ (∪ 𝑦
∪ 𝑧)) = ((𝑥 ∩ ∪ 𝑦)
∪ (𝑥 ∩ 𝑧)) |
121 | 120 | fveq2i 6449 |
. . . . . . . . . . . 12
⊢
(♯‘(𝑥
∩ (∪ 𝑦 ∪ 𝑧))) = (♯‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) |
122 | | inindi 4051 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∩ (∪ 𝑦
∩ 𝑧)) = ((𝑥 ∩ ∪ 𝑦)
∩ (𝑥 ∩ 𝑧)) |
123 | 122 | fveq2i 6449 |
. . . . . . . . . . . . 13
⊢
(♯‘(𝑥
∩ (∪ 𝑦 ∩ 𝑧))) = (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧))) |
124 | 123 | oveq2i 6933 |
. . . . . . . . . . . 12
⊢
(((♯‘(𝑥
∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧)))) =
(((♯‘(𝑥 ∩
∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦)
∩ (𝑥 ∩ 𝑧)))) |
125 | 119, 121,
124 | 3eqtr4g 2839 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧))) =
(((♯‘(𝑥 ∩
∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘(𝑥 ∩ (∪ 𝑦
∩ 𝑧))))) |
126 | 108, 111,
117, 125 | assraddsubd 10789 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧))) =
((♯‘(𝑥 ∩
∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))) |
127 | 126 | oveq2d 6938 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧)))) =
((♯‘𝑥) −
((♯‘(𝑥 ∩
∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))) |
128 | | hashcl 13462 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ Fin →
(♯‘𝑥) ∈
ℕ0) |
129 | 128 | adantl 475 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘𝑥) ∈
ℕ0) |
130 | 129 | nn0cnd 11704 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘𝑥) ∈
ℂ) |
131 | 111, 117 | subcld 10734 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) ∈ ℂ) |
132 | 130, 108,
131 | subsub4d 10765 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦)))
− ((♯‘(𝑥
∩ 𝑧)) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∩ 𝑧))))) = ((♯‘𝑥) − ((♯‘(𝑥 ∩ ∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))) |
133 | 127, 132 | eqtr4d 2817 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧)))) =
(((♯‘𝑥) −
(♯‘(𝑥 ∩
∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))) |
134 | 133 | adantr 474 |
. . . . . . 7
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧)))) =
(((♯‘𝑥) −
(♯‘(𝑥 ∩
∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))) |
135 | | disjdif 4264 |
. . . . . . . . . . 11
⊢
(𝒫 𝑦 ∩
(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅ |
136 | 135 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅) |
137 | | ssun1 3999 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
138 | | sspwb 5149 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧})) |
139 | 137, 138 | mpbi 222 |
. . . . . . . . . . . . 13
⊢ 𝒫
𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}) |
140 | | undif 4273 |
. . . . . . . . . . . . 13
⊢
(𝒫 𝑦 ⊆
𝒫 (𝑦 ∪ {𝑧}) ↔ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧})) |
141 | 139, 140 | mpbi 222 |
. . . . . . . . . . . 12
⊢
(𝒫 𝑦 ∪
(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧}) |
142 | 141 | eqcomi 2787 |
. . . . . . . . . . 11
⊢ 𝒫
(𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) |
143 | 142 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) |
144 | | simpll 757 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑦 ∈ Fin) |
145 | | snfi 8326 |
. . . . . . . . . . . 12
⊢ {𝑧} ∈ Fin |
146 | | unfi 8515 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) |
147 | 144, 145,
146 | sylancl 580 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) |
148 | | pwfi 8549 |
. . . . . . . . . . 11
⊢ ((𝑦 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin) |
149 | 147, 148 | sylib 210 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin) |
150 | 55 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → -1 ∈
ℂ) |
151 | | elpwi 4389 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}) → 𝑠 ⊆ (𝑦 ∪ {𝑧})) |
152 | | ssfi 8468 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝑠 ⊆ (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin) |
153 | 147, 151,
152 | syl2an 589 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin) |
154 | | hashcl 13462 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ Fin →
(♯‘𝑠) ∈
ℕ0) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘𝑠) ∈
ℕ0) |
156 | 150, 155 | expcld 13327 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (-1↑(♯‘𝑠)) ∈
ℂ) |
157 | | simplr 759 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑥 ∈ Fin) |
158 | | inss1 4053 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∩ ∩ 𝑠)
⊆ 𝑥 |
159 | | ssfi 8468 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∩ 𝑠)
⊆ 𝑥) → (𝑥 ∩ ∩ 𝑠)
∈ Fin) |
160 | 157, 158,
159 | sylancl 580 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ ∩ 𝑠) ∈ Fin) |
161 | | hashcl 13462 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ ∩ 𝑠)
∈ Fin → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈
ℕ0) |
162 | 160, 161 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈
ℕ0) |
163 | 162 | nn0cnd 11704 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈
ℂ) |
164 | 156, 163 | mulcld 10397 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) ∈ ℂ) |
165 | 136, 143,
149, 164 | fsumsplit 14878 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= (Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
+ Σ𝑠 ∈
(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))))) |
166 | | fveq2 6446 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (♯‘𝑠) = (♯‘(𝑡 ∪ {𝑧}))) |
167 | 166 | oveq2d 6938 |
. . . . . . . . . . . . 13
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (-1↑(♯‘𝑠)) =
(-1↑(♯‘(𝑡
∪ {𝑧})))) |
168 | | inteq 4713 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = ∩
(𝑡 ∪ {𝑧})) |
169 | 27 | intunsn 4749 |
. . . . . . . . . . . . . . . 16
⊢ ∩ (𝑡
∪ {𝑧}) = (∩ 𝑡
∩ 𝑧) |
170 | 168, 169 | syl6eq 2830 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = (∩
𝑡 ∩ 𝑧)) |
171 | 170 | ineq2d 4037 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (𝑥 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑡 ∩ 𝑧))) |
172 | 171 | fveq2d 6450 |
. . . . . . . . . . . . 13
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (♯‘(𝑥 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧)))) |
173 | 167, 172 | oveq12d 6940 |
. . . . . . . . . . . 12
⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) = ((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧))))) |
174 | | pwfi 8549 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ Fin ↔ 𝒫
𝑦 ∈
Fin) |
175 | 144, 174 | sylib 210 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ∈ Fin) |
176 | | eqid 2778 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})) = (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})) |
177 | | elpwi 4389 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ 𝒫 𝑦 → 𝑢 ⊆ 𝑦) |
178 | 177 | adantl 475 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑢 ⊆ 𝑦) |
179 | | unss1 4005 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ⊆ 𝑦 → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧})) |
180 | 178, 179 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧})) |
181 | | vex 3401 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑢 ∈ V |
182 | | snex 5140 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑧} ∈ V |
183 | 181, 182 | unex 7233 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∪ {𝑧}) ∈ V |
184 | 183 | elpw 4385 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧})) |
185 | 180, 184 | sylibr 226 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧})) |
186 | | simpllr 766 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦) |
187 | | elpwi 4389 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → (𝑢 ∪ {𝑧}) ⊆ 𝑦) |
188 | | ssun2 4000 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧}) |
189 | 27 | snss 4549 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧})) |
190 | 188, 189 | mpbir 223 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ (𝑢 ∪ {𝑧}) |
191 | 190 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑧 ∈ (𝑢 ∪ {𝑧})) |
192 | | ssel 3815 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∪ {𝑧}) ⊆ 𝑦 → (𝑧 ∈ (𝑢 ∪ {𝑧}) → 𝑧 ∈ 𝑦)) |
193 | 187, 191,
192 | syl2imc 41 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → 𝑧 ∈ 𝑦)) |
194 | 186, 193 | mtod 190 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ (𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦) |
195 | 185, 194 | eldifd 3803 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) |
196 | | eldifi 3955 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) |
197 | 196 | adantl 475 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) |
198 | 197 | elpwid 4391 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ (𝑦 ∪ {𝑧})) |
199 | | uncom 3980 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦) |
200 | 198, 199 | syl6sseq 3870 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ ({𝑧} ∪ 𝑦)) |
201 | | ssundif 4276 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦) |
202 | 200, 201 | sylib 210 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ⊆ 𝑦) |
203 | | vex 3401 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
204 | 203 | elpw2 5062 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦 ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦) |
205 | 202, 204 | sylibr 226 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦) |
206 | | elpwunsn 4452 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑧 ∈ 𝑠) |
207 | 206 | ad2antll 719 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑧 ∈ 𝑠) |
208 | 207 | snssd 4571 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → {𝑧} ⊆ 𝑠) |
209 | | ssequn2 4009 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑧} ⊆ 𝑠 ↔ (𝑠 ∪ {𝑧}) = 𝑠) |
210 | 208, 209 | sylib 210 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 ∪ {𝑧}) = 𝑠) |
211 | 210 | eqcomd 2784 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑠 = (𝑠 ∪ {𝑧})) |
212 | | uneq1 3983 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = ((𝑠 ∖ {𝑧}) ∪ {𝑧})) |
213 | | undif1 4267 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∖ {𝑧}) ∪ {𝑧}) = (𝑠 ∪ {𝑧}) |
214 | 212, 213 | syl6eq 2830 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = (𝑠 ∪ {𝑧})) |
215 | 214 | eqeq2d 2788 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑠 = (𝑢 ∪ {𝑧}) ↔ 𝑠 = (𝑠 ∪ {𝑧}))) |
216 | 211, 215 | syl5ibrcom 239 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) → 𝑠 = (𝑢 ∪ {𝑧}))) |
217 | 177 | ad2antrl 718 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 ⊆ 𝑦) |
218 | | simpllr 766 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑦) |
219 | 217, 218 | ssneldd 3824 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑢) |
220 | | difsnb 4568 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ 𝑢 ↔ (𝑢 ∖ {𝑧}) = 𝑢) |
221 | 219, 220 | sylib 210 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 ∖ {𝑧}) = 𝑢) |
222 | 221 | eqcomd 2784 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 = (𝑢 ∖ {𝑧})) |
223 | | difeq1 3944 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = ((𝑢 ∪ {𝑧}) ∖ {𝑧})) |
224 | | difun2 4272 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∪ {𝑧}) ∖ {𝑧}) = (𝑢 ∖ {𝑧}) |
225 | 223, 224 | syl6eq 2830 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = (𝑢 ∖ {𝑧})) |
226 | 225 | eqeq2d 2788 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑢 = (𝑢 ∖ {𝑧}))) |
227 | 222, 226 | syl5ibrcom 239 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 = (𝑢 ∪ {𝑧}) → 𝑢 = (𝑠 ∖ {𝑧}))) |
228 | 216, 227 | impbid 204 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑠 = (𝑢 ∪ {𝑧}))) |
229 | 176, 195,
205, 228 | f1o2d 7164 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})):𝒫 𝑦–1-1-onto→(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) |
230 | | uneq1 3983 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑡 → (𝑢 ∪ {𝑧}) = (𝑡 ∪ {𝑧})) |
231 | | vex 3401 |
. . . . . . . . . . . . . . 15
⊢ 𝑡 ∈ V |
232 | 231, 182 | unex 7233 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∪ {𝑧}) ∈ V |
233 | 230, 176,
232 | fvmpt 6542 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝒫 𝑦 → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧})) |
234 | 233 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑡 ∈ 𝒫 𝑦) → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧})) |
235 | 196, 164 | sylan2 586 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) ∈ ℂ) |
236 | 173, 175,
229, 234, 235 | fsumf1o 14861 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= Σ𝑡 ∈ 𝒫
𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧))))) |
237 | | uneq1 3983 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑠 → (𝑡 ∪ {𝑧}) = (𝑠 ∪ {𝑧})) |
238 | 237 | fveq2d 6450 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑠 → (♯‘(𝑡 ∪ {𝑧})) = (♯‘(𝑠 ∪ {𝑧}))) |
239 | 238 | oveq2d 6938 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑠 → (-1↑(♯‘(𝑡 ∪ {𝑧}))) = (-1↑(♯‘(𝑠 ∪ {𝑧})))) |
240 | | inteq 4713 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑠 → ∩ 𝑡 = ∩
𝑠) |
241 | 240 | ineq1d 4036 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑠 → (∩ 𝑡 ∩ 𝑧) = (∩ 𝑠 ∩ 𝑧)) |
242 | 241 | ineq2d 4037 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑠 → (𝑥 ∩ (∩ 𝑡 ∩ 𝑧)) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) |
243 | 242 | fveq2d 6450 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑠 → (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧))) = (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) |
244 | 239, 243 | oveq12d 6940 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑠 → ((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧)))) =
((-1↑(♯‘(𝑠
∪ {𝑧}))) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) |
245 | 244 | cbvsumv 14834 |
. . . . . . . . . . . 12
⊢
Σ𝑡 ∈
𝒫 𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) |
246 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → -1 ∈ ℂ) |
247 | | elpwi 4389 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ⊆ 𝑦) |
248 | | ssfi 8468 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ Fin ∧ 𝑠 ⊆ 𝑦) → 𝑠 ∈ Fin) |
249 | 144, 247,
248 | syl2an 589 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ Fin) |
250 | 249, 154 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘𝑠) ∈
ℕ0) |
251 | 246, 250 | expp1d 13328 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑((♯‘𝑠) + 1)) =
((-1↑(♯‘𝑠)) · -1)) |
252 | 247 | adantl 475 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ⊆ 𝑦) |
253 | | simpllr 766 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦) |
254 | 252, 253 | ssneldd 3824 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑠) |
255 | | hashunsng 13496 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ V → ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1))) |
256 | 255 | elv 3402 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1)) |
257 | 249, 254,
256 | syl2anc 579 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1)) |
258 | 257 | oveq2d 6938 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = (-1↑((♯‘𝑠) + 1))) |
259 | 139 | sseli 3817 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) |
260 | 259, 156 | sylan2 586 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘𝑠)) ∈
ℂ) |
261 | 246, 260 | mulcomd 10398 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 ·
(-1↑(♯‘𝑠))) = ((-1↑(♯‘𝑠)) ·
-1)) |
262 | 251, 258,
261 | 3eqtr4d 2824 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = (-1 ·
(-1↑(♯‘𝑠)))) |
263 | 260 | mulm1d 10827 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 ·
(-1↑(♯‘𝑠))) = -(-1↑(♯‘𝑠))) |
264 | 262, 263 | eqtrd 2814 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = -(-1↑(♯‘𝑠))) |
265 | 264 | oveq1d 6937 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) =
(-(-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) |
266 | | inss1 4053 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∩ (∩ 𝑠
∩ 𝑧)) ⊆ 𝑥 |
267 | | ssfi 8468 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∩ 𝑠
∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin) |
268 | 157, 266,
267 | sylancl 580 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin) |
269 | | hashcl 13462 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∩ (∩ 𝑠
∩ 𝑧)) ∈ Fin →
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))) ∈
ℕ0) |
270 | 268, 269 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈
ℕ0) |
271 | 270 | nn0cnd 11704 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ) |
272 | 259, 271 | sylan2 586 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ) |
273 | 260, 272 | mulneg1d 10828 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-(-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧)))) = -((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) |
274 | 265, 273 | eqtrd 2814 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) =
-((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) |
275 | 274 | sumeq2dv 14841 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) |
276 | 245, 275 | syl5eq 2826 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑡 ∈ 𝒫 𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡
∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) |
277 | 156, 271 | mulcld 10397 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧)))) ∈ ℂ) |
278 | 259, 277 | sylan2 586 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧)))) ∈ ℂ) |
279 | 175, 278 | fsumneg 14923 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧))))) |
280 | 236, 276,
279 | 3eqtrd 2818 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= -Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) |
281 | 280 | oveq2d 6938 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
+ -Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) |
282 | 139 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧})) |
283 | 282 | sselda 3821 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) |
284 | 283, 164 | syldan 585 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) ∈ ℂ) |
285 | 175, 284 | fsumcl 14871 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
∈ ℂ) |
286 | 283, 277 | syldan 585 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
(∩ 𝑠 ∩ 𝑧)))) ∈ ℂ) |
287 | 175, 286 | fsumcl 14871 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))) ∈
ℂ) |
288 | 285, 287 | negsubd 10740 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧))))) =
(Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
− Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) |
289 | 165, 281,
288 | 3eqtrd 2818 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= (Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
− Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) |
290 | 289 | adantr 474 |
. . . . . . 7
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
= (Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))
− Σ𝑠 ∈
𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠
∩ 𝑧)))))) |
291 | 102, 134,
290 | 3eqtr4d 2824 |
. . . . . 6
⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦
∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) |
292 | 291 | ex 403 |
. . . . 5
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
→ ((♯‘𝑥)
− (♯‘(𝑥
∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))) |
293 | 292 | ralrimdva 3151 |
. . . 4
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
→ ∀𝑥 ∈ Fin
((♯‘𝑥) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))) |
294 | | ineq1 4030 |
. . . . . . . 8
⊢ (𝑏 = 𝑥 → (𝑏 ∩ (∪ 𝑦 ∪ 𝑧)) = (𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) |
295 | 294 | fveq2d 6450 |
. . . . . . 7
⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧))) = (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) |
296 | 67, 295 | oveq12d 6940 |
. . . . . 6
⊢ (𝑏 = 𝑥 → ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))))) |
297 | | ineq1 4030 |
. . . . . . . . 9
⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠)) |
298 | 297 | fveq2d 6450 |
. . . . . . . 8
⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ ∩ 𝑠))) |
299 | 298 | oveq2d 6938 |
. . . . . . 7
⊢ (𝑏 = 𝑥 → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = ((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠)))) |
300 | 299 | sumeq2sdv 14842 |
. . . . . 6
⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
(𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) ·
(♯‘(𝑥 ∩
∩ 𝑠)))) |
301 | 296, 300 | eqeq12d 2793 |
. . . . 5
⊢ (𝑏 = 𝑥 → (((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝑥)
− (♯‘(𝑥
∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))) |
302 | 301 | cbvralv 3367 |
. . . 4
⊢
(∀𝑏 ∈
Fin ((♯‘𝑏)
− (♯‘(𝑏
∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ∀𝑥 ∈ Fin
((♯‘𝑥) −
(♯‘(𝑥 ∩
(∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) |
303 | 293, 302 | syl6ibr 244 |
. . 3
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦)))
= Σ𝑠 ∈ 𝒫
𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
→ ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
(∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))) |
304 | 16, 24, 38, 46, 66, 303 | findcard2s 8489 |
. 2
⊢ (𝐴 ∈ Fin → ∀𝑏 ∈ Fin
((♯‘𝑏) −
(♯‘(𝑏 ∩
∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) |
305 | | fveq2 6446 |
. . . . 5
⊢ (𝑏 = 𝐵 → (♯‘𝑏) = (♯‘𝐵)) |
306 | | ineq1 4030 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (𝑏 ∩ ∪ 𝐴) = (𝐵 ∩ ∪ 𝐴)) |
307 | 306 | fveq2d 6450 |
. . . . 5
⊢ (𝑏 = 𝐵 → (♯‘(𝑏 ∩ ∪ 𝐴)) = (♯‘(𝐵 ∩ ∪ 𝐴))) |
308 | 305, 307 | oveq12d 6940 |
. . . 4
⊢ (𝑏 = 𝐵 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴)))) |
309 | | simpl 476 |
. . . . . . . 8
⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑏 = 𝐵) |
310 | 309 | ineq1d 4036 |
. . . . . . 7
⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (𝑏 ∩ ∩ 𝑠) = (𝐵 ∩ ∩ 𝑠)) |
311 | 310 | fveq2d 6450 |
. . . . . 6
⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝐵 ∩ ∩ 𝑠))) |
312 | 311 | oveq2d 6938 |
. . . . 5
⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → ((-1↑(♯‘𝑠)) ·
(♯‘(𝑏 ∩
∩ 𝑠))) = ((-1↑(♯‘𝑠)) ·
(♯‘(𝐵 ∩
∩ 𝑠)))) |
313 | 312 | sumeq2dv 14841 |
. . . 4
⊢ (𝑏 = 𝐵 → Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
= Σ𝑠 ∈ 𝒫
𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))) |
314 | 308, 313 | eqeq12d 2793 |
. . 3
⊢ (𝑏 = 𝐵 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
↔ ((♯‘𝐵)
− (♯‘(𝐵
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))) |
315 | 314 | rspccva 3510 |
. 2
⊢
((∀𝑏 ∈
Fin ((♯‘𝑏)
− (♯‘(𝑏
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
∧ 𝐵 ∈ Fin) →
((♯‘𝐵) −
(♯‘(𝐵 ∩
∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))) |
316 | 304, 315 | sylan 575 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐵) −
(♯‘(𝐵 ∩
∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))) |