Proof of Theorem incexc
Step | Hyp | Ref
| Expression |
1 | | unifi 8138 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴
∈ Fin) |
2 | | hashcl 13009 |
. . . 4
⊢ (∪ 𝐴
∈ Fin → (#‘∪ 𝐴) ∈
ℕ0) |
3 | 2 | nn0cnd 11230 |
. . 3
⊢ (∪ 𝐴
∈ Fin → (#‘∪ 𝐴) ∈ ℂ) |
4 | 1, 3 | syl 17 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(#‘∪ 𝐴) ∈ ℂ) |
5 | | simpl 472 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin) |
6 | | pwfi 8144 |
. . . . 5
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
7 | 5, 6 | sylib 207 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫
𝐴 ∈
Fin) |
8 | | diffi 8077 |
. . . 4
⊢
(𝒫 𝐴 ∈
Fin → (𝒫 𝐴
∖ {∅}) ∈ Fin) |
9 | 7, 8 | syl 17 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (𝒫
𝐴 ∖ {∅}) ∈
Fin) |
10 | | 1cnd 9935 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → 1
∈ ℂ) |
11 | 10 | negcld 10258 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → -1
∈ ℂ) |
12 | | eldifsni 4261 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ≠ ∅) |
13 | 12 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝑠 ≠
∅) |
14 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ∈ 𝒫 𝐴) |
15 | | elpwi 4117 |
. . . . . . . . . 10
⊢ (𝑠 ∈ 𝒫 𝐴 → 𝑠 ⊆ 𝐴) |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝒫 𝐴 ∖ {∅}) → 𝑠 ⊆ 𝐴) |
17 | | ssfi 8065 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Fin ∧ 𝑠 ⊆ 𝐴) → 𝑠 ∈ Fin) |
18 | 5, 16, 17 | syl2an 493 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝑠 ∈
Fin) |
19 | | hashnncl 13018 |
. . . . . . . 8
⊢ (𝑠 ∈ Fin →
((#‘𝑠) ∈ ℕ
↔ 𝑠 ≠
∅)) |
20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((#‘𝑠) ∈ ℕ
↔ 𝑠 ≠
∅)) |
21 | 13, 20 | mpbird 246 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(#‘𝑠) ∈
ℕ) |
22 | | nnm1nn0 11211 |
. . . . . 6
⊢
((#‘𝑠) ∈
ℕ → ((#‘𝑠)
− 1) ∈ ℕ0) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((#‘𝑠) − 1)
∈ ℕ0) |
24 | 11, 23 | expcld 12870 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(-1↑((#‘𝑠)
− 1)) ∈ ℂ) |
25 | 16 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝑠 ⊆ 𝐴) |
26 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝐴 ⊆
Fin) |
27 | 25, 26 | sstrd 3578 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
𝑠 ⊆
Fin) |
28 | | unifi 8138 |
. . . . . . . 8
⊢ ((𝑠 ∈ Fin ∧ 𝑠 ⊆ Fin) → ∪ 𝑠
∈ Fin) |
29 | 18, 27, 28 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∪ 𝑠 ∈ Fin) |
30 | | intssuni 4434 |
. . . . . . . 8
⊢ (𝑠 ≠ ∅ → ∩ 𝑠
⊆ ∪ 𝑠) |
31 | 13, 30 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∩ 𝑠 ⊆ ∪ 𝑠) |
32 | | ssfi 8065 |
. . . . . . 7
⊢ ((∪ 𝑠
∈ Fin ∧ ∩ 𝑠 ⊆ ∪ 𝑠) → ∩ 𝑠
∈ Fin) |
33 | 29, 31, 32 | syl2anc 691 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∩ 𝑠 ∈ Fin) |
34 | | hashcl 13009 |
. . . . . 6
⊢ (∩ 𝑠
∈ Fin → (#‘∩ 𝑠) ∈
ℕ0) |
35 | 33, 34 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(#‘∩ 𝑠) ∈
ℕ0) |
36 | 35 | nn0cnd 11230 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(#‘∩ 𝑠) ∈ ℂ) |
37 | 24, 36 | mulcld 9939 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((-1↑((#‘𝑠)
− 1)) · (#‘∩ 𝑠)) ∈ ℂ) |
38 | 9, 37 | fsumcl 14311 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
∈ ℂ) |
39 | | disjdif 3992 |
. . . . 5
⊢
({∅} ∩ (𝒫 𝐴 ∖ {∅})) =
∅ |
40 | 39 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ({∅}
∩ (𝒫 𝐴 ∖
{∅})) = ∅) |
41 | | 0elpw 4760 |
. . . . . . . 8
⊢ ∅
∈ 𝒫 𝐴 |
42 | | snssi 4280 |
. . . . . . . 8
⊢ (∅
∈ 𝒫 𝐴 →
{∅} ⊆ 𝒫 𝐴) |
43 | 41, 42 | ax-mp 5 |
. . . . . . 7
⊢ {∅}
⊆ 𝒫 𝐴 |
44 | | undif 4001 |
. . . . . . 7
⊢
({∅} ⊆ 𝒫 𝐴 ↔ ({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫
𝐴) |
45 | 43, 44 | mpbi 219 |
. . . . . 6
⊢
({∅} ∪ (𝒫 𝐴 ∖ {∅})) = 𝒫 𝐴 |
46 | 45 | eqcomi 2619 |
. . . . 5
⊢ 𝒫
𝐴 = ({∅} ∪
(𝒫 𝐴 ∖
{∅})) |
47 | 46 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝒫
𝐴 = ({∅} ∪
(𝒫 𝐴 ∖
{∅}))) |
48 | | 1cnd 9935 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 1 ∈
ℂ) |
49 | 48 | negcld 10258 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → -1 ∈
ℂ) |
50 | 5, 15, 17 | syl2an 493 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑠 ∈ Fin) |
51 | | hashcl 13009 |
. . . . . . 7
⊢ (𝑠 ∈ Fin →
(#‘𝑠) ∈
ℕ0) |
52 | 50, 51 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (#‘𝑠) ∈
ℕ0) |
53 | 49, 52 | expcld 12870 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (-1↑(#‘𝑠)) ∈
ℂ) |
54 | 1 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → ∪ 𝐴
∈ Fin) |
55 | | inss1 3795 |
. . . . . . . 8
⊢ (∪ 𝐴
∩ ∩ 𝑠) ⊆ ∪ 𝐴 |
56 | | ssfi 8065 |
. . . . . . . 8
⊢ ((∪ 𝐴
∈ Fin ∧ (∪ 𝐴 ∩ ∩ 𝑠) ⊆ ∪ 𝐴)
→ (∪ 𝐴 ∩ ∩ 𝑠) ∈ Fin) |
57 | 54, 55, 56 | sylancl 693 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (∪ 𝐴
∩ ∩ 𝑠) ∈ Fin) |
58 | | hashcl 13009 |
. . . . . . 7
⊢ ((∪ 𝐴
∩ ∩ 𝑠) ∈ Fin → (#‘(∪ 𝐴
∩ ∩ 𝑠)) ∈
ℕ0) |
59 | 57, 58 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (#‘(∪ 𝐴
∩ ∩ 𝑠)) ∈
ℕ0) |
60 | 59 | nn0cnd 11230 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) → (#‘(∪ 𝐴
∩ ∩ 𝑠)) ∈ ℂ) |
61 | 53, 60 | mulcld 9939 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ 𝒫 𝐴) →
((-1↑(#‘𝑠))
· (#‘(∪ 𝐴 ∩ ∩ 𝑠))) ∈
ℂ) |
62 | 40, 47, 7, 61 | fsumsplit 14318 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ 𝒫
𝐴((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠))))) |
63 | | inidm 3784 |
. . . . . . 7
⊢ (∪ 𝐴
∩ ∪ 𝐴) = ∪ 𝐴 |
64 | 63 | fveq2i 6106 |
. . . . . 6
⊢
(#‘(∪ 𝐴 ∩ ∪ 𝐴)) = (#‘∪ 𝐴) |
65 | 64 | oveq2i 6560 |
. . . . 5
⊢
((#‘∪ 𝐴) − (#‘(∪ 𝐴
∩ ∪ 𝐴))) = ((#‘∪
𝐴) − (#‘∪ 𝐴)) |
66 | 4 | subidd 10259 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((#‘∪ 𝐴) − (#‘∪ 𝐴))
= 0) |
67 | 65, 66 | syl5eq 2656 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((#‘∪ 𝐴) − (#‘(∪ 𝐴
∩ ∪ 𝐴))) = 0) |
68 | | incexclem 14407 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ ∪ 𝐴
∈ Fin) → ((#‘∪ 𝐴) − (#‘(∪ 𝐴
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠)))) |
69 | 1, 68 | syldan 486 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((#‘∪ 𝐴) − (#‘(∪ 𝐴
∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠)))) |
70 | 67, 69 | eqtr3d 2646 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 0 =
Σ𝑠 ∈ 𝒫
𝐴((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠)))) |
71 | 4, 38 | negsubd 10277 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((#‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠))) = ((#‘∪
𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖
{∅})((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠)))) |
72 | | 0ex 4718 |
. . . . . . 7
⊢ ∅
∈ V |
73 | | 1cnd 9935 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 1 ∈
ℂ) |
74 | 73, 4 | mulcld 9939 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 ·
(#‘∪ 𝐴)) ∈ ℂ) |
75 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑠 = ∅ → (#‘𝑠) =
(#‘∅)) |
76 | | hash0 13019 |
. . . . . . . . . . . 12
⊢
(#‘∅) = 0 |
77 | 75, 76 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑠 = ∅ → (#‘𝑠) = 0) |
78 | 77 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑠 = ∅ →
(-1↑(#‘𝑠)) =
(-1↑0)) |
79 | | neg1cn 11001 |
. . . . . . . . . . 11
⊢ -1 ∈
ℂ |
80 | | exp0 12726 |
. . . . . . . . . . 11
⊢ (-1
∈ ℂ → (-1↑0) = 1) |
81 | 79, 80 | ax-mp 5 |
. . . . . . . . . 10
⊢
(-1↑0) = 1 |
82 | 78, 81 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑠 = ∅ →
(-1↑(#‘𝑠)) =
1) |
83 | | rint0 4452 |
. . . . . . . . . 10
⊢ (𝑠 = ∅ → (∪ 𝐴
∩ ∩ 𝑠) = ∪ 𝐴) |
84 | 83 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑠 = ∅ →
(#‘(∪ 𝐴 ∩ ∩ 𝑠)) = (#‘∪ 𝐴)) |
85 | 82, 84 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑠 = ∅ →
((-1↑(#‘𝑠))
· (#‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (#‘∪ 𝐴))) |
86 | 85 | sumsn 14319 |
. . . . . . 7
⊢ ((∅
∈ V ∧ (1 · (#‘∪ 𝐴)) ∈ ℂ) →
Σ𝑠 ∈ {∅}
((-1↑(#‘𝑠))
· (#‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (#‘∪ 𝐴))) |
87 | 72, 74, 86 | sylancr 694 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ {∅}
((-1↑(#‘𝑠))
· (#‘(∪ 𝐴 ∩ ∩ 𝑠))) = (1 · (#‘∪ 𝐴))) |
88 | 4 | mulid2d 9937 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (1 ·
(#‘∪ 𝐴)) = (#‘∪
𝐴)) |
89 | 87, 88 | eqtr2d 2645 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(#‘∪ 𝐴) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠)))) |
90 | 9, 37 | fsumneg 14361 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})-((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= -Σ𝑠 ∈
(𝒫 𝐴 ∖
{∅})((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))) |
91 | | expm1t 12750 |
. . . . . . . . . . 11
⊢ ((-1
∈ ℂ ∧ (#‘𝑠) ∈ ℕ) →
(-1↑(#‘𝑠)) =
((-1↑((#‘𝑠)
− 1)) · -1)) |
92 | 11, 21, 91 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(-1↑(#‘𝑠)) =
((-1↑((#‘𝑠)
− 1)) · -1)) |
93 | 24, 11 | mulcomd 9940 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((-1↑((#‘𝑠)
− 1)) · -1) = (-1 · (-1↑((#‘𝑠) − 1)))) |
94 | 24 | mulm1d 10361 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) → (-1
· (-1↑((#‘𝑠) − 1))) = -(-1↑((#‘𝑠) − 1))) |
95 | 92, 93, 94 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(-1↑(#‘𝑠)) =
-(-1↑((#‘𝑠)
− 1))) |
96 | 25 | unissd 4398 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∪ 𝑠 ⊆ ∪ 𝐴) |
97 | 31, 96 | sstrd 3578 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
∩ 𝑠 ⊆ ∪ 𝐴) |
98 | | sseqin2 3779 |
. . . . . . . . . . 11
⊢ (∩ 𝑠
⊆ ∪ 𝐴 ↔ (∪ 𝐴 ∩ ∩ 𝑠) =
∩ 𝑠) |
99 | 97, 98 | sylib 207 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(∪ 𝐴 ∩ ∩ 𝑠) = ∩
𝑠) |
100 | 99 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(#‘(∪ 𝐴 ∩ ∩ 𝑠)) = (#‘∩ 𝑠)) |
101 | 95, 100 | oveq12d 6567 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
((-1↑(#‘𝑠))
· (#‘(∪ 𝐴 ∩ ∩ 𝑠))) = (-(-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠))) |
102 | 24, 36 | mulneg1d 10362 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
(-(-1↑((#‘𝑠)
− 1)) · (#‘∩ 𝑠)) = -((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))) |
103 | 101, 102 | eqtr2d 2645 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑠 ∈ (𝒫 𝐴 ∖ {∅})) →
-((-1↑((#‘𝑠)
− 1)) · (#‘∩ 𝑠)) = ((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠)))) |
104 | 103 | sumeq2dv 14281 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})-((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= Σ𝑠 ∈
(𝒫 𝐴 ∖
{∅})((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠)))) |
105 | 90, 104 | eqtr3d 2646 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
-Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= Σ𝑠 ∈
(𝒫 𝐴 ∖
{∅})((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠)))) |
106 | 89, 105 | oveq12d 6567 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((#‘∪ 𝐴) + -Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠))))) |
107 | 71, 106 | eqtr3d 2646 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((#‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠))) = (Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑(#‘𝑠)) · (#‘(∪ 𝐴
∩ ∩ 𝑠))))) |
108 | 62, 70, 107 | 3eqtr4rd 2655 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
((#‘∪ 𝐴) − Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠))) = 0) |
109 | 4, 38, 108 | subeq0d 10279 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(#‘∪ 𝐴) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠))) |