Step | Hyp | Ref
| Expression |
1 | | incexc 15729 |
. . 3
โข ((๐ด โ Fin โง ๐ด โ Fin) โ
(โฏโโช ๐ด) = ฮฃ๐ โ (๐ซ ๐ด โ
{โ
})((-1โ((โฏโ๐ ) โ 1)) ยท (โฏโโฉ ๐ ))) |
2 | | hashcl 14263 |
. . . . . . . . . . . 12
โข (๐ด โ Fin โ
(โฏโ๐ด) โ
โ0) |
3 | 2 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ ๐ซ ๐ด) โ (โฏโ๐ด) โ
โ0) |
4 | 3 | nn0zd 12532 |
. . . . . . . . . 10
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ ๐ซ ๐ด) โ (โฏโ๐ด) โ
โค) |
5 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ด โ Fin โง ๐ด โ Fin) โ ๐ด โ Fin) |
6 | | elpwi 4572 |
. . . . . . . . . . . 12
โข (๐ โ ๐ซ ๐ด โ ๐ โ ๐ด) |
7 | | ssdomg 8947 |
. . . . . . . . . . . . 13
โข (๐ด โ Fin โ (๐ โ ๐ด โ ๐ โผ ๐ด)) |
8 | 7 | imp 408 |
. . . . . . . . . . . 12
โข ((๐ด โ Fin โง ๐ โ ๐ด) โ ๐ โผ ๐ด) |
9 | 5, 6, 8 | syl2an 597 |
. . . . . . . . . . 11
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ ๐ซ ๐ด) โ ๐ โผ ๐ด) |
10 | | hashdomi 14287 |
. . . . . . . . . . 11
โข (๐ โผ ๐ด โ (โฏโ๐) โค (โฏโ๐ด)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ ๐ซ ๐ด) โ (โฏโ๐) โค (โฏโ๐ด)) |
12 | | fznn 13516 |
. . . . . . . . . . 11
โข
((โฏโ๐ด)
โ โค โ ((โฏโ๐) โ (1...(โฏโ๐ด)) โ ((โฏโ๐) โ โ โง
(โฏโ๐) โค
(โฏโ๐ด)))) |
13 | 12 | rbaibd 542 |
. . . . . . . . . 10
โข
(((โฏโ๐ด)
โ โค โง (โฏโ๐) โค (โฏโ๐ด)) โ ((โฏโ๐) โ (1...(โฏโ๐ด)) โ (โฏโ๐) โ
โ)) |
14 | 4, 11, 13 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ ๐ซ ๐ด) โ ((โฏโ๐) โ
(1...(โฏโ๐ด))
โ (โฏโ๐)
โ โ)) |
15 | | ssfi 9124 |
. . . . . . . . . . 11
โข ((๐ด โ Fin โง ๐ โ ๐ด) โ ๐ โ Fin) |
16 | 5, 6, 15 | syl2an 597 |
. . . . . . . . . 10
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ ๐ซ ๐ด) โ ๐ โ Fin) |
17 | | hashnncl 14273 |
. . . . . . . . . 10
โข (๐ โ Fin โ
((โฏโ๐) โ
โ โ ๐ โ
โ
)) |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ ๐ซ ๐ด) โ ((โฏโ๐) โ โ โ ๐ โ โ
)) |
19 | 14, 18 | bitr2d 280 |
. . . . . . . 8
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ ๐ซ ๐ด) โ (๐ โ โ
โ (โฏโ๐) โ
(1...(โฏโ๐ด)))) |
20 | | df-ne 2945 |
. . . . . . . 8
โข (๐ โ โ
โ ยฌ ๐ = โ
) |
21 | | risset 3224 |
. . . . . . . 8
โข
((โฏโ๐)
โ (1...(โฏโ๐ด)) โ โ๐ โ (1...(โฏโ๐ด))๐ = (โฏโ๐)) |
22 | 19, 20, 21 | 3bitr3g 313 |
. . . . . . 7
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ ๐ซ ๐ด) โ (ยฌ ๐ = โ
โ โ๐ โ
(1...(โฏโ๐ด))๐ = (โฏโ๐))) |
23 | | velsn 4607 |
. . . . . . . 8
โข (๐ โ {โ
} โ ๐ = โ
) |
24 | 23 | notbii 320 |
. . . . . . 7
โข (ยฌ
๐ โ {โ
} โ
ยฌ ๐ =
โ
) |
25 | | eqcom 2744 |
. . . . . . . 8
โข
((โฏโ๐) =
๐ โ ๐ = (โฏโ๐)) |
26 | 25 | rexbii 3098 |
. . . . . . 7
โข
(โ๐ โ
(1...(โฏโ๐ด))(โฏโ๐) = ๐ โ โ๐ โ (1...(โฏโ๐ด))๐ = (โฏโ๐)) |
27 | 22, 24, 26 | 3bitr4g 314 |
. . . . . 6
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ ๐ซ ๐ด) โ (ยฌ ๐ โ {โ
} โ
โ๐ โ
(1...(โฏโ๐ด))(โฏโ๐) = ๐)) |
28 | 27 | rabbidva 3417 |
. . . . 5
โข ((๐ด โ Fin โง ๐ด โ Fin) โ {๐ โ ๐ซ ๐ด โฃ ยฌ ๐ โ {โ
}} = {๐ โ ๐ซ ๐ด โฃ โ๐ โ
(1...(โฏโ๐ด))(โฏโ๐) = ๐}) |
29 | | dfdif2 3924 |
. . . . 5
โข
(๐ซ ๐ด โ
{โ
}) = {๐ โ
๐ซ ๐ด โฃ ยฌ
๐ โ
{โ
}} |
30 | | iunrab 5017 |
. . . . 5
โข โช ๐ โ (1...(โฏโ๐ด)){๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} = {๐ โ ๐ซ ๐ด โฃ โ๐ โ (1...(โฏโ๐ด))(โฏโ๐) = ๐} |
31 | 28, 29, 30 | 3eqtr4g 2802 |
. . . 4
โข ((๐ด โ Fin โง ๐ด โ Fin) โ (๐ซ
๐ด โ {โ
}) =
โช ๐ โ (1...(โฏโ๐ด)){๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) |
32 | 31 | sumeq1d 15593 |
. . 3
โข ((๐ด โ Fin โง ๐ด โ Fin) โ
ฮฃ๐ โ (๐ซ
๐ด โ
{โ
})((-1โ((โฏโ๐ ) โ 1)) ยท (โฏโโฉ ๐ ))
= ฮฃ๐ โ โช ๐ โ (1...(โฏโ๐ด)){๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} ((-1โ((โฏโ๐ ) โ 1)) ยท
(โฏโโฉ ๐ ))) |
33 | 1, 32 | eqtrd 2777 |
. 2
โข ((๐ด โ Fin โง ๐ด โ Fin) โ
(โฏโโช ๐ด) = ฮฃ๐ โ โช
๐ โ
(1...(โฏโ๐ด)){๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} ((-1โ((โฏโ๐ ) โ 1)) ยท
(โฏโโฉ ๐ ))) |
34 | | fzfid 13885 |
. . 3
โข ((๐ด โ Fin โง ๐ด โ Fin) โ
(1...(โฏโ๐ด))
โ Fin) |
35 | | simpll 766 |
. . . . 5
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โ ๐ด โ
Fin) |
36 | | pwfi 9129 |
. . . . 5
โข (๐ด โ Fin โ ๐ซ
๐ด โ
Fin) |
37 | 35, 36 | sylib 217 |
. . . 4
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โ ๐ซ ๐ด โ
Fin) |
38 | | ssrab2 4042 |
. . . 4
โข {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} โ ๐ซ ๐ด |
39 | | ssfi 9124 |
. . . 4
โข
((๐ซ ๐ด โ
Fin โง {๐ โ
๐ซ ๐ด โฃ
(โฏโ๐) = ๐} โ ๐ซ ๐ด) โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} โ Fin) |
40 | 37, 38, 39 | sylancl 587 |
. . 3
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โ {๐ โ ๐ซ
๐ด โฃ
(โฏโ๐) = ๐} โ Fin) |
41 | | fveqeq2 6856 |
. . . . . . . . 9
โข (๐ = ๐ โ ((โฏโ๐) = ๐ โ (โฏโ๐ ) = ๐)) |
42 | 41 | elrab 3650 |
. . . . . . . 8
โข (๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} โ (๐ โ ๐ซ ๐ด โง (โฏโ๐ ) = ๐)) |
43 | 42 | simprbi 498 |
. . . . . . 7
โข (๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} โ (โฏโ๐ ) = ๐) |
44 | 43 | adantl 483 |
. . . . . 6
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ (โฏโ๐ ) = ๐) |
45 | 44 | ralrimiva 3144 |
. . . . 5
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โ โ๐ โ
{๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} (โฏโ๐ ) = ๐) |
46 | 45 | ralrimiva 3144 |
. . . 4
โข ((๐ด โ Fin โง ๐ด โ Fin) โ
โ๐ โ
(1...(โฏโ๐ด))โ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} (โฏโ๐ ) = ๐) |
47 | | invdisj 5094 |
. . . 4
โข
(โ๐ โ
(1...(โฏโ๐ด))โ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} (โฏโ๐ ) = ๐ โ Disj ๐ โ (1...(โฏโ๐ด)){๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) |
48 | 46, 47 | syl 17 |
. . 3
โข ((๐ด โ Fin โง ๐ด โ Fin) โ Disj
๐ โ
(1...(โฏโ๐ด)){๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) |
49 | 44 | oveq1d 7377 |
. . . . . . 7
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ ((โฏโ๐ ) โ 1) = (๐ โ 1)) |
50 | 49 | oveq2d 7378 |
. . . . . 6
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ (-1โ((โฏโ๐ ) โ 1)) = (-1โ(๐ โ 1))) |
51 | 50 | oveq1d 7377 |
. . . . 5
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ ((-1โ((โฏโ๐ ) โ 1)) ยท
(โฏโโฉ ๐ )) = ((-1โ(๐ โ 1)) ยท (โฏโโฉ ๐ ))) |
52 | | 1cnd 11157 |
. . . . . . . . 9
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โ 1 โ โ) |
53 | 52 | negcld 11506 |
. . . . . . . 8
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โ -1 โ โ) |
54 | | elfznn 13477 |
. . . . . . . . . 10
โข (๐ โ
(1...(โฏโ๐ด))
โ ๐ โ
โ) |
55 | 54 | adantl 483 |
. . . . . . . . 9
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โ ๐ โ
โ) |
56 | | nnm1nn0 12461 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
57 | 55, 56 | syl 17 |
. . . . . . . 8
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โ (๐ โ 1) โ
โ0) |
58 | 53, 57 | expcld 14058 |
. . . . . . 7
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โ (-1โ(๐ โ
1)) โ โ) |
59 | 58 | adantr 482 |
. . . . . 6
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ (-1โ(๐ โ 1)) โ โ) |
60 | | unifi 9292 |
. . . . . . . . . 10
โข ((๐ด โ Fin โง ๐ด โ Fin) โ โช ๐ด
โ Fin) |
61 | 60 | ad2antrr 725 |
. . . . . . . . 9
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ โช ๐ด โ Fin) |
62 | 55 | adantr 482 |
. . . . . . . . . . . . 13
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ ๐ โ โ) |
63 | 44, 62 | eqeltrd 2838 |
. . . . . . . . . . . 12
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ (โฏโ๐ ) โ โ) |
64 | 35 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ ๐ด โ Fin) |
65 | | elrabi 3644 |
. . . . . . . . . . . . . . . 16
โข (๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} โ ๐ โ ๐ซ ๐ด) |
66 | 65 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ ๐ โ ๐ซ ๐ด) |
67 | | elpwi 4572 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ซ ๐ด โ ๐ โ ๐ด) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ ๐ โ ๐ด) |
69 | 64, 68 | ssfid 9218 |
. . . . . . . . . . . . 13
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ ๐ โ Fin) |
70 | | hashnncl 14273 |
. . . . . . . . . . . . 13
โข (๐ โ Fin โ
((โฏโ๐ ) โ
โ โ ๐ โ
โ
)) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . 12
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ ((โฏโ๐ ) โ โ โ ๐ โ โ
)) |
72 | 63, 71 | mpbid 231 |
. . . . . . . . . . 11
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ ๐ โ โ
) |
73 | | intssuni 4936 |
. . . . . . . . . . 11
โข (๐ โ โ
โ โฉ ๐
โ โช ๐ ) |
74 | 72, 73 | syl 17 |
. . . . . . . . . 10
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ โฉ ๐ โ โช ๐ ) |
75 | 68 | unissd 4880 |
. . . . . . . . . 10
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ โช ๐ โ โช ๐ด) |
76 | 74, 75 | sstrd 3959 |
. . . . . . . . 9
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ โฉ ๐ โ โช ๐ด) |
77 | 61, 76 | ssfid 9218 |
. . . . . . . 8
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ โฉ ๐ โ Fin) |
78 | | hashcl 14263 |
. . . . . . . 8
โข (โฉ ๐
โ Fin โ (โฏโโฉ ๐ ) โ
โ0) |
79 | 77, 78 | syl 17 |
. . . . . . 7
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ (โฏโโฉ ๐ )
โ โ0) |
80 | 79 | nn0cnd 12482 |
. . . . . 6
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ (โฏโโฉ ๐ )
โ โ) |
81 | 59, 80 | mulcld 11182 |
. . . . 5
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ ((-1โ(๐ โ 1)) ยท (โฏโโฉ ๐ ))
โ โ) |
82 | 51, 81 | eqeltrd 2838 |
. . . 4
โข ((((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐}) โ ((-1โ((โฏโ๐ ) โ 1)) ยท
(โฏโโฉ ๐ )) โ โ) |
83 | 82 | anasss 468 |
. . 3
โข (((๐ด โ Fin โง ๐ด โ Fin) โง (๐ โ
(1...(โฏโ๐ด))
โง ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐})) โ ((-1โ((โฏโ๐ ) โ 1)) ยท
(โฏโโฉ ๐ )) โ โ) |
84 | 34, 40, 48, 83 | fsumiun 15713 |
. 2
โข ((๐ด โ Fin โง ๐ด โ Fin) โ
ฮฃ๐ โ โช ๐ โ (1...(โฏโ๐ด)){๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} ((-1โ((โฏโ๐ ) โ 1)) ยท
(โฏโโฉ ๐ )) = ฮฃ๐ โ (1...(โฏโ๐ด))ฮฃ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} ((-1โ((โฏโ๐ ) โ 1)) ยท
(โฏโโฉ ๐ ))) |
85 | 51 | sumeq2dv 15595 |
. . . 4
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โ ฮฃ๐ โ
{๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} ((-1โ((โฏโ๐ ) โ 1)) ยท
(โฏโโฉ ๐ )) = ฮฃ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} ((-1โ(๐ โ 1)) ยท (โฏโโฉ ๐ ))) |
86 | 40, 58, 80 | fsummulc2 15676 |
. . . 4
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โ ((-1โ(๐ โ
1)) ยท ฮฃ๐
โ {๐ โ ๐ซ
๐ด โฃ
(โฏโ๐) = ๐} (โฏโโฉ ๐ ))
= ฮฃ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} ((-1โ(๐ โ 1)) ยท (โฏโโฉ ๐ ))) |
87 | 85, 86 | eqtr4d 2780 |
. . 3
โข (((๐ด โ Fin โง ๐ด โ Fin) โง ๐ โ
(1...(โฏโ๐ด)))
โ ฮฃ๐ โ
{๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} ((-1โ((โฏโ๐ ) โ 1)) ยท
(โฏโโฉ ๐ )) = ((-1โ(๐ โ 1)) ยท ฮฃ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} (โฏโโฉ
๐ ))) |
88 | 87 | sumeq2dv 15595 |
. 2
โข ((๐ด โ Fin โง ๐ด โ Fin) โ
ฮฃ๐ โ
(1...(โฏโ๐ด))ฮฃ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} ((-1โ((โฏโ๐ ) โ 1)) ยท
(โฏโโฉ ๐ )) = ฮฃ๐ โ (1...(โฏโ๐ด))((-1โ(๐ โ 1)) ยท ฮฃ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} (โฏโโฉ
๐ ))) |
89 | 33, 84, 88 | 3eqtrd 2781 |
1
โข ((๐ด โ Fin โง ๐ด โ Fin) โ
(โฏโโช ๐ด) = ฮฃ๐ โ (1...(โฏโ๐ด))((-1โ(๐ โ 1)) ยท ฮฃ๐ โ {๐ โ ๐ซ ๐ด โฃ (โฏโ๐) = ๐} (โฏโโฉ
๐ ))) |