Proof of Theorem incexc
Step | Hyp | Ref
| Expression |
1 | | unifi 8255 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴
∈ Fin) |
2 | | hashcl 13147 |
. . . 4
⊢ (∪ 𝐴
∈ Fin → (#‘∪ 𝐴) ∈
ℕ0) |
3 | 2 | nn0cnd 11353 |
. . 3
⊢ (∪ 𝐴
∈ Fin → (#‘∪ 𝐴) ∈ ℂ) |
4 | 1, 3 | syl 17 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(#‘∪ 𝐴) ∈ ℂ) |
5 | | simpl 473 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin) |
6 | | pwfi 8261 |
. . . . 5
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
7 | 5, 6 | sylib 208 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫
𝐴 ∈
Fin) |
8 | | diffi 8192 |
. . . 4
⊢
(𝒫 𝐴 ∈
Fin → (𝒫 𝐴
∖ {∅}) ∈ Fin) |
9 | 7, 8 | syl 17 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (𝒫
𝐴 ∖ {∅}) ∈
Fin) |
10 | | 1cnd 10056 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 1
∈ ℂ) |
11 | 10 | negcld 10379 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → -1
∈ ℂ) |
12 | | eldifsni 4320 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ≠ ∅) |
13 | 12 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝑠 ≠
∅) |
14 | | eldifi 3732 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ∈ 𝒫 𝐴) |
15 | | elpwi 4168 |
. . . . . . . . . 10
⊢ (𝑠 ∈ 𝒫 𝐴 → 𝑠 ⊆ 𝐴) |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ⊆ 𝐴) |
17 | | ssfi 8180 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Fin ∧ 𝑠 ⊆ 𝐴) → 𝑠 ∈ Fin) |
18 | 5, 16, 17 | syl2an 494 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝑠 ∈
Fin) |
19 | | hashnncl 13157 |
. . . . . . . 8
⊢ (𝑠 ∈ Fin →
((#‘𝑠) ∈ ℕ
↔ 𝑠 ≠
∅)) |
20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((#‘𝑠) ∈ ℕ
↔ 𝑠 ≠
∅)) |
21 | 13, 20 | mpbird 247 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(#‘𝑠) ∈
ℕ) |
22 | | nnm1nn0 11334 |
. . . . . 6
⊢
((#‘𝑠) ∈
ℕ → ((#‘𝑠)
− 1) ∈ ℕ0) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((#‘𝑠) − 1)
∈ ℕ0) |
24 | 11, 23 | expcld 13008 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(-1↑((#‘𝑠)
− 1)) ∈ ℂ) |
25 | 16 | adantl 482 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝑠 ⊆ 𝐴) |
26 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝐴 ⊆
Fin) |
27 | 25, 26 | sstrd 3613 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝑠 ⊆
Fin) |
28 | | unifi 8255 |
. . . . . . . 8
⊢ ((𝑠 ∈ Fin ∧ 𝑠 ⊆ Fin) → ∪ 𝑠
∈ Fin) |
29 | 18, 27, 28 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∪ 𝑠 ∈ Fin) |
30 | | intssuni 4499 |
. . . . . . . 8
⊢ (𝑠 ≠ ∅ → ∩ 𝑠
⊆ ∪ 𝑠) |
31 | 13, 30 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∩ 𝑠 ⊆ ∪ 𝑠) |
32 | | ssfi 8180 |
. . . . . . 7
⊢ ((∪ 𝑠
∈ Fin ∧ ∩ 𝑠 ⊆ ∪ 𝑠) → ∩ 𝑠
∈ Fin) |
33 | 29, 31, 32 | syl2anc 693 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∩ 𝑠 ∈ Fin) |
34 | | hashcl 13147 |
. . . . . 6
⊢ (∩ 𝑠
∈ Fin → (#‘∩ 𝑠) ∈
ℕ0) |
35 | 33, 34 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(#‘∩ 𝑠) ∈
ℕ0) |
36 | 35 | nn0cnd 11353 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(#‘∩ 𝑠) ∈ ℂ) |
37 | 24, 36 | mulcld 10060 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((-1↑((#‘𝑠)
− 1)) · (#‘∩ 𝑠)) ∈ ℂ) |
38 | 9, 37 | fsumcl 14464 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
∈ ℂ) |
39 | | disjdif 4040 |
. . . . 5
⊢
({∅} ∩ (𝒫 𝐴 ∖ {∅})) =
∅ |
40 | 39 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ({∅}
∩ (𝒫 𝐴 ∖
{∅})) = ∅) |
41 | | 0elpw 4834 |
. . . . . . . 8
⊢ ∅
∈ 𝒫 𝐴 |
42 | | snssi 4339 |
. . . . . . . 8
⊢ (∅
∈ 𝒫 𝐴 →
{∅} ⊆ 𝒫 𝐴) |
43 | 41, 42 | ax-mp 5 |
. . . . . . 7
⊢ {∅}
⊆ 𝒫 𝐴 |
44 | | undif 4049 |
. . . . . . 7
⊢
({∅} ⊆ 𝒫 𝐴 ↔ ({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫
𝐴) |
45 | 43, 44 | mpbi 220 |
. . . . . 6
⊢
({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫 𝐴 |
46 | 45 | eqcomi 2631 |
. . . . 5
⊢ 𝒫
𝐴 = ({∅} ∪
(𝒫 𝐴 ∖
{∅})) |
47 | 46 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫
𝐴 = ({∅} ∪
(𝒫 𝐴 ∖
{∅}))) |
48 | | 1cnd 10056 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 1 ∈
ℂ) |
49 | 48 | negcld 10379 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → -1 ∈
ℂ) |
50 | 5, 15, 17 | syl2an 494 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑠 ∈ Fin) |
51 | | hashcl 13147 |
. . . . . . 7
⊢ (𝑠 ∈ Fin →
(#‘𝑠) ∈
ℕ0) |
52 | 50, 51 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (#‘𝑠) ∈
ℕ0) |
53 | 49, 52 | expcld 13008 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (-1↑(#‘𝑠)) ∈
ℂ) |
54 | 1 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → ∪ 𝐴
∈ Fin) |
55 | | inss1 3833 |
. . . . . . . 8
⊢ (∪ 𝐴
∩ ∩ 𝑠) ⊆ ∪ 𝐴 |
56 | | ssfi 8180 |
. . . . . . . 8
⊢ ((∪ 𝐴
∈ Fin ∧ (∪ 𝐴 ∩ ∩ 𝑠) ⊆ ∪ 𝐴)
→ (∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin) |
57 | 54, 55, 56 | sylancl 694 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (∪ 𝐴
∩ ∩ 𝑠) ∈ Fin) |
58 | | hashcl 13147 |
. . . . . . 7
⊢ ((∪ 𝐴
∩ ∩ 𝑠) ∈ Fin → (#‘(∪ 𝐴
∩ ∩ 𝑠)) ∈
ℕ0) |
59 | 57, 58 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (#‘(∪ 𝐴
∩ ∩ 𝑠)) ∈
ℕ0) |
60 | 59 | nn0cnd 11353 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (#‘(∪ 𝐴
∩ ∩ 𝑠)) ∈ ℂ) |
61 | 53, 60 | mulcld 10060 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) →
((-1↑(#‘𝑠))
· (#‘(∪ 𝐴 ∩ ∩ 𝑠))) ∈
ℂ) |
62 | 40, 47, 7, 61 | fsumsplit 14471 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ 𝒫
𝐴((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠))))) |
63 | | inidm 3822 |
. . . . . . 7
⊢ (∪ 𝐴
∩ ∪ 𝐴) = ∪ 𝐴 |
64 | 63 | fveq2i 6194 |
. . . . . 6
⊢
(#‘(∪ 𝐴 ∩ ∪ 𝐴)) = (#‘∪ 𝐴) |
65 | 64 | oveq2i 6661 |
. . . . 5
⊢
((#‘∪ 𝐴) − (#‘(∪ 𝐴
∩ ∪ 𝐴))) = ((#‘∪
𝐴) − (#‘∪ 𝐴)) |
66 | 4 | subidd 10380 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((#‘∪ 𝐴) − (#‘∪ 𝐴))
= 0) |
67 | 65, 66 | syl5eq 2668 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((#‘∪ 𝐴) − (#‘(∪ 𝐴
∩ ∪ 𝐴))) = 0) |
68 | | incexclem 14568 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ ∪ 𝐴
∈ Fin) → ((#‘∪ 𝐴) − (#‘(∪ 𝐴
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠)))) |
69 | 1, 68 | syldan 487 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((#‘∪ 𝐴) − (#‘(∪ 𝐴
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠)))) |
70 | 67, 69 | eqtr3d 2658 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 0 =
Σ𝑠 ∈ 𝒫
𝐴((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠)))) |
71 | 4, 38 | negsubd 10398 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((#‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠))) = ((#‘∪
𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖
{∅})((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠)))) |
72 | | 0ex 4790 |
. . . . . . 7
⊢ ∅
∈ V |
73 | | 1cnd 10056 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 1 ∈
ℂ) |
74 | 73, 4 | mulcld 10060 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 ·
(#‘∪ 𝐴)) ∈ ℂ) |
75 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑠 = ∅ → (#‘𝑠) =
(#‘∅)) |
76 | | hash0 13158 |
. . . . . . . . . . . 12
⊢
(#‘∅) = 0 |
77 | 75, 76 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝑠 = ∅ → (#‘𝑠) = 0) |
78 | 77 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑠 = ∅ →
(-1↑(#‘𝑠)) =
(-1↑0)) |
79 | | neg1cn 11124 |
. . . . . . . . . . 11
⊢ -1 ∈
ℂ |
80 | | exp0 12864 |
. . . . . . . . . . 11
⊢ (-1
∈ ℂ → (-1↑0) = 1) |
81 | 79, 80 | ax-mp 5 |
. . . . . . . . . 10
⊢
(-1↑0) = 1 |
82 | 78, 81 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑠 = ∅ →
(-1↑(#‘𝑠)) =
1) |
83 | | rint0 4517 |
. . . . . . . . . 10
⊢ (𝑠 = ∅ → (∪ 𝐴
∩ ∩ 𝑠) = ∪ 𝐴) |
84 | 83 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑠 = ∅ →
(#‘(∪ 𝐴 ∩ ∩ 𝑠)) = (#‘∪ 𝐴)) |
85 | 82, 84 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑠 = ∅ →
((-1↑(#‘𝑠))
· (#‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (#‘∪ 𝐴))) |
86 | 85 | sumsn 14475 |
. . . . . . 7
⊢ ((∅
∈ V ∧ (1 · (#‘∪ 𝐴)) ∈ ℂ) →
Σ𝑠 ∈ {∅}
((-1↑(#‘𝑠))
· (#‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (#‘∪ 𝐴))) |
87 | 72, 74, 86 | sylancr 695 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ {∅}
((-1↑(#‘𝑠))
· (#‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (#‘∪ 𝐴))) |
88 | 4 | mulid2d 10058 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 ·
(#‘∪ 𝐴)) = (#‘∪
𝐴)) |
89 | 87, 88 | eqtr2d 2657 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(#‘∪ 𝐴) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠)))) |
90 | 9, 37 | fsumneg 14519 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})-((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= -Σ𝑠 ∈
(𝒫 𝐴 ∖
{∅})((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))) |
91 | | expm1t 12888 |
. . . . . . . . . . 11
⊢ ((-1
∈ ℂ ∧ (#‘𝑠) ∈ ℕ) →
(-1↑(#‘𝑠)) =
((-1↑((#‘𝑠)
− 1)) · -1)) |
92 | 11, 21, 91 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(-1↑(#‘𝑠)) =
((-1↑((#‘𝑠)
− 1)) · -1)) |
93 | 24, 11 | mulcomd 10061 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((-1↑((#‘𝑠)
− 1)) · -1) = (-1 · (-1↑((#‘𝑠) − 1)))) |
94 | 24 | mulm1d 10482 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1
· (-1↑((#‘𝑠) − 1))) = -(-1↑((#‘𝑠) − 1))) |
95 | 92, 93, 94 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(-1↑(#‘𝑠)) =
-(-1↑((#‘𝑠)
− 1))) |
96 | 25 | unissd 4462 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∪ 𝑠 ⊆ ∪ 𝐴) |
97 | 31, 96 | sstrd 3613 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∩ 𝑠 ⊆ ∪ 𝐴) |
98 | | sseqin2 3817 |
. . . . . . . . . . 11
⊢ (∩ 𝑠
⊆ ∪ 𝐴 ↔ (∪ 𝐴 ∩ ∩ 𝑠) =
∩ 𝑠) |
99 | 97, 98 | sylib 208 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(∪ 𝐴 ∩ ∩ 𝑠) = ∩
𝑠) |
100 | 99 | fveq2d 6195 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(#‘(∪ 𝐴 ∩ ∩ 𝑠)) = (#‘∩ 𝑠)) |
101 | 95, 100 | oveq12d 6668 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((-1↑(#‘𝑠))
· (#‘(∪ 𝐴 ∩ ∩ 𝑠))) = (-(-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠))) |
102 | 24, 36 | mulneg1d 10483 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(-(-1↑((#‘𝑠)
− 1)) · (#‘∩ 𝑠)) = -((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))) |
103 | 101, 102 | eqtr2d 2657 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
-((-1↑((#‘𝑠)
− 1)) · (#‘∩ 𝑠)) = ((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠)))) |
104 | 103 | sumeq2dv 14433 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})-((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= Σ𝑠 ∈
(𝒫 𝐴 ∖
{∅})((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠)))) |
105 | 90, 104 | eqtr3d 2658 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
-Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= Σ𝑠 ∈
(𝒫 𝐴 ∖
{∅})((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠)))) |
106 | 89, 105 | oveq12d 6668 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((#‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠))))) |
107 | 71, 106 | eqtr3d 2658 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((#‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠))))) |
108 | 62, 70, 107 | 3eqtr4rd 2667 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((#‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠))) = 0) |
109 | 4, 38, 108 | subeq0d 10400 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(#‘∪ 𝐴) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠))) |