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 vex 
 |-  z e. _V
28 27 unisn 
 |-  U. { z } = z
29 28 uneq2i 
 |-  ( U. y u. U. { z } ) = ( U. y u. z )
30 26 29 eqtri 
 |-  U. ( y u. { z } ) = ( U. y u. z )
31 25 30 eqtrdi 
 |-  ( x = ( y u. { z } ) -> U. x = ( U. y u. z ) )
32 31 ineq2d 
 |-  ( x = ( y u. { z } ) -> ( b i^i U. x ) = ( b i^i ( U. y u. z ) ) )
33 32 fveq2d 
 |-  ( x = ( y u. { z } ) -> ( # ` ( b i^i U. x ) ) = ( # ` ( b i^i ( U. y u. z ) ) ) )
34 33 oveq2d 
 |-  ( x = ( y u. { z } ) -> ( ( # ` b ) - ( # ` ( b i^i U. x ) ) ) = ( ( # ` b ) - ( # ` ( b i^i ( U. y u. z ) ) ) ) )
35 pweq 
 |-  ( x = ( y u. { z } ) -> ~P x = ~P ( y u. { z } ) )
36 35 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 ) ) ) )
37 34 36 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 ) ) ) ) )
38 37 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 ) ) ) ) )
39 unieq 
 |-  ( x = A -> U. x = U. A )
40 39 ineq2d 
 |-  ( x = A -> ( b i^i U. x ) = ( b i^i U. A ) )
41 40 fveq2d 
 |-  ( x = A -> ( # ` ( b i^i U. x ) ) = ( # ` ( b i^i U. A ) ) )
42 41 oveq2d 
 |-  ( x = A -> ( ( # ` b ) - ( # ` ( b i^i U. x ) ) ) = ( ( # ` b ) - ( # ` ( b i^i U. A ) ) ) )
43 pweq 
 |-  ( x = A -> ~P x = ~P A )
44 43 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 ) ) ) )
45 42 44 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 ) ) ) ) )
46 45 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 ) ) ) ) )
47 hashcl 
 |-  ( b e. Fin -> ( # ` b ) e. NN0 )
48 47 nn0cnd 
 |-  ( b e. Fin -> ( # ` b ) e. CC )
49 48 mulid2d 
 |-  ( b e. Fin -> ( 1 x. ( # ` b ) ) = ( # ` b ) )
50 0ex 
 |-  (/) e. _V
51 49 48 eqeltrd 
 |-  ( b e. Fin -> ( 1 x. ( # ` b ) ) e. CC )
52 fveq2 
 |-  ( s = (/) -> ( # ` s ) = ( # ` (/) ) )
53 52 8 eqtrdi 
 |-  ( s = (/) -> ( # ` s ) = 0 )
54 53 oveq2d 
 |-  ( s = (/) -> ( -u 1 ^ ( # ` s ) ) = ( -u 1 ^ 0 ) )
55 neg1cn 
 |-  -u 1 e. CC
56 exp0 
 |-  ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 )
57 55 56 ax-mp 
 |-  ( -u 1 ^ 0 ) = 1
58 54 57 eqtrdi 
 |-  ( s = (/) -> ( -u 1 ^ ( # ` s ) ) = 1 )
59 rint0 
 |-  ( s = (/) -> ( b i^i |^| s ) = b )
60 59 fveq2d 
 |-  ( s = (/) -> ( # ` ( b i^i |^| s ) ) = ( # ` b ) )
61 58 60 oveq12d 
 |-  ( s = (/) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = ( 1 x. ( # ` b ) ) )
62 61 sumsn 
 |-  ( ( (/) e. _V /\ ( 1 x. ( # ` b ) ) e. CC ) -> sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = ( 1 x. ( # ` b ) ) )
63 50 51 62 sylancr 
 |-  ( b e. Fin -> sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = ( 1 x. ( # ` b ) ) )
64 48 subid1d 
 |-  ( b e. Fin -> ( ( # ` b ) - 0 ) = ( # ` b ) )
65 49 63 64 3eqtr4rd 
 |-  ( b e. Fin -> ( ( # ` b ) - 0 ) = sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) )
66 65 rgen 
 |-  A. b e. Fin ( ( # ` b ) - 0 ) = sum_ s e. { (/) } ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) )
67 fveq2 
 |-  ( b = x -> ( # ` b ) = ( # ` x ) )
68 ineq1 
 |-  ( b = x -> ( b i^i U. y ) = ( x i^i U. y ) )
69 68 fveq2d 
 |-  ( b = x -> ( # ` ( b i^i U. y ) ) = ( # ` ( x i^i U. y ) ) )
70 67 69 oveq12d 
 |-  ( b = x -> ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = ( ( # ` x ) - ( # ` ( x i^i U. y ) ) ) )
71 simpl 
 |-  ( ( b = x /\ s e. ~P y ) -> b = x )
72 71 ineq1d 
 |-  ( ( b = x /\ s e. ~P y ) -> ( b i^i |^| s ) = ( x i^i |^| s ) )
73 72 fveq2d 
 |-  ( ( b = x /\ s e. ~P y ) -> ( # ` ( b i^i |^| s ) ) = ( # ` ( x i^i |^| s ) ) )
74 73 oveq2d 
 |-  ( ( b = x /\ s e. ~P y ) -> ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( b i^i |^| s ) ) ) = ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( x i^i |^| s ) ) ) )
75 74 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 ) ) ) )
76 70 75 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 ) ) ) ) )
77 76 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 ) ) ) )
78 77 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 ) ) ) )
79 simpr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> x e. Fin )
80 inss1 
 |-  ( x i^i z ) C_ x
81 ssfi 
 |-  ( ( x e. Fin /\ ( x i^i z ) C_ x ) -> ( x i^i z ) e. Fin )
82 79 80 81 sylancl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( x i^i z ) e. Fin )
83 fveq2 
 |-  ( b = ( x i^i z ) -> ( # ` b ) = ( # ` ( x i^i z ) ) )
84 ineq1 
 |-  ( b = ( x i^i z ) -> ( b i^i U. y ) = ( ( x i^i z ) i^i U. y ) )
85 in32 
 |-  ( ( x i^i z ) i^i U. y ) = ( ( x i^i U. y ) i^i z )
86 inass 
 |-  ( ( x i^i U. y ) i^i z ) = ( x i^i ( U. y i^i z ) )
87 85 86 eqtri 
 |-  ( ( x i^i z ) i^i U. y ) = ( x i^i ( U. y i^i z ) )
88 84 87 eqtrdi 
 |-  ( b = ( x i^i z ) -> ( b i^i U. y ) = ( x i^i ( U. y i^i z ) ) )
89 88 fveq2d 
 |-  ( b = ( x i^i z ) -> ( # ` ( b i^i U. y ) ) = ( # ` ( x i^i ( U. y i^i z ) ) ) )
90 83 89 oveq12d 
 |-  ( b = ( x i^i z ) -> ( ( # ` b ) - ( # ` ( b i^i U. y ) ) ) = ( ( # ` ( x i^i z ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) )
91 ineq1 
 |-  ( b = ( x i^i z ) -> ( b i^i |^| s ) = ( ( x i^i z ) i^i |^| s ) )
92 in32 
 |-  ( ( x i^i z ) i^i |^| s ) = ( ( x i^i |^| s ) i^i z )
93 inass 
 |-  ( ( x i^i |^| s ) i^i z ) = ( x i^i ( |^| s i^i z ) )
94 92 93 eqtri 
 |-  ( ( x i^i z ) i^i |^| s ) = ( x i^i ( |^| s i^i z ) )
95 91 94 eqtrdi 
 |-  ( b = ( x i^i z ) -> ( b i^i |^| s ) = ( x i^i ( |^| s i^i z ) ) )
96 95 fveq2d 
 |-  ( b = ( x i^i z ) -> ( # ` ( b i^i |^| s ) ) = ( # ` ( x i^i ( |^| s i^i z ) ) ) )
97 96 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 ) ) ) ) )
98 97 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 ) ) ) ) )
99 90 98 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 ) ) ) ) ) )
100 99 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 ) ) ) ) )
101 82 100 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 ) ) ) ) )
102 78 101 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 ) ) ) ) ) )
103 inss1 
 |-  ( x i^i U. y ) C_ x
104 ssfi 
 |-  ( ( x e. Fin /\ ( x i^i U. y ) C_ x ) -> ( x i^i U. y ) e. Fin )
105 79 103 104 sylancl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( x i^i U. y ) e. Fin )
106 hashcl 
 |-  ( ( x i^i U. y ) e. Fin -> ( # ` ( x i^i U. y ) ) e. NN0 )
107 105 106 syl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( x i^i U. y ) ) e. NN0 )
108 107 nn0cnd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( x i^i U. y ) ) e. CC )
109 hashcl 
 |-  ( ( x i^i z ) e. Fin -> ( # ` ( x i^i z ) ) e. NN0 )
110 82 109 syl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( x i^i z ) ) e. NN0 )
111 110 nn0cnd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( x i^i z ) ) e. CC )
112 inss1 
 |-  ( x i^i ( U. y i^i z ) ) C_ x
113 ssfi 
 |-  ( ( x e. Fin /\ ( x i^i ( U. y i^i z ) ) C_ x ) -> ( x i^i ( U. y i^i z ) ) e. Fin )
114 79 112 113 sylancl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( x i^i ( U. y i^i z ) ) e. Fin )
115 hashcl 
 |-  ( ( x i^i ( U. y i^i z ) ) e. Fin -> ( # ` ( x i^i ( U. y i^i z ) ) ) e. NN0 )
116 114 115 syl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( x i^i ( U. y i^i z ) ) ) e. NN0 )
117 116 nn0cnd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` ( x i^i ( U. y i^i z ) ) ) e. CC )
118 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 ) ) ) ) )
119 105 82 118 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 ) ) ) ) )
120 indi 
 |-  ( x i^i ( U. y u. z ) ) = ( ( x i^i U. y ) u. ( x i^i z ) )
121 120 fveq2i 
 |-  ( # ` ( x i^i ( U. y u. z ) ) ) = ( # ` ( ( x i^i U. y ) u. ( x i^i z ) ) )
122 inindi 
 |-  ( x i^i ( U. y i^i z ) ) = ( ( x i^i U. y ) i^i ( x i^i z ) )
123 122 fveq2i 
 |-  ( # ` ( x i^i ( U. y i^i z ) ) ) = ( # ` ( ( x i^i U. y ) i^i ( x i^i z ) ) )
124 123 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 ) ) ) )
125 119 121 124 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 ) ) ) ) )
126 108 111 117 125 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 ) ) ) ) ) )
127 126 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 ) ) ) ) ) ) )
128 hashcl 
 |-  ( x e. Fin -> ( # ` x ) e. NN0 )
129 128 adantl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` x ) e. NN0 )
130 129 nn0cnd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( # ` x ) e. CC )
131 111 117 subcld 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( ( # ` ( x i^i z ) ) - ( # ` ( x i^i ( U. y i^i z ) ) ) ) e. CC )
132 130 108 131 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 ) ) ) ) ) ) )
133 127 132 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 ) ) ) ) ) )
134 133 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 ) ) ) ) ) )
135 disjdif 
 |-  ( ~P y i^i ( ~P ( y u. { z } ) \ ~P y ) ) = (/)
136 135 a1i 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( ~P y i^i ( ~P ( y u. { z } ) \ ~P y ) ) = (/) )
137 ssun1 
 |-  y C_ ( y u. { z } )
138 137 sspwi 
 |-  ~P y C_ ~P ( y u. { z } )
139 undif 
 |-  ( ~P y C_ ~P ( y u. { z } ) <-> ( ~P y u. ( ~P ( y u. { z } ) \ ~P y ) ) = ~P ( y u. { z } ) )
140 138 139 mpbi 
 |-  ( ~P y u. ( ~P ( y u. { z } ) \ ~P y ) ) = ~P ( y u. { z } )
141 140 eqcomi 
 |-  ~P ( y u. { z } ) = ( ~P y u. ( ~P ( y u. { z } ) \ ~P y ) )
142 141 a1i 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ~P ( y u. { z } ) = ( ~P y u. ( ~P ( y u. { z } ) \ ~P y ) ) )
143 simpll 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> y e. Fin )
144 snfi 
 |-  { z } e. Fin
145 unfi 
 |-  ( ( y e. Fin /\ { z } e. Fin ) -> ( y u. { z } ) e. Fin )
146 143 144 145 sylancl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ( y u. { z } ) e. Fin )
147 pwfi 
 |-  ( ( y u. { z } ) e. Fin <-> ~P ( y u. { z } ) e. Fin )
148 146 147 sylib 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) -> ~P ( y u. { z } ) e. Fin )
149 55 a1i 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> -u 1 e. CC )
150 elpwi 
 |-  ( s e. ~P ( y u. { z } ) -> s C_ ( y u. { z } ) )
151 ssfi 
 |-  ( ( ( y u. { z } ) e. Fin /\ s C_ ( y u. { z } ) ) -> s e. Fin )
152 146 150 151 syl2an 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> s e. Fin )
153 hashcl 
 |-  ( s e. Fin -> ( # ` s ) e. NN0 )
154 152 153 syl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( # ` s ) e. NN0 )
155 149 154 expcld 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( -u 1 ^ ( # ` s ) ) e. CC )
156 simplr 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> x e. Fin )
157 inss1 
 |-  ( x i^i |^| s ) C_ x
158 ssfi 
 |-  ( ( x e. Fin /\ ( x i^i |^| s ) C_ x ) -> ( x i^i |^| s ) e. Fin )
159 156 157 158 sylancl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( x i^i |^| s ) e. Fin )
160 hashcl 
 |-  ( ( x i^i |^| s ) e. Fin -> ( # ` ( x i^i |^| s ) ) e. NN0 )
161 159 160 syl 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( # ` ( x i^i |^| s ) ) e. NN0 )
162 161 nn0cnd 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P ( y u. { z } ) ) -> ( # ` ( x i^i |^| s ) ) e. CC )
163 155 162 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 )
164 136 142 148 163 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 ) ) ) ) )
165 fveq2 
 |-  ( s = ( t u. { z } ) -> ( # ` s ) = ( # ` ( t u. { z } ) ) )
166 165 oveq2d 
 |-  ( s = ( t u. { z } ) -> ( -u 1 ^ ( # ` s ) ) = ( -u 1 ^ ( # ` ( t u. { z } ) ) ) )
167 inteq 
 |-  ( s = ( t u. { z } ) -> |^| s = |^| ( t u. { z } ) )
168 27 intunsn 
 |-  |^| ( t u. { z } ) = ( |^| t i^i z )
169 167 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 166 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 143 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 snex 
 |-  { 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 27 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 163 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 55 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 143 246 247 syl2an 
 |-  ( ( ( ( y e. Fin /\ -. z e. y ) /\ x e. Fin ) /\ s e. ~P y ) -> s e. Fin )
249 248 153 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 138 sseli 
 |-  ( s e. ~P y -> s e. ~P ( y u. { z } ) )
259 258 155 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 156 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 155 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 138 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 163 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 164 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 102 134 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 67 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 syl6ibr 
 |-  ( ( 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 38 46 66 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 ) ) ) )