Metamath Proof Explorer

Theorem incexclem

Description: Lemma for incexc . (Contributed by Mario Carneiro, 7-Aug-2017)

Ref Expression
Assertion incexclem 
|- ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` B ) - ( # ` ( B i^i U. A ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( B i^i |^| s ) ) ) )

Proof

Step Hyp Ref Expression
1 unieq 
 |-  ( x = (/) -> U. x = U. (/) )
2 uni0 
 |-  U. (/) = (/)
3 1 2 eqtrdi 
 |-  ( x = (/) -> U. x = (/) )
4 3 ineq2d 
 |-  ( x = (/) -> ( b i^i U. x ) = ( b i^i (/) ) )
5 in0 
 |-  ( b i^i (/) ) = (/)
6 4 5 eqtrdi 
 |-  ( x = (/) -> ( b i^i U. x ) = (/) )
7 6 fveq2d 
 |-  ( x = (/) -> ( # ` ( b i^i U. x ) ) = ( # ` (/) ) )
8 hash0 
 |-  ( # ` (/) ) = 0
9 7 8 eqtrdi 
 |-  ( x = (/) -> ( # ` ( b i^i U. x ) ) = 0 )
10 9 oveq2d 
 |-  ( x = (/) -> ( ( # ` b ) - ( # ` ( b i^i U. x ) ) ) = ( ( # ` b ) - 0 ) )
11 pweq 
 |-  ( x = (/) -> ~P x = ~P (/) )
12 pw0 
 |-  ~P (/) = { (/) }
13 11 12 eqtrdi 
 |-  ( x = (/) -> ~P x = { (/) } )
14 13 sumeq1d 
 |-  ( x = (/) -> sum_ s e. ~P x ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) )
15 10 14 eqeq12d 
 |-  ( x = (/) -> ( ( ( # ` b ) - ( # ` ( b i^i U. x ) ) ) = sum_ s e. ~P x ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) <-> ( ( # ` b ) - 0 ) = sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) )
16 15 ralbidv 
 |-  ( x = (/) -> ( A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. x ) ) ) = sum_ s e. ~P x ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) <-> A. b e. Fin ( ( # ` b ) - 0 ) = sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) )
17 unieq 
 |-  ( x = y -> U. x = U. y )
18 17 ineq2d 
 |-  ( x = y -> ( b i^i U. x ) = ( b i^i U. y ) )
19 18 fveq2d 
 |-  ( x = y -> ( # ` ( b i^i U. x ) ) = ( # ` ( b i^i U. y ) ) )
20 19 oveq2d 
 |-  ( x = y -> ( ( # ` b ) - ( # ` ( b i^i U. x ) ) ) = ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) )
21 pweq 
 |-  ( x = y -> ~P x = ~P y )
22 21 sumeq1d 
 |-  ( x = y -> sum_ s e. ~P x ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) )
23 20 22 eqeq12d 
 |-  ( x = y -> ( ( ( # ` b ) - ( # ` ( b i^i U. x ) ) ) = sum_ s e. ~P x ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) <-> ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) )
24 23 ralbidv 
 |-  ( x = y -> ( A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. x ) ) ) = sum_ s e. ~P x ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) <-> A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) )
25 unieq 
 |-  ( x = ( y u. { z } ) -> U. x = U. ( y u. { z } ) )
26 uniun 
 |-  U. ( y u. { z } ) = ( U. y u. U. { z } )
27 unisnv 
 |-  U. { z } = z
28 27 uneq2i 
 |-  ( U. y u. U. { z } ) = ( U. y u. z )
29 26 28 eqtri 
 |-  U. ( y u. { z } ) = ( U. y u. z )
30 25 29 eqtrdi 
 |-  ( x = ( y u. { z } ) -> U. x = ( U. y u. z ) )
31 30 ineq2d 
 |-  ( x = ( y u. { z } ) -> ( b i^i U. x ) = ( b i^i ( U. y u. z ) ) )
32 31 fveq2d 
 |-  ( x = ( y u. { z } ) -> ( # ` ( b i^i U. x ) ) = ( # ` ( b i^i ( U. y u. z ) ) ) )
33 32 oveq2d 
 |-  ( x = ( y u. { z } ) -> ( ( # ` b ) - ( # ` ( b i^i U. x ) ) ) = ( ( # ` b ) - ( # ` ( b i^i ( U. y u. z ) ) ) ) )
34 pweq 
 |-  ( x = ( y u. { z } ) -> ~P x = ~P ( y u. { z } ) )
35 34 sumeq1d 
 |-  ( x = ( y u. { z } ) -> sum_ s e. ~P x ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) )
36 33 35 eqeq12d 
 |-  ( x = ( y u. { z } ) -> ( ( ( # ` b ) - ( # ` ( b i^i U. x ) ) ) = sum_ s e. ~P x ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) <-> ( ( # ` b ) - ( # ` ( b i^i ( U. y u. z ) ) ) ) = sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) )
37 36 ralbidv 
 |-  ( x = ( y u. { z } ) -> ( A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. x ) ) ) = sum_ s e. ~P x ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) <-> A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i ( U. y u. z ) ) ) ) = sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) )
38 unieq 
 |-  ( x = A -> U. x = U. A )
39 38 ineq2d 
 |-  ( x = A -> ( b i^i U. x ) = ( b i^i U. A ) )
40 39 fveq2d 
 |-  ( x = A -> ( # ` ( b i^i U. x ) ) = ( # ` ( b i^i U. A ) ) )
41 40 oveq2d 
 |-  ( x = A -> ( ( # ` b ) - ( # ` ( b i^i U. x ) ) ) = ( ( # ` b ) - ( # ` ( b i^i U. A ) ) ) )
42 pweq 
 |-  ( x = A -> ~P x = ~P A )
43 42 sumeq1d 
 |-  ( x = A -> sum_ s e. ~P x ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) )
44 41 43 eqeq12d 
 |-  ( x = A -> ( ( ( # ` b ) - ( # ` ( b i^i U. x ) ) ) = sum_ s e. ~P x ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) <-> ( ( # ` b ) - ( # ` ( b i^i U. A ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) )
45 44 ralbidv 
 |-  ( x = A -> ( A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. x ) ) ) = sum_ s e. ~P x ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) <-> A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. A ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) )
46 hashcl 
 |-  ( b e. Fin -> ( # ` b ) e. NN0 )
47 46 nn0cnd 
 |-  ( b e. Fin -> ( # ` b ) e. CC )
48 47 mullidd 
 |-  ( b e. Fin -> ( 1 x. ( # ` b ) ) = ( # ` b ) )
49 0ex 
 |-  (/) e. _V
50 48 47 eqeltrd 
 |-  ( b e. Fin -> ( 1 x. ( # ` b ) ) e. CC )
51 fveq2 
 |-  ( s = (/) -> ( # ` s ) = ( # ` (/) ) )
52 51 8 eqtrdi 
 |-  ( s = (/) -> ( # ` s ) = 0 )
53 52 oveq2d 
 |-  ( s = (/) -> ( -u 1 ^ ( # ` s ) ) = ( -u 1 ^ 0 ) )
54 neg1cn 
 |-  -u 1 e. CC
55 exp0 
 |-  ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 )
56 54 55 ax-mp 
 |-  ( -u 1 ^ 0 ) = 1
57 53 56 eqtrdi 
 |-  ( s = (/) -> ( -u 1 ^ ( # ` s ) ) = 1 )
58 rint0 
 |-  ( s = (/) -> ( b i^i |^| s ) = b )
59 58 fveq2d 
 |-  ( s = (/) -> ( # ` ( b i^i |^| s ) ) = ( # ` b ) )
60 57 59 oveq12d 
 |-  ( s = (/) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = ( 1 x. ( # ` b ) ) )
61 60 sumsn 
 |-  ( ( (/) e. _V /\ ( 1 x. ( # ` b ) ) e. CC ) -> sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = ( 1 x. ( # ` b ) ) )
62 49 50 61 sylancr 
 |-  ( b e. Fin -> sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = ( 1 x. ( # ` b ) ) )
63 47 subid1d 
 |-  ( b e. Fin -> ( ( # ` b ) - 0 ) = ( # ` b ) )
64 48 62 63 3eqtr4rd 
 |-  ( b e. Fin -> ( ( # ` b ) - 0 ) = sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) )
65 64 rgen 
 |-  A. b e. Fin ( ( # ` b ) - 0 ) = sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) )
66 fveq2 
 |-  ( b = x -> ( # ` b ) = ( # ` x ) )
67 ineq1 
 |-  ( b = x -> ( b i^i U. y ) = ( x i^i U. y ) )
68 67 fveq2d 
 |-  ( b = x -> ( # ` ( b i^i U. y ) ) = ( # ` ( x i^i U. y ) ) )
69 66 68 oveq12d 
 |-  ( b = x -> ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = ( ( # ` x ) - ( # ` ( x i^i U. y ) ) ) )
70 simpl 
 |-  ( ( b = x /\ s e. ~P y ) -> b = x )
71 70 ineq1d 
 |-  ( ( b = x /\ s e. ~P y ) -> ( b i^i |^| s ) = ( x i^i |^| s ) )
72 71 fveq2d 
 |-  ( ( b = x /\ s e. ~P y ) -> ( # ` ( b i^i |^| s ) ) = ( # ` ( x i^i |^| s ) ) )
73 72 oveq2d 
 |-  ( ( b = x /\ s e. ~P y ) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) )
74 73 sumeq2dv 
 |-  ( b = x -> sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) )
75 69 74 eqeq12d 
 |-  ( b = x -> ( ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) <-> ( ( # ` x ) - ( # ` ( x i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) ) )
76 75 rspcva 
 |-  ( ( x e. Fin /\ A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) -> ( ( # ` x ) - ( # ` ( x i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) )
77 76 adantll 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) -> ( ( # ` x ) - ( # ` ( x i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) )
78 simpr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> x e. Fin )
79 inss1 
 |-  ( x i^i z ) C_ x
80 ssfi 
 |-  ( ( x e. Fin /\ ( x i^i z ) C_ x ) -> ( x i^i z ) e. Fin )
81 78 79 80 sylancl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( x i^i z ) e. Fin )
82 fveq2 
 |-  ( b = ( x i^i z ) -> ( # ` b ) = ( # ` ( x i^i z ) ) )
83 ineq1 
 |-  ( b = ( x i^i z ) -> ( b i^i U. y ) = ( ( x i^i z ) i^i U. y ) )
84 in32 
 |-  ( ( x i^i z ) i^i U. y ) = ( ( x i^i U. y ) i^i z )
85 inass 
 |-  ( ( x i^i U. y ) i^i z ) = ( x i^i ( U. y i^i z ) )
86 84 85 eqtri 
 |-  ( ( x i^i z ) i^i U. y ) = ( x i^i ( U. y i^i z ) )
87 83 86 eqtrdi 
 |-  ( b = ( x i^i z ) -> ( b i^i U. y ) = ( x i^i ( U. y i^i z ) ) )
88 87 fveq2d 
 |-  ( b = ( x i^i z ) -> ( # ` ( b i^i U. y ) ) = ( # ` ( x i^i ( U. y i^i z ) ) ) )
89 82 88 oveq12d 
 |-  ( b = ( x i^i z ) -> ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = ( ( # ` ( x i^i z ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) )
90 ineq1 
 |-  ( b = ( x i^i z ) -> ( b i^i |^| s ) = ( ( x i^i z ) i^i |^| s ) )
91 in32 
 |-  ( ( x i^i z ) i^i |^| s ) = ( ( x i^i |^| s ) i^i z )
92 inass 
 |-  ( ( x i^i |^| s ) i^i z ) = ( x i^i ( |^| s i^i z ) )
93 91 92 eqtri 
 |-  ( ( x i^i z ) i^i |^| s ) = ( x i^i ( |^| s i^i z ) )
94 90 93 eqtrdi 
 |-  ( b = ( x i^i z ) -> ( b i^i |^| s ) = ( x i^i ( |^| s i^i z ) ) )
95 94 fveq2d 
 |-  ( b = ( x i^i z ) -> ( # ` ( b i^i |^| s ) ) = ( # ` ( x i^i ( |^| s i^i z ) ) ) )
96 95 oveq2d 
 |-  ( b = ( x i^i z ) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) )
97 96 sumeq2sdv 
 |-  ( b = ( x i^i z ) -> sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) )
98 89 97 eqeq12d 
 |-  ( b = ( x i^i z ) -> ( ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) <-> ( ( # ` ( x i^i z ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) ) )
99 98 rspcva 
 |-  ( ( ( x i^i z ) e. Fin /\ A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) -> ( ( # ` ( x i^i z ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) )
100 81 99 sylan 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) -> ( ( # ` ( x i^i z ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) )
101 77 100 oveq12d 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) -> ( ( ( # ` x ) - ( # ` ( x i^i U. y ) ) ) - ( ( # ` ( x i^i z ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) ) = ( sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) - sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) ) )
102 inss1 
 |-  ( x i^i U. y ) C_ x
103 ssfi 
 |-  ( ( x e. Fin /\ ( x i^i U. y ) C_ x ) -> ( x i^i U. y ) e. Fin )
104 78 102 103 sylancl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( x i^i U. y ) e. Fin )
105 hashcl 
 |-  ( ( x i^i U. y ) e. Fin -> ( # ` ( x i^i U. y ) ) e. NN0 )
106 104 105 syl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( x i^i U. y ) ) e. NN0 )
107 106 nn0cnd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( x i^i U. y ) ) e. CC )
108 hashcl 
 |-  ( ( x i^i z ) e. Fin -> ( # ` ( x i^i z ) ) e. NN0 )
109 81 108 syl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( x i^i z ) ) e. NN0 )
110 109 nn0cnd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( x i^i z ) ) e. CC )
111 inss1 
 |-  ( x i^i ( U. y i^i z ) ) C_ x
112 ssfi 
 |-  ( ( x e. Fin /\ ( x i^i ( U. y i^i z ) ) C_ x ) -> ( x i^i ( U. y i^i z ) ) e. Fin )
113 78 111 112 sylancl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( x i^i ( U. y i^i z ) ) e. Fin )
114 hashcl 
 |-  ( ( x i^i ( U. y i^i z ) ) e. Fin -> ( # ` ( x i^i ( U. y i^i z ) ) ) e. NN0 )
115 113 114 syl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( x i^i ( U. y i^i z ) ) ) e. NN0 )
116 115 nn0cnd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( x i^i ( U. y i^i z ) ) ) e. CC )
117 hashun3 
 |-  ( ( ( x i^i U. y ) e. Fin /\ ( x i^i z ) e. Fin ) -> ( # ` ( ( x i^i U. y ) u. ( x i^i z ) ) ) = ( ( ( # ` ( x i^i U. y ) ) + ( # ` ( x i^i z ) ) ) - ( # ` ( ( x i^i U. y ) i^i ( x i^i z ) ) ) ) )
118 104 81 117 syl2anc 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( ( x i^i U. y ) u. ( x i^i z ) ) ) = ( ( ( # ` ( x i^i U. y ) ) + ( # ` ( x i^i z ) ) ) - ( # ` ( ( x i^i U. y ) i^i ( x i^i z ) ) ) ) )
119 indi 
 |-  ( x i^i ( U. y u. z ) ) = ( ( x i^i U. y ) u. ( x i^i z ) )
120 119 fveq2i 
 |-  ( # ` ( x i^i ( U. y u. z ) ) ) = ( # ` ( ( x i^i U. y ) u. ( x i^i z ) ) )
121 inindi 
 |-  ( x i^i ( U. y i^i z ) ) = ( ( x i^i U. y ) i^i ( x i^i z ) )
122 121 fveq2i 
 |-  ( # ` ( x i^i ( U. y i^i z ) ) ) = ( # ` ( ( x i^i U. y ) i^i ( x i^i z ) ) )
123 122 oveq2i 
 |-  ( ( ( # ` ( x i^i U. y ) ) + ( # ` ( x i^i z ) ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) = ( ( ( # ` ( x i^i U. y ) ) + ( # ` ( x i^i z ) ) ) - ( # ` ( ( x i^i U. y ) i^i ( x i^i z ) ) ) )
124 118 120 123 3eqtr4g 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( x i^i ( U. y u. z ) ) ) = ( ( ( # ` ( x i^i U. y ) ) + ( # ` ( x i^i z ) ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) )
125 107 110 116 124 assraddsubd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( x i^i ( U. y u. z ) ) ) = ( ( # ` ( x i^i U. y ) ) + ( ( # ` ( x i^i z ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) ) )
126 125 oveq2d 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( ( # ` x ) - ( # ` ( x i^i ( U. y u. z ) ) ) ) = ( ( # ` x ) - ( ( # ` ( x i^i U. y ) ) + ( ( # ` ( x i^i z ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) ) ) )
127 hashcl 
 |-  ( x e. Fin -> ( # ` x ) e. NN0 )
128 127 adantl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` x ) e. NN0 )
129 128 nn0cnd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` x ) e. CC )
130 110 116 subcld 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( ( # ` ( x i^i z ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) e. CC )
131 129 107 130 subsub4d 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( ( ( # ` x ) - ( # ` ( x i^i U. y ) ) ) - ( ( # ` ( x i^i z ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) ) = ( ( # ` x ) - ( ( # ` ( x i^i U. y ) ) + ( ( # ` ( x i^i z ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) ) ) )
132 126 131 eqtr4d 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( ( # ` x ) - ( # ` ( x i^i ( U. y u. z ) ) ) ) = ( ( ( # ` x ) - ( # ` ( x i^i U. y ) ) ) - ( ( # ` ( x i^i z ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) ) )
133 132 adantr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) -> ( ( # ` x ) - ( # ` ( x i^i ( U. y u. z ) ) ) ) = ( ( ( # ` x ) - ( # ` ( x i^i U. y ) ) ) - ( ( # ` ( x i^i z ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) ) )
134 disjdif 
 |-  ( ~P y i^i ( ~P ( y u. { z } ) \ ~P y ) ) = (/)
135 134 a1i 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( ~P y i^i ( ~P ( y u. { z } ) \ ~P y ) ) = (/) )
136 ssun1 
 |-  y C_ ( y u. { z } )
137 136 sspwi 
 |-  ~P y C_ ~P ( y u. { z } )
138 undif 
 |-  ( ~P y C_ ~P ( y u. { z } ) <-> ( ~P y u. ( ~P ( y u. { z } ) \ ~P y ) ) = ~P ( y u. { z } ) )
139 137 138 mpbi 
 |-  ( ~P y u. ( ~P ( y u. { z } ) \ ~P y ) ) = ~P ( y u. { z } )
140 139 eqcomi 
 |-  ~P ( y u. { z } ) = ( ~P y u. ( ~P ( y u. { z } ) \ ~P y ) )
141 140 a1i 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ~P ( y u. { z } ) = ( ~P y u. ( ~P ( y u. { z } ) \ ~P y ) ) )
142 simpll 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> y e. Fin )
143 snfi 
 |-  { z } e. Fin
144 unfi 
 |-  ( ( y e. Fin /\ { z } e. Fin ) -> ( y u. { z } ) e. Fin )
145 142 143 144 sylancl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( y u. { z } ) e. Fin )
146 pwfi 
 |-  ( ( y u. { z } ) e. Fin <-> ~P ( y u. { z } ) e. Fin )
147 145 146 sylib 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ~P ( y u. { z } ) e. Fin )
148 54 a1i 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> -u 1 e. CC )
149 elpwi 
 |-  ( s e. ~P ( y u. { z } ) -> s C_ ( y u. { z } ) )
150 ssfi 
 |-  ( ( ( y u. { z } ) e. Fin /\ s C_ ( y u. { z } ) ) -> s e. Fin )
151 145 149 150 syl2an 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> s e. Fin )
152 hashcl 
 |-  ( s e. Fin -> ( # ` s ) e. NN0 )
153 151 152 syl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( # ` s ) e. NN0 )
154 148 153 expcld 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( -u 1 ^ ( # ` s ) ) e. CC )
155 simplr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> x e. Fin )
156 inss1 
 |-  ( x i^i |^| s ) C_ x
157 ssfi 
 |-  ( ( x e. Fin /\ ( x i^i |^| s ) C_ x ) -> ( x i^i |^| s ) e. Fin )
158 155 156 157 sylancl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( x i^i |^| s ) e. Fin )
159 hashcl 
 |-  ( ( x i^i |^| s ) e. Fin -> ( # ` ( x i^i |^| s ) ) e. NN0 )
160 158 159 syl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( # ` ( x i^i |^| s ) ) e. NN0 )
161 160 nn0cnd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( # ` ( x i^i |^| s ) ) e. CC )
162 154 161 mulcld 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) e. CC )
163 135 141 147 162 fsumsplit 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) = ( sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) + sum_ s e. ( ~P ( y u. { z } ) \ ~P y ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) ) )
164 fveq2 
 |-  ( s = ( t u. { z } ) -> ( # ` s ) = ( # ` ( t u. { z } ) ) )
165 164 oveq2d 
 |-  ( s = ( t u. { z } ) -> ( -u 1 ^ ( # ` s ) ) = ( -u 1 ^ ( # ` ( t u. { z } ) ) ) )
166 inteq 
 |-  ( s = ( t u. { z } ) -> |^| s = |^| ( t u. { z } ) )
167 vex 
 |-  z e. _V
168 167 intunsn 
 |-  |^| ( t u. { z } ) = ( |^| t i^i z )
169 166 168 eqtrdi 
 |-  ( s = ( t u. { z } ) -> |^| s = ( |^| t i^i z ) )
170 169 ineq2d 
 |-  ( s = ( t u. { z } ) -> ( x i^i |^| s ) = ( x i^i ( |^| t i^i z ) ) )
171 170 fveq2d 
 |-  ( s = ( t u. { z } ) -> ( # ` ( x i^i |^| s ) ) = ( # ` ( x i^i ( |^| t i^i z ) ) ) )
172 165 171 oveq12d 
 |-  ( s = ( t u. { z } ) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) = ( ( -u 1 ^ ( # ` ( t u. { z } ) ) ) x. ( # ` ( x i^i ( |^| t i^i z ) ) ) ) )
173 pwfi 
 |-  ( y e. Fin <-> ~P y e. Fin )
174 142 173 sylib 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ~P y e. Fin )
175 eqid 
 |-  ( u e. ~P y |-> ( u u. { z } ) ) = ( u e. ~P y |-> ( u u. { z } ) )
176 elpwi 
 |-  ( u e. ~P y -> u C_ y )
177 176 adantl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ u e. ~P y ) -> u C_ y )
178 unss1 
 |-  ( u C_ y -> ( u u. { z } ) C_ ( y u. { z } ) )
179 177 178 syl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ u e. ~P y ) -> ( u u. { z } ) C_ ( y u. { z } ) )
180 vex 
 |-  u e. _V
181 vsnex 
 |-  { z } e. _V
182 180 181 unex 
 |-  ( u u. { z } ) e. _V
183 182 elpw 
 |-  ( ( u u. { z } ) e. ~P ( y u. { z } ) <-> ( u u. { z } ) C_ ( y u. { z } ) )
184 179 183 sylibr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ u e. ~P y ) -> ( u u. { z } ) e. ~P ( y u. { z } ) )
185 simpllr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ u e. ~P y ) -> -. z e. y )
186 elpwi 
 |-  ( ( u u. { z } ) e. ~P y -> ( u u. { z } ) C_ y )
187 ssun2 
 |-  { z } C_ ( u u. { z } )
188 167 snss 
 |-  ( z e. ( u u. { z } ) <-> { z } C_ ( u u. { z } ) )
189 187 188 mpbir 
 |-  z e. ( u u. { z } )
190 189 a1i 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ u e. ~P y ) -> z e. ( u u. { z } ) )
191 ssel 
 |-  ( ( u u. { z } ) C_ y -> ( z e. ( u u. { z } ) -> z e. y ) )
192 186 190 191 syl2imc 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ u e. ~P y ) -> ( ( u u. { z } ) e. ~P y -> z e. y ) )
193 185 192 mtod 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ u e. ~P y ) -> -. ( u u. { z } ) e. ~P y )
194 184 193 eldifd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ u e. ~P y ) -> ( u u. { z } ) e. ( ~P ( y u. { z } ) \ ~P y ) )
195 eldifi 
 |-  ( s e. ( ~P ( y u. { z } ) \ ~P y ) -> s e. ~P ( y u. { z } ) )
196 195 adantl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) -> s e. ~P ( y u. { z } ) )
197 196 elpwid 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) -> s C_ ( y u. { z } ) )
198 uncom 
 |-  ( y u. { z } ) = ( { z } u. y )
199 197 198 sseqtrdi 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) -> s C_ ( { z } u. y ) )
200 ssundif 
 |-  ( s C_ ( { z } u. y ) <-> ( s \ { z } ) C_ y )
201 199 200 sylib 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) -> ( s \ { z } ) C_ y )
202 vex 
 |-  y e. _V
203 202 elpw2 
 |-  ( ( s \ { z } ) e. ~P y <-> ( s \ { z } ) C_ y )
204 201 203 sylibr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) -> ( s \ { z } ) e. ~P y )
205 elpwunsn 
 |-  ( s e. ( ~P ( y u. { z } ) \ ~P y ) -> z e. s )
206 205 ad2antll 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ ( u e. ~P y /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) ) -> z e. s )
207 206 snssd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ ( u e. ~P y /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) ) -> { z } C_ s )
208 ssequn2 
 |-  ( { z } C_ s <-> ( s u. { z } ) = s )
209 207 208 sylib 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ ( u e. ~P y /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) ) -> ( s u. { z } ) = s )
210 209 eqcomd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ ( u e. ~P y /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) ) -> s = ( s u. { z } ) )
211 uneq1 
 |-  ( u = ( s \ { z } ) -> ( u u. { z } ) = ( ( s \ { z } ) u. { z } ) )
212 undif1 
 |-  ( ( s \ { z } ) u. { z } ) = ( s u. { z } )
213 211 212 eqtrdi 
 |-  ( u = ( s \ { z } ) -> ( u u. { z } ) = ( s u. { z } ) )
214 213 eqeq2d 
 |-  ( u = ( s \ { z } ) -> ( s = ( u u. { z } ) <-> s = ( s u. { z } ) ) )
215 210 214 syl5ibrcom 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ ( u e. ~P y /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) ) -> ( u = ( s \ { z } ) -> s = ( u u. { z } ) ) )
216 176 ad2antrl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ ( u e. ~P y /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) ) -> u C_ y )
217 simpllr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ ( u e. ~P y /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) ) -> -. z e. y )
218 216 217 ssneldd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ ( u e. ~P y /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) ) -> -. z e. u )
219 difsnb 
 |-  ( -. z e. u <-> ( u \ { z } ) = u )
220 218 219 sylib 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ ( u e. ~P y /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) ) -> ( u \ { z } ) = u )
221 220 eqcomd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ ( u e. ~P y /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) ) -> u = ( u \ { z } ) )
222 difeq1 
 |-  ( s = ( u u. { z } ) -> ( s \ { z } ) = ( ( u u. { z } ) \ { z } ) )
223 difun2 
 |-  ( ( u u. { z } ) \ { z } ) = ( u \ { z } )
224 222 223 eqtrdi 
 |-  ( s = ( u u. { z } ) -> ( s \ { z } ) = ( u \ { z } ) )
225 224 eqeq2d 
 |-  ( s = ( u u. { z } ) -> ( u = ( s \ { z } ) <-> u = ( u \ { z } ) ) )
226 221 225 syl5ibrcom 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ ( u e. ~P y /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) ) -> ( s = ( u u. { z } ) -> u = ( s \ { z } ) ) )
227 215 226 impbid 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ ( u e. ~P y /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) ) -> ( u = ( s \ { z } ) <-> s = ( u u. { z } ) ) )
228 175 194 204 227 f1o2d 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( u e. ~P y |-> ( u u. { z } ) ) : ~P y -1-1-onto-> ( ~P ( y u. { z } ) \ ~P y ) )
229 uneq1 
 |-  ( u = t -> ( u u. { z } ) = ( t u. { z } ) )
230 vex 
 |-  t e. _V
231 230 181 unex 
 |-  ( t u. { z } ) e. _V
232 229 175 231 fvmpt 
 |-  ( t e. ~P y -> ( ( u e. ~P y |-> ( u u. { z } ) ) ` t ) = ( t u. { z } ) )
233 232 adantl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ t e. ~P y ) -> ( ( u e. ~P y |-> ( u u. { z } ) ) ` t ) = ( t u. { z } ) )
234 195 162 sylan2 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ( ~P ( y u. { z } ) \ ~P y ) ) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) e. CC )
235 172 174 228 233 234 fsumf1o 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> sum_ s e. ( ~P ( y u. { z } ) \ ~P y ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) = sum_ t e. ~P y ( ( -u 1 ^ ( # ` ( t u. { z } ) ) ) x. ( # ` ( x i^i ( |^| t i^i z ) ) ) ) )
236 uneq1 
 |-  ( t = s -> ( t u. { z } ) = ( s u. { z } ) )
237 236 fveq2d 
 |-  ( t = s -> ( # ` ( t u. { z } ) ) = ( # ` ( s u. { z } ) ) )
238 237 oveq2d 
 |-  ( t = s -> ( -u 1 ^ ( # ` ( t u. { z } ) ) ) = ( -u 1 ^ ( # ` ( s u. { z } ) ) ) )
239 inteq 
 |-  ( t = s -> |^| t = |^| s )
240 239 ineq1d 
 |-  ( t = s -> ( |^| t i^i z ) = ( |^| s i^i z ) )
241 240 ineq2d 
 |-  ( t = s -> ( x i^i ( |^| t i^i z ) ) = ( x i^i ( |^| s i^i z ) ) )
242 241 fveq2d 
 |-  ( t = s -> ( # ` ( x i^i ( |^| t i^i z ) ) ) = ( # ` ( x i^i ( |^| s i^i z ) ) ) )
243 238 242 oveq12d 
 |-  ( t = s -> ( ( -u 1 ^ ( # ` ( t u. { z } ) ) ) x. ( # ` ( x i^i ( |^| t i^i z ) ) ) ) = ( ( -u 1 ^ ( # ` ( s u. { z } ) ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) )
244 243 cbvsumv 
 |-  sum_ t e. ~P y ( ( -u 1 ^ ( # ` ( t u. { z } ) ) ) x. ( # ` ( x i^i ( |^| t i^i z ) ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` ( s u. { z } ) ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) )
245 54 a1i 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> -u 1 e. CC )
246 elpwi 
 |-  ( s e. ~P y -> s C_ y )
247 ssfi 
 |-  ( ( y e. Fin /\ s C_ y ) -> s e. Fin )
248 142 246 247 syl2an 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> s e. Fin )
249 248 152 syl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( # ` s ) e. NN0 )
250 245 249 expp1d 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( -u 1 ^ ( ( # ` s ) + 1 ) ) = ( ( -u 1 ^ ( # ` s ) ) x. -u 1 ) )
251 246 adantl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> s C_ y )
252 simpllr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> -. z e. y )
253 251 252 ssneldd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> -. z e. s )
254 hashunsng 
 |-  ( z e. _V -> ( ( s e. Fin /\ -. z e. s ) -> ( # ` ( s u. { z } ) ) = ( ( # ` s ) + 1 ) ) )
255 254 elv 
 |-  ( ( s e. Fin /\ -. z e. s ) -> ( # ` ( s u. { z } ) ) = ( ( # ` s ) + 1 ) )
256 248 253 255 syl2anc 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( # ` ( s u. { z } ) ) = ( ( # ` s ) + 1 ) )
257 256 oveq2d 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( -u 1 ^ ( # ` ( s u. { z } ) ) ) = ( -u 1 ^ ( ( # ` s ) + 1 ) ) )
258 137 sseli 
 |-  ( s e. ~P y -> s e. ~P ( y u. { z } ) )
259 258 154 sylan2 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( -u 1 ^ ( # ` s ) ) e. CC )
260 245 259 mulcomd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( -u 1 x. ( -u 1 ^ ( # ` s ) ) ) = ( ( -u 1 ^ ( # ` s ) ) x. -u 1 ) )
261 250 257 260 3eqtr4d 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( -u 1 ^ ( # ` ( s u. { z } ) ) ) = ( -u 1 x. ( -u 1 ^ ( # ` s ) ) ) )
262 259 mulm1d 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( -u 1 x. ( -u 1 ^ ( # ` s ) ) ) = -u ( -u 1 ^ ( # ` s ) ) )
263 261 262 eqtrd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( -u 1 ^ ( # ` ( s u. { z } ) ) ) = -u ( -u 1 ^ ( # ` s ) ) )
264 263 oveq1d 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( ( -u 1 ^ ( # ` ( s u. { z } ) ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) = ( -u ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) )
265 inss1 
 |-  ( x i^i ( |^| s i^i z ) ) C_ x
266 ssfi 
 |-  ( ( x e. Fin /\ ( x i^i ( |^| s i^i z ) ) C_ x ) -> ( x i^i ( |^| s i^i z ) ) e. Fin )
267 155 265 266 sylancl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( x i^i ( |^| s i^i z ) ) e. Fin )
268 hashcl 
 |-  ( ( x i^i ( |^| s i^i z ) ) e. Fin -> ( # ` ( x i^i ( |^| s i^i z ) ) ) e. NN0 )
269 267 268 syl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( # ` ( x i^i ( |^| s i^i z ) ) ) e. NN0 )
270 269 nn0cnd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( # ` ( x i^i ( |^| s i^i z ) ) ) e. CC )
271 258 270 sylan2 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( # ` ( x i^i ( |^| s i^i z ) ) ) e. CC )
272 259 271 mulneg1d 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( -u ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) = -u ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) )
273 264 272 eqtrd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( ( -u 1 ^ ( # ` ( s u. { z } ) ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) = -u ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) )
274 273 sumeq2dv 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> sum_ s e. ~P y ( ( -u 1 ^ ( # ` ( s u. { z } ) ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) = sum_ s e. ~P y -u ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) )
275 244 274 eqtrid 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> sum_ t e. ~P y ( ( -u 1 ^ ( # ` ( t u. { z } ) ) ) x. ( # ` ( x i^i ( |^| t i^i z ) ) ) ) = sum_ s e. ~P y -u ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) )
276 154 270 mulcld 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) e. CC )
277 258 276 sylan2 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) e. CC )
278 174 277 fsumneg 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> sum_ s e. ~P y -u ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) = -u sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) )
279 235 275 278 3eqtrd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> sum_ s e. ( ~P ( y u. { z } ) \ ~P y ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) = -u sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) )
280 279 oveq2d 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) + sum_ s e. ( ~P ( y u. { z } ) \ ~P y ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) ) = ( sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) + -u sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) ) )
281 137 a1i 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ~P y C_ ~P ( y u. { z } ) )
282 281 sselda 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> s e. ~P ( y u. { z } ) )
283 282 162 syldan 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) e. CC )
284 174 283 fsumcl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) e. CC )
285 282 276 syldan 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) e. CC )
286 174 285 fsumcl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) e. CC )
287 284 286 negsubd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) + -u sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) ) = ( sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) - sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) ) )
288 163 280 287 3eqtrd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) = ( sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) - sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) ) )
289 288 adantr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) -> sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) = ( sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) - sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i ( |^| s i^i z ) ) ) ) ) )
290 101 133 289 3eqtr4d 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) -> ( ( # ` x ) - ( # ` ( x i^i ( U. y u. z ) ) ) ) = sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) )
291 290 ex 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) -> ( ( # ` x ) - ( # ` ( x i^i ( U. y u. z ) ) ) ) = sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) ) )
292 291 ralrimdva 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) -> A. x e. Fin ( ( # ` x ) - ( # ` ( x i^i ( U. y u. z ) ) ) ) = sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) ) )
293 ineq1 
 |-  ( b = x -> ( b i^i ( U. y u. z ) ) = ( x i^i ( U. y u. z ) ) )
294 293 fveq2d 
 |-  ( b = x -> ( # ` ( b i^i ( U. y u. z ) ) ) = ( # ` ( x i^i ( U. y u. z ) ) ) )
295 66 294 oveq12d 
 |-  ( b = x -> ( ( # ` b ) - ( # ` ( b i^i ( U. y u. z ) ) ) ) = ( ( # ` x ) - ( # ` ( x i^i ( U. y u. z ) ) ) ) )
296 ineq1 
 |-  ( b = x -> ( b i^i |^| s ) = ( x i^i |^| s ) )
297 296 fveq2d 
 |-  ( b = x -> ( # ` ( b i^i |^| s ) ) = ( # ` ( x i^i |^| s ) ) )
298 297 oveq2d 
 |-  ( b = x -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) )
299 298 sumeq2sdv 
 |-  ( b = x -> sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) )
300 295 299 eqeq12d 
 |-  ( b = x -> ( ( ( # ` b ) - ( # ` ( b i^i ( U. y u. z ) ) ) ) = sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) <-> ( ( # ` x ) - ( # ` ( x i^i ( U. y u. z ) ) ) ) = sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) ) )
301 300 cbvralvw 
 |-  ( A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i ( U. y u. z ) ) ) ) = sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) <-> A. x e. Fin ( ( # ` x ) - ( # ` ( x i^i ( U. y u. z ) ) ) ) = sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) )
302 292 301 imbitrrdi 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = sum_ s e. ~P y ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) -> A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i ( U. y u. z ) ) ) ) = sum_ s e. ~P ( y u. { z } ) ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) ) )
303 16 24 37 45 65 302 findcard2s 
 |-  ( A e. Fin -> A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. A ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) )
304 fveq2 
 |-  ( b = B -> ( # ` b ) = ( # ` B ) )
305 ineq1 
 |-  ( b = B -> ( b i^i U. A ) = ( B i^i U. A ) )
306 305 fveq2d 
 |-  ( b = B -> ( # ` ( b i^i U. A ) ) = ( # ` ( B i^i U. A ) ) )
307 304 306 oveq12d 
 |-  ( b = B -> ( ( # ` b ) - ( # ` ( b i^i U. A ) ) ) = ( ( # ` B ) - ( # ` ( B i^i U. A ) ) ) )
308 simpl 
 |-  ( ( b = B /\ s e. ~P A ) -> b = B )
309 308 ineq1d 
 |-  ( ( b = B /\ s e. ~P A ) -> ( b i^i |^| s ) = ( B i^i |^| s ) )
310 309 fveq2d 
 |-  ( ( b = B /\ s e. ~P A ) -> ( # ` ( b i^i |^| s ) ) = ( # ` ( B i^i |^| s ) ) )
311 310 oveq2d 
 |-  ( ( b = B /\ s e. ~P A ) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( B i^i |^| s ) ) ) )
312 311 sumeq2dv 
 |-  ( b = B -> sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( B i^i |^| s ) ) ) )
313 307 312 eqeq12d 
 |-  ( b = B -> ( ( ( # ` b ) - ( # ` ( b i^i U. A ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) <-> ( ( # ` B ) - ( # ` ( B i^i U. A ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( B i^i |^| s ) ) ) ) )
314 313 rspccva 
 |-  ( ( A. b e. Fin ( ( # ` b ) - ( # ` ( b i^i U. A ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) /\ B e. Fin ) -> ( ( # ` B ) - ( # ` ( B i^i U. A ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( B i^i |^| s ) ) ) )
315 303 314 sylan 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` B ) - ( # ` ( B i^i U. A ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( B i^i |^| s ) ) ) )