Metamath Proof Explorer

Theorem incexc

Description: The inclusion/exclusion principle for counting the elements of a finite union of finite sets. This is Metamath 100 proof #96. (Contributed by Mario Carneiro, 7-Aug-2017)

Ref Expression
Assertion incexc 
|- ( ( A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) = sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) )

Proof

Step Hyp Ref Expression
1 unifi 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> U. A e. Fin )
2 hashcl 
 |-  ( U. A e. Fin -> ( # ` U. A ) e. NN0 )
3 2 nn0cnd 
 |-  ( U. A e. Fin -> ( # ` U. A ) e. CC )
4 1 3 syl 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) e. CC )
5 simpl 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> A e. Fin )
6 pwfi 
 |-  ( A e. Fin <-> ~P A e. Fin )
7 5 6 sylib 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ~P A e. Fin )
8 diffi 
 |-  ( ~P A e. Fin -> ( ~P A \ { (/) } ) e. Fin )
9 7 8 syl 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( ~P A \ { (/) } ) e. Fin )
10 1cnd 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> 1 e. CC )
11 10 negcld 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> -u 1 e. CC )
12 eldifsni 
 |-  ( s e. ( ~P A \ { (/) } ) -> s =/= (/) )
13 12 adantl 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> s =/= (/) )
14 eldifi 
 |-  ( s e. ( ~P A \ { (/) } ) -> s e. ~P A )
15 elpwi 
 |-  ( s e. ~P A -> s C_ A )
16 14 15 syl 
 |-  ( s e. ( ~P A \ { (/) } ) -> s C_ A )
17 ssfi 
 |-  ( ( A e. Fin /\ s C_ A ) -> s e. Fin )
18 5 16 17 syl2an 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> s e. Fin )
19 hashnncl 
 |-  ( s e. Fin -> ( ( # ` s ) e. NN <-> s =/= (/) ) )
20 18 19 syl 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( ( # ` s ) e. NN <-> s =/= (/) ) )
21 13 20 mpbird 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( # ` s ) e. NN )
22 nnm1nn0 
 |-  ( ( # ` s ) e. NN -> ( ( # ` s ) - 1 ) e. NN0 )
23 21 22 syl 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( ( # ` s ) - 1 ) e. NN0 )
24 11 23 expcld 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( -u 1 ^ ( ( # ` s ) - 1 ) ) e. CC )
25 16 adantl 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> s C_ A )
26 simplr 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> A C_ Fin )
27 25 26 sstrd 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> s C_ Fin )
28 unifi 
 |-  ( ( s e. Fin /\ s C_ Fin ) -> U. s e. Fin )
29 18 27 28 syl2anc 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> U. s e. Fin )
30 intssuni 
 |-  ( s =/= (/) -> |^| s C_ U. s )
31 13 30 syl 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> |^| s C_ U. s )
32 29 31 ssfid 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> |^| s e. Fin )
33 hashcl 
 |-  ( |^| s e. Fin -> ( # ` |^| s ) e. NN0 )
34 32 33 syl 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( # ` |^| s ) e. NN0 )
35 34 nn0cnd 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( # ` |^| s ) e. CC )
36 24 35 mulcld 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) e. CC )
37 9 36 fsumcl 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) e. CC )
38 disjdif 
 |-  ( { (/) } i^i ( ~P A \ { (/) } ) ) = (/)
39 38 a1i 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( { (/) } i^i ( ~P A \ { (/) } ) ) = (/) )
40 0elpw 
 |-  (/) e. ~P A
41 snssi 
 |-  ( (/) e. ~P A -> { (/) } C_ ~P A )
42 40 41 ax-mp 
 |-  { (/) } C_ ~P A
43 undif 
 |-  ( { (/) } C_ ~P A <-> ( { (/) } u. ( ~P A \ { (/) } ) ) = ~P A )
44 42 43 mpbi 
 |-  ( { (/) } u. ( ~P A \ { (/) } ) ) = ~P A
45 44 eqcomi 
 |-  ~P A = ( { (/) } u. ( ~P A \ { (/) } ) )
46 45 a1i 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ~P A = ( { (/) } u. ( ~P A \ { (/) } ) ) )
47 1cnd 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ~P A ) -> 1 e. CC )
48 47 negcld 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ~P A ) -> -u 1 e. CC )
49 5 15 17 syl2an 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ~P A ) -> s e. Fin )
50 hashcl 
 |-  ( s e. Fin -> ( # ` s ) e. NN0 )
51 49 50 syl 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ~P A ) -> ( # ` s ) e. NN0 )
52 48 51 expcld 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ~P A ) -> ( -u 1 ^ ( # ` s ) ) e. CC )
53 1 adantr 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ~P A ) -> U. A e. Fin )
54 inss1 
 |-  ( U. A i^i |^| s ) C_ U. A
55 ssfi 
 |-  ( ( U. A e. Fin /\ ( U. A i^i |^| s ) C_ U. A ) -> ( U. A i^i |^| s ) e. Fin )
56 53 54 55 sylancl 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ~P A ) -> ( U. A i^i |^| s ) e. Fin )
57 hashcl 
 |-  ( ( U. A i^i |^| s ) e. Fin -> ( # ` ( U. A i^i |^| s ) ) e. NN0 )
58 56 57 syl 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ~P A ) -> ( # ` ( U. A i^i |^| s ) ) e. NN0 )
59 58 nn0cnd 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ~P A ) -> ( # ` ( U. A i^i |^| s ) ) e. CC )
60 52 59 mulcld 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ~P A ) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) e. CC )
61 39 46 7 60 fsumsplit 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) = ( sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) + sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) ) )
62 inidm 
 |-  ( U. A i^i U. A ) = U. A
63 62 fveq2i 
 |-  ( # ` ( U. A i^i U. A ) ) = ( # ` U. A )
64 63 oveq2i 
 |-  ( ( # ` U. A ) - ( # ` ( U. A i^i U. A ) ) ) = ( ( # ` U. A ) - ( # ` U. A ) )
65 4 subidd 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( ( # ` U. A ) - ( # ` U. A ) ) = 0 )
66 64 65 eqtrid 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( ( # ` U. A ) - ( # ` ( U. A i^i U. A ) ) ) = 0 )
67 incexclem 
 |-  ( ( A e. Fin /\ U. A e. Fin ) -> ( ( # ` U. A ) - ( # ` ( U. A i^i U. A ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) )
68 1 67 syldan 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( ( # ` U. A ) - ( # ` ( U. A i^i U. A ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) )
69 66 68 eqtr3d 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> 0 = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) )
70 4 37 negsubd 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( ( # ` U. A ) + -u sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) ) = ( ( # ` U. A ) - sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) ) )
71 0ex 
 |-  (/) e. _V
72 1cnd 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> 1 e. CC )
73 72 4 mulcld 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( 1 x. ( # ` U. A ) ) e. CC )
74 fveq2 
 |-  ( s = (/) -> ( # ` s ) = ( # ` (/) ) )
75 hash0 
 |-  ( # ` (/) ) = 0
76 74 75 eqtrdi 
 |-  ( s = (/) -> ( # ` s ) = 0 )
77 76 oveq2d 
 |-  ( s = (/) -> ( -u 1 ^ ( # ` s ) ) = ( -u 1 ^ 0 ) )
78 neg1cn 
 |-  -u 1 e. CC
79 exp0 
 |-  ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 )
80 78 79 ax-mp 
 |-  ( -u 1 ^ 0 ) = 1
81 77 80 eqtrdi 
 |-  ( s = (/) -> ( -u 1 ^ ( # ` s ) ) = 1 )
82 rint0 
 |-  ( s = (/) -> ( U. A i^i |^| s ) = U. A )
83 82 fveq2d 
 |-  ( s = (/) -> ( # ` ( U. A i^i |^| s ) ) = ( # ` U. A ) )
84 81 83 oveq12d 
 |-  ( s = (/) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) = ( 1 x. ( # ` U. A ) ) )
85 84 sumsn 
 |-  ( ( (/) e. _V /\ ( 1 x. ( # ` U. A ) ) e. CC ) -> sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) = ( 1 x. ( # ` U. A ) ) )
86 71 73 85 sylancr 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) = ( 1 x. ( # ` U. A ) ) )
87 4 mullidd 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( 1 x. ( # ` U. A ) ) = ( # ` U. A ) )
88 86 87 eqtr2d 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) = sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) )
89 9 36 fsumneg 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> sum_ s e. ( ~P A \ { (/) } ) -u ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) = -u sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) )
90 expm1t 
 |-  ( ( -u 1 e. CC /\ ( # ` s ) e. NN ) -> ( -u 1 ^ ( # ` s ) ) = ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. -u 1 ) )
91 11 21 90 syl2anc 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( -u 1 ^ ( # ` s ) ) = ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. -u 1 ) )
92 24 11 mulcomd 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. -u 1 ) = ( -u 1 x. ( -u 1 ^ ( ( # ` s ) - 1 ) ) ) )
93 24 mulm1d 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( -u 1 x. ( -u 1 ^ ( ( # ` s ) - 1 ) ) ) = -u ( -u 1 ^ ( ( # ` s ) - 1 ) ) )
94 91 92 93 3eqtrd 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( -u 1 ^ ( # ` s ) ) = -u ( -u 1 ^ ( ( # ` s ) - 1 ) ) )
95 25 unissd 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> U. s C_ U. A )
96 31 95 sstrd 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> |^| s C_ U. A )
97 sseqin2 
 |-  ( |^| s C_ U. A <-> ( U. A i^i |^| s ) = |^| s )
98 96 97 sylib 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( U. A i^i |^| s ) = |^| s )
99 98 fveq2d 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( # ` ( U. A i^i |^| s ) ) = ( # ` |^| s ) )
100 94 99 oveq12d 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) = ( -u ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) )
101 24 35 mulneg1d 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> ( -u ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) = -u ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) )
102 100 101 eqtr2d 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ s e. ( ~P A \ { (/) } ) ) -> -u ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) = ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) )
103 102 sumeq2dv 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> sum_ s e. ( ~P A \ { (/) } ) -u ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) = sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) )
104 89 103 eqtr3d 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> -u sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) = sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) )
105 88 104 oveq12d 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( ( # ` U. A ) + -u sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) ) = ( sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) + sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) ) )
106 70 105 eqtr3d 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( ( # ` U. A ) - sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) ) = ( sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) + sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( U. A i^i |^| s ) ) ) ) )
107 61 69 106 3eqtr4rd 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( ( # ` U. A ) - sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) ) = 0 )
108 4 37 107 subeq0d 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) = sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) )