MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  incexclem Unicode version

Theorem incexclem 12295
Description: Lemma for incexc 12296. (Contributed by Mario Carneiro, 7-Aug-2017.)
Assertion
Ref Expression
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 ) ) ) )
Distinct variable groups:    A, s    B, s

Proof of Theorem incexclem
Dummy variables  b 
t  u  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unieq 3836 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  U. x  =  U. (/) )
2 uni0 3854 . . . . . . . . . . 11  |-  U. (/)  =  (/)
31, 2syl6eq 2331 . . . . . . . . . 10  |-  ( x  =  (/)  ->  U. x  =  (/) )
43ineq2d 3370 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( b  i^i  U. x )  =  ( b  i^i  (/) ) )
5 in0 3480 . . . . . . . . 9  |-  ( b  i^i  (/) )  =  (/)
64, 5syl6eq 2331 . . . . . . . 8  |-  ( x  =  (/)  ->  ( b  i^i  U. x )  =  (/) )
76fveq2d 5529 . . . . . . 7  |-  ( x  =  (/)  ->  ( # `  ( b  i^i  U. x ) )  =  ( # `  (/) ) )
8 hash0 11355 . . . . . . 7  |-  ( # `  (/) )  =  0
97, 8syl6eq 2331 . . . . . 6  |-  ( x  =  (/)  ->  ( # `  ( b  i^i  U. x ) )  =  0 )
109oveq2d 5874 . . . . 5  |-  ( x  =  (/)  ->  ( (
# `  b )  -  ( # `  (
b  i^i  U. x
) ) )  =  ( ( # `  b
)  -  0 ) )
11 pweq 3628 . . . . . . 7  |-  ( x  =  (/)  ->  ~P x  =  ~P (/) )
12 pw0 3762 . . . . . . 7  |-  ~P (/)  =  { (/)
}
1311, 12syl6eq 2331 . . . . . 6  |-  ( x  =  (/)  ->  ~P x  =  { (/) } )
1413sumeq1d 12174 . . . . 5  |-  ( 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 ) ) ) )
1510, 14eqeq12d 2297 . . . 4  |-  ( 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 ) ) ) ) )
1615ralbidv 2563 . . 3  |-  ( 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 3836 . . . . . . . 8  |-  ( x  =  y  ->  U. x  =  U. y )
1817ineq2d 3370 . . . . . . 7  |-  ( x  =  y  ->  (
b  i^i  U. x
)  =  ( b  i^i  U. y ) )
1918fveq2d 5529 . . . . . 6  |-  ( x  =  y  ->  ( # `
 ( b  i^i  U. x ) )  =  ( # `  (
b  i^i  U. y
) ) )
2019oveq2d 5874 . . . . 5  |-  ( x  =  y  ->  (
( # `  b )  -  ( # `  (
b  i^i  U. x
) ) )  =  ( ( # `  b
)  -  ( # `  ( b  i^i  U. y ) ) ) )
21 pweq 3628 . . . . . 6  |-  ( x  =  y  ->  ~P x  =  ~P y
)
2221sumeq1d 12174 . . . . 5  |-  ( 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 ) ) ) )
2320, 22eqeq12d 2297 . . . 4  |-  ( 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 ) ) ) ) )
2423ralbidv 2563 . . 3  |-  ( 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 3836 . . . . . . . . 9  |-  ( x  =  ( y  u. 
{ z } )  ->  U. x  =  U. ( y  u.  {
z } ) )
26 uniun 3846 . . . . . . . . . 10  |-  U. (
y  u.  { z } )  =  ( U. y  u.  U. { z } )
27 vex 2791 . . . . . . . . . . . 12  |-  z  e. 
_V
2827unisn 3843 . . . . . . . . . . 11  |-  U. {
z }  =  z
2928uneq2i 3326 . . . . . . . . . 10  |-  ( U. y  u.  U. { z } )  =  ( U. y  u.  z
)
3026, 29eqtri 2303 . . . . . . . . 9  |-  U. (
y  u.  { z } )  =  ( U. y  u.  z
)
3125, 30syl6eq 2331 . . . . . . . 8  |-  ( x  =  ( y  u. 
{ z } )  ->  U. x  =  ( U. y  u.  z
) )
3231ineq2d 3370 . . . . . . 7  |-  ( x  =  ( y  u. 
{ z } )  ->  ( b  i^i  U. x )  =  ( b  i^i  ( U. y  u.  z )
) )
3332fveq2d 5529 . . . . . 6  |-  ( x  =  ( y  u. 
{ z } )  ->  ( # `  (
b  i^i  U. x
) )  =  (
# `  ( b  i^i  ( U. y  u.  z ) ) ) )
3433oveq2d 5874 . . . . 5  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ( # `  b )  -  ( # `
 ( b  i^i  U. x ) ) )  =  ( ( # `  b )  -  ( # `
 ( b  i^i  ( U. y  u.  z ) ) ) ) )
35 pweq 3628 . . . . . 6  |-  ( x  =  ( y  u. 
{ z } )  ->  ~P x  =  ~P ( y  u. 
{ z } ) )
3635sumeq1d 12174 . . . . 5  |-  ( 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 ) ) ) )
3734, 36eqeq12d 2297 . . . 4  |-  ( 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 ) ) ) ) )
3837ralbidv 2563 . . 3  |-  ( 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 3836 . . . . . . . 8  |-  ( x  =  A  ->  U. x  =  U. A )
4039ineq2d 3370 . . . . . . 7  |-  ( x  =  A  ->  (
b  i^i  U. x
)  =  ( b  i^i  U. A ) )
4140fveq2d 5529 . . . . . 6  |-  ( x  =  A  ->  ( # `
 ( b  i^i  U. x ) )  =  ( # `  (
b  i^i  U. A ) ) )
4241oveq2d 5874 . . . . 5  |-  ( x  =  A  ->  (
( # `  b )  -  ( # `  (
b  i^i  U. x
) ) )  =  ( ( # `  b
)  -  ( # `  ( b  i^i  U. A ) ) ) )
43 pweq 3628 . . . . . 6  |-  ( x  =  A  ->  ~P x  =  ~P A
)
4443sumeq1d 12174 . . . . 5  |-  ( 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 ) ) ) )
4542, 44eqeq12d 2297 . . . 4  |-  ( 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 ) ) ) ) )
4645ralbidv 2563 . . 3  |-  ( 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 11350 . . . . . . 7  |-  ( b  e.  Fin  ->  ( # `
 b )  e. 
NN0 )
4847nn0cnd 10020 . . . . . 6  |-  ( b  e.  Fin  ->  ( # `
 b )  e.  CC )
4948mulid2d 8853 . . . . 5  |-  ( b  e.  Fin  ->  (
1  x.  ( # `  b ) )  =  ( # `  b
) )
50 0ex 4150 . . . . . . 7  |-  (/)  e.  _V
5150a1i 10 . . . . . 6  |-  ( b  e.  Fin  ->  (/)  e.  _V )
5249, 48eqeltrd 2357 . . . . . 6  |-  ( b  e.  Fin  ->  (
1  x.  ( # `  b ) )  e.  CC )
53 fveq2 5525 . . . . . . . . . . 11  |-  ( s  =  (/)  ->  ( # `  s )  =  (
# `  (/) ) )
5453, 8syl6eq 2331 . . . . . . . . . 10  |-  ( s  =  (/)  ->  ( # `  s )  =  0 )
5554oveq2d 5874 . . . . . . . . 9  |-  ( s  =  (/)  ->  ( -u
1 ^ ( # `  s ) )  =  ( -u 1 ^ 0 ) )
56 neg1cn 9813 . . . . . . . . . 10  |-  -u 1  e.  CC
57 exp0 11108 . . . . . . . . . 10  |-  ( -u
1  e.  CC  ->  (
-u 1 ^ 0 )  =  1 )
5856, 57ax-mp 8 . . . . . . . . 9  |-  ( -u
1 ^ 0 )  =  1
5955, 58syl6eq 2331 . . . . . . . 8  |-  ( s  =  (/)  ->  ( -u
1 ^ ( # `  s ) )  =  1 )
60 ssv 3198 . . . . . . . . . . 11  |-  b  C_  _V
61 inteq 3865 . . . . . . . . . . . 12  |-  ( s  =  (/)  ->  |^| s  =  |^| (/) )
62 int0 3876 . . . . . . . . . . . 12  |-  |^| (/)  =  _V
6361, 62syl6eq 2331 . . . . . . . . . . 11  |-  ( s  =  (/)  ->  |^| s  =  _V )
6460, 63syl5sseqr 3227 . . . . . . . . . 10  |-  ( s  =  (/)  ->  b  C_  |^| s )
65 df-ss 3166 . . . . . . . . . 10  |-  ( b 
C_  |^| s  <->  ( b  i^i  |^| s )  =  b )
6664, 65sylib 188 . . . . . . . . 9  |-  ( s  =  (/)  ->  ( b  i^i  |^| s )  =  b )
6766fveq2d 5529 . . . . . . . 8  |-  ( s  =  (/)  ->  ( # `  ( b  i^i  |^| s ) )  =  ( # `  b
) )
6859, 67oveq12d 5876 . . . . . . 7  |-  ( s  =  (/)  ->  ( (
-u 1 ^ ( # `
 s ) )  x.  ( # `  (
b  i^i  |^| s ) ) )  =  ( 1  x.  ( # `  b ) ) )
6968sumsn 12213 . . . . . 6  |-  ( (
(/)  e.  _V  /\  (
1  x.  ( # `  b ) )  e.  CC )  ->  sum_ s  e.  { (/) }  ( (
-u 1 ^ ( # `
 s ) )  x.  ( # `  (
b  i^i  |^| s ) ) )  =  ( 1  x.  ( # `  b ) ) )
7051, 52, 69syl2anc 642 . . . . 5  |-  ( b  e.  Fin  ->  sum_ s  e.  { (/) }  ( (
-u 1 ^ ( # `
 s ) )  x.  ( # `  (
b  i^i  |^| s ) ) )  =  ( 1  x.  ( # `  b ) ) )
7148subid1d 9146 . . . . 5  |-  ( b  e.  Fin  ->  (
( # `  b )  -  0 )  =  ( # `  b
) )
7249, 70, 713eqtr4rd 2326 . . . 4  |-  ( b  e.  Fin  ->  (
( # `  b )  -  0 )  = 
sum_ s  e.  { (/)
}  ( ( -u
1 ^ ( # `  s ) )  x.  ( # `  (
b  i^i  |^| s ) ) ) )
7372rgen 2608 . . 3  |-  A. b  e.  Fin  ( ( # `  b )  -  0 )  =  sum_ s  e.  { (/) }  ( (
-u 1 ^ ( # `
 s ) )  x.  ( # `  (
b  i^i  |^| s ) ) )
74 fveq2 5525 . . . . . . . . . . . 12  |-  ( b  =  x  ->  ( # `
 b )  =  ( # `  x
) )
75 ineq1 3363 . . . . . . . . . . . . 13  |-  ( b  =  x  ->  (
b  i^i  U. y
)  =  ( x  i^i  U. y ) )
7675fveq2d 5529 . . . . . . . . . . . 12  |-  ( b  =  x  ->  ( # `
 ( b  i^i  U. y ) )  =  ( # `  (
x  i^i  U. y
) ) )
7774, 76oveq12d 5876 . . . . . . . . . . 11  |-  ( b  =  x  ->  (
( # `  b )  -  ( # `  (
b  i^i  U. y
) ) )  =  ( ( # `  x
)  -  ( # `  ( x  i^i  U. y ) ) ) )
78 simpl 443 . . . . . . . . . . . . . . 15  |-  ( ( b  =  x  /\  s  e.  ~P y
)  ->  b  =  x )
7978ineq1d 3369 . . . . . . . . . . . . . 14  |-  ( ( b  =  x  /\  s  e.  ~P y
)  ->  ( b  i^i  |^| s )  =  ( x  i^i  |^| s ) )
8079fveq2d 5529 . . . . . . . . . . . . 13  |-  ( ( b  =  x  /\  s  e.  ~P y
)  ->  ( # `  (
b  i^i  |^| s ) )  =  ( # `  ( x  i^i  |^| s ) ) )
8180oveq2d 5874 . . . . . . . . . . . 12  |-  ( ( b  =  x  /\  s  e.  ~P y
)  ->  ( ( -u 1 ^ ( # `  s ) )  x.  ( # `  (
b  i^i  |^| s ) ) )  =  ( ( -u 1 ^ ( # `  s
) )  x.  ( # `
 ( x  i^i  |^| s ) ) ) )
8281sumeq2dv 12176 . . . . . . . . . . 11  |-  ( 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 ) ) ) )
8377, 82eqeq12d 2297 . . . . . . . . . 10  |-  ( 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 ) ) ) ) )
8483rspcva 2882 . . . . . . . . 9  |-  ( ( 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 ) ) ) )
8584adantll 694 . . . . . . . 8  |-  ( ( ( ( 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 ) ) ) )
86 simpr 447 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  x  e.  Fin )
87 inss1 3389 . . . . . . . . . 10  |-  ( x  i^i  z )  C_  x
88 ssfi 7083 . . . . . . . . . 10  |-  ( ( x  e.  Fin  /\  ( x  i^i  z
)  C_  x )  ->  ( x  i^i  z
)  e.  Fin )
8986, 87, 88sylancl 643 . . . . . . . . 9  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  (
x  i^i  z )  e.  Fin )
90 fveq2 5525 . . . . . . . . . . . 12  |-  ( b  =  ( x  i^i  z )  ->  ( # `
 b )  =  ( # `  (
x  i^i  z )
) )
91 ineq1 3363 . . . . . . . . . . . . . 14  |-  ( b  =  ( x  i^i  z )  ->  (
b  i^i  U. y
)  =  ( ( x  i^i  z )  i^i  U. y ) )
92 in32 3381 . . . . . . . . . . . . . . 15  |-  ( ( x  i^i  z )  i^i  U. y )  =  ( ( x  i^i  U. y )  i^i  z )
93 inass 3379 . . . . . . . . . . . . . . 15  |-  ( ( x  i^i  U. y
)  i^i  z )  =  ( x  i^i  ( U. y  i^i  z ) )
9492, 93eqtri 2303 . . . . . . . . . . . . . 14  |-  ( ( x  i^i  z )  i^i  U. y )  =  ( x  i^i  ( U. y  i^i  z ) )
9591, 94syl6eq 2331 . . . . . . . . . . . . 13  |-  ( b  =  ( x  i^i  z )  ->  (
b  i^i  U. y
)  =  ( x  i^i  ( U. y  i^i  z ) ) )
9695fveq2d 5529 . . . . . . . . . . . 12  |-  ( b  =  ( x  i^i  z )  ->  ( # `
 ( b  i^i  U. y ) )  =  ( # `  (
x  i^i  ( U. y  i^i  z ) ) ) )
9790, 96oveq12d 5876 . . . . . . . . . . 11  |-  ( b  =  ( x  i^i  z )  ->  (
( # `  b )  -  ( # `  (
b  i^i  U. y
) ) )  =  ( ( # `  (
x  i^i  z )
)  -  ( # `  ( x  i^i  ( U. y  i^i  z
) ) ) ) )
98 ineq1 3363 . . . . . . . . . . . . . . 15  |-  ( b  =  ( x  i^i  z )  ->  (
b  i^i  |^| s )  =  ( ( x  i^i  z )  i^i  |^| s ) )
99 in32 3381 . . . . . . . . . . . . . . . 16  |-  ( ( x  i^i  z )  i^i  |^| s )  =  ( ( x  i^i  |^| s )  i^i  z
)
100 inass 3379 . . . . . . . . . . . . . . . 16  |-  ( ( x  i^i  |^| s
)  i^i  z )  =  ( x  i^i  ( |^| s  i^i  z ) )
10199, 100eqtri 2303 . . . . . . . . . . . . . . 15  |-  ( ( x  i^i  z )  i^i  |^| s )  =  ( x  i^i  ( |^| s  i^i  z
) )
10298, 101syl6eq 2331 . . . . . . . . . . . . . 14  |-  ( b  =  ( x  i^i  z )  ->  (
b  i^i  |^| s )  =  ( x  i^i  ( |^| s  i^i  z ) ) )
103102fveq2d 5529 . . . . . . . . . . . . 13  |-  ( b  =  ( x  i^i  z )  ->  ( # `
 ( b  i^i  |^| s ) )  =  ( # `  (
x  i^i  ( |^| s  i^i  z ) ) ) )
104103oveq2d 5874 . . . . . . . . . . . 12  |-  ( b  =  ( x  i^i  z )  ->  (
( -u 1 ^ ( # `
 s ) )  x.  ( # `  (
b  i^i  |^| s ) ) )  =  ( ( -u 1 ^ ( # `  s
) )  x.  ( # `
 ( x  i^i  ( |^| s  i^i  z ) ) ) ) )
105104sumeq2sdv 12177 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
10697, 105eqeq12d 2297 . . . . . . . . . 10  |-  ( 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 ) ) ) ) ) )
107106rspcva 2882 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) ) )
10889, 107sylan 457 . . . . . . . 8  |-  ( ( ( ( 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 ) ) ) ) )
10985, 108oveq12d 5876 . . . . . . 7  |-  ( ( ( ( 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 ) ) ) ) ) )
110 inss1 3389 . . . . . . . . . . . . . 14  |-  ( x  i^i  U. y ) 
C_  x
111 ssfi 7083 . . . . . . . . . . . . . 14  |-  ( ( x  e.  Fin  /\  ( x  i^i  U. y
)  C_  x )  ->  ( x  i^i  U. y )  e.  Fin )
11286, 110, 111sylancl 643 . . . . . . . . . . . . 13  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  (
x  i^i  U. y
)  e.  Fin )
113 hashun3 11366 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
) ) ) )
114112, 89, 113syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) ) )
115 indi 3415 . . . . . . . . . . . . 13  |-  ( x  i^i  ( U. y  u.  z ) )  =  ( ( x  i^i  U. y )  u.  (
x  i^i  z )
)
116115fveq2i 5528 . . . . . . . . . . . 12  |-  ( # `  ( x  i^i  ( U. y  u.  z
) ) )  =  ( # `  (
( x  i^i  U. y )  u.  (
x  i^i  z )
) )
117 inindi 3386 . . . . . . . . . . . . . 14  |-  ( x  i^i  ( U. y  i^i  z ) )  =  ( ( x  i^i  U. y )  i^i  (
x  i^i  z )
)
118117fveq2i 5528 . . . . . . . . . . . . 13  |-  ( # `  ( x  i^i  ( U. y  i^i  z
) ) )  =  ( # `  (
( x  i^i  U. y )  i^i  (
x  i^i  z )
) )
119118oveq2i 5869 . . . . . . . . . . . 12  |-  ( ( ( # `  (
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 )
) ) )
120114, 116, 1193eqtr4g 2340 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) ) )
121 hashcl 11350 . . . . . . . . . . . . . 14  |-  ( ( x  i^i  U. y
)  e.  Fin  ->  (
# `  ( x  i^i  U. y ) )  e.  NN0 )
122112, 121syl 15 . . . . . . . . . . . . 13  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ( # `
 ( x  i^i  U. y ) )  e. 
NN0 )
123122nn0cnd 10020 . . . . . . . . . . . 12  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ( # `
 ( x  i^i  U. y ) )  e.  CC )
124 hashcl 11350 . . . . . . . . . . . . . 14  |-  ( ( x  i^i  z )  e.  Fin  ->  ( # `
 ( x  i^i  z ) )  e. 
NN0 )
12589, 124syl 15 . . . . . . . . . . . . 13  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ( # `
 ( x  i^i  z ) )  e. 
NN0 )
126125nn0cnd 10020 . . . . . . . . . . . 12  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ( # `
 ( x  i^i  z ) )  e.  CC )
127 inss1 3389 . . . . . . . . . . . . . . 15  |-  ( x  i^i  ( U. y  i^i  z ) )  C_  x
128 ssfi 7083 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  Fin  /\  ( x  i^i  ( U. y  i^i  z
) )  C_  x
)  ->  ( x  i^i  ( U. y  i^i  z ) )  e. 
Fin )
12986, 127, 128sylancl 643 . . . . . . . . . . . . . 14  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  (
x  i^i  ( U. y  i^i  z ) )  e.  Fin )
130 hashcl 11350 . . . . . . . . . . . . . 14  |-  ( ( x  i^i  ( U. y  i^i  z ) )  e.  Fin  ->  ( # `
 ( x  i^i  ( U. y  i^i  z ) ) )  e.  NN0 )
131129, 130syl 15 . . . . . . . . . . . . 13  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ( # `
 ( x  i^i  ( U. y  i^i  z ) ) )  e.  NN0 )
132131nn0cnd 10020 . . . . . . . . . . . 12  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ( # `
 ( x  i^i  ( U. y  i^i  z ) ) )  e.  CC )
133123, 126, 132addsubassd 9177 . . . . . . . . . . 11  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  (
( ( # `  (
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  z
) ) ) ) ) )
134120, 133eqtrd 2315 . . . . . . . . . 10  |-  ( ( ( 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
) ) ) ) ) )
135134oveq2d 5874 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) ) ) ) )
136 hashcl 11350 . . . . . . . . . . . 12  |-  ( x  e.  Fin  ->  ( # `
 x )  e. 
NN0 )
137136adantl 452 . . . . . . . . . . 11  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ( # `
 x )  e. 
NN0 )
138137nn0cnd 10020 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ( # `
 x )  e.  CC )
139126, 132subcld 9157 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  (
( # `  ( x  i^i  z ) )  -  ( # `  (
x  i^i  ( U. y  i^i  z ) ) ) )  e.  CC )
140138, 123, 139subsub4d 9188 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) ) ) ) )
141135, 140eqtr4d 2318 . . . . . . . 8  |-  ( ( ( 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 ) ) ) ) ) )
142141adantr 451 . . . . . . 7  |-  ( ( ( ( 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
) ) ) ) ) )
143 disjdif 3526 . . . . . . . . . . 11  |-  ( ~P y  i^i  ( ~P ( y  u.  {
z } )  \  ~P y ) )  =  (/)
144143a1i 10 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ( ~P y  i^i  ( ~P ( y  u.  {
z } )  \  ~P y ) )  =  (/) )
145 ssun1 3338 . . . . . . . . . . . . . 14  |-  y  C_  ( y  u.  {
z } )
146 sspwb 4223 . . . . . . . . . . . . . 14  |-  ( y 
C_  ( y  u. 
{ z } )  <->  ~P y  C_  ~P (
y  u.  { z } ) )
147145, 146mpbi 199 . . . . . . . . . . . . 13  |-  ~P y  C_ 
~P ( y  u. 
{ z } )
148 undif 3534 . . . . . . . . . . . . 13  |-  ( ~P y  C_  ~P (
y  u.  { z } )  <->  ( ~P y  u.  ( ~P ( y  u.  {
z } )  \  ~P y ) )  =  ~P ( y  u. 
{ z } ) )
149147, 148mpbi 199 . . . . . . . . . . . 12  |-  ( ~P y  u.  ( ~P ( y  u.  {
z } )  \  ~P y ) )  =  ~P ( y  u. 
{ z } )
150149eqcomi 2287 . . . . . . . . . . 11  |-  ~P (
y  u.  { z } )  =  ( ~P y  u.  ( ~P ( y  u.  {
z } )  \  ~P y ) )
151150a1i 10 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ~P ( y  u.  {
z } )  =  ( ~P y  u.  ( ~P ( y  u.  { z } )  \  ~P y
) ) )
152 simpll 730 . . . . . . . . . . . 12  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  y  e.  Fin )
153 snfi 6941 . . . . . . . . . . . 12  |-  { z }  e.  Fin
154 unfi 7124 . . . . . . . . . . . 12  |-  ( ( y  e.  Fin  /\  { z }  e.  Fin )  ->  ( y  u. 
{ z } )  e.  Fin )
155152, 153, 154sylancl 643 . . . . . . . . . . 11  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  (
y  u.  { z } )  e.  Fin )
156 pwfi 7151 . . . . . . . . . . 11  |-  ( ( y  u.  { z } )  e.  Fin  <->  ~P ( y  u.  {
z } )  e. 
Fin )
157155, 156sylib 188 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ~P ( y  u.  {
z } )  e. 
Fin )
15856a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P ( y  u. 
{ z } ) )  ->  -u 1  e.  CC )
159 elpwi 3633 . . . . . . . . . . . . . 14  |-  ( s  e.  ~P ( y  u.  { z } )  ->  s  C_  ( y  u.  {
z } ) )
160 ssfi 7083 . . . . . . . . . . . . . 14  |-  ( ( ( y  u.  {
z } )  e. 
Fin  /\  s  C_  ( y  u.  {
z } ) )  ->  s  e.  Fin )
161155, 159, 160syl2an 463 . . . . . . . . . . . . 13  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P ( y  u. 
{ z } ) )  ->  s  e.  Fin )
162 hashcl 11350 . . . . . . . . . . . . 13  |-  ( s  e.  Fin  ->  ( # `
 s )  e. 
NN0 )
163161, 162syl 15 . . . . . . . . . . . 12  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P ( y  u. 
{ z } ) )  ->  ( # `  s
)  e.  NN0 )
164158, 163expcld 11245 . . . . . . . . . . 11  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P ( y  u. 
{ z } ) )  ->  ( -u 1 ^ ( # `  s
) )  e.  CC )
165 simplr 731 . . . . . . . . . . . . . 14  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P ( y  u. 
{ z } ) )  ->  x  e.  Fin )
166 inss1 3389 . . . . . . . . . . . . . 14  |-  ( x  i^i  |^| s )  C_  x
167 ssfi 7083 . . . . . . . . . . . . . 14  |-  ( ( x  e.  Fin  /\  ( x  i^i  |^| s
)  C_  x )  ->  ( x  i^i  |^| s )  e.  Fin )
168165, 166, 167sylancl 643 . . . . . . . . . . . . 13  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P ( y  u. 
{ z } ) )  ->  ( x  i^i  |^| s )  e. 
Fin )
169 hashcl 11350 . . . . . . . . . . . . 13  |-  ( ( x  i^i  |^| s
)  e.  Fin  ->  (
# `  ( x  i^i  |^| s ) )  e.  NN0 )
170168, 169syl 15 . . . . . . . . . . . 12  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P ( y  u. 
{ z } ) )  ->  ( # `  (
x  i^i  |^| s ) )  e.  NN0 )
171170nn0cnd 10020 . . . . . . . . . . 11  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P ( y  u. 
{ z } ) )  ->  ( # `  (
x  i^i  |^| s ) )  e.  CC )
172164, 171mulcld 8855 . . . . . . . . . 10  |-  ( ( ( ( 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 )
173144, 151, 157, 172fsumsplit 12212 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) ) )
174 fveq2 5525 . . . . . . . . . . . . . 14  |-  ( s  =  ( t  u. 
{ z } )  ->  ( # `  s
)  =  ( # `  ( t  u.  {
z } ) ) )
175174oveq2d 5874 . . . . . . . . . . . . 13  |-  ( s  =  ( t  u. 
{ z } )  ->  ( -u 1 ^ ( # `  s
) )  =  (
-u 1 ^ ( # `
 ( t  u. 
{ z } ) ) ) )
176 inteq 3865 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( t  u. 
{ z } )  ->  |^| s  =  |^| ( t  u.  {
z } ) )
17727intunsn 3901 . . . . . . . . . . . . . . . 16  |-  |^| (
t  u.  { z } )  =  (
|^| t  i^i  z
)
178176, 177syl6eq 2331 . . . . . . . . . . . . . . 15  |-  ( s  =  ( t  u. 
{ z } )  ->  |^| s  =  (
|^| t  i^i  z
) )
179178ineq2d 3370 . . . . . . . . . . . . . 14  |-  ( s  =  ( t  u. 
{ z } )  ->  ( x  i^i  |^| s )  =  ( x  i^i  ( |^| t  i^i  z ) ) )
180179fveq2d 5529 . . . . . . . . . . . . 13  |-  ( s  =  ( t  u. 
{ z } )  ->  ( # `  (
x  i^i  |^| s ) )  =  ( # `  ( x  i^i  ( |^| t  i^i  z
) ) ) )
181175, 180oveq12d 5876 . . . . . . . . . . . 12  |-  ( 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 ) ) ) ) )
182 pwfi 7151 . . . . . . . . . . . . 13  |-  ( y  e.  Fin  <->  ~P y  e.  Fin )
183152, 182sylib 188 . . . . . . . . . . . 12  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ~P y  e.  Fin )
184 eqid 2283 . . . . . . . . . . . . 13  |-  ( u  e.  ~P y  |->  ( u  u.  { z } ) )  =  ( u  e.  ~P y  |->  ( u  u. 
{ z } ) )
185 elpwi 3633 . . . . . . . . . . . . . . . . 17  |-  ( u  e.  ~P y  ->  u  C_  y )
186185adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  u  e.  ~P y )  ->  u  C_  y )
187 unss1 3344 . . . . . . . . . . . . . . . 16  |-  ( u 
C_  y  ->  (
u  u.  { z } )  C_  (
y  u.  { z } ) )
188186, 187syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  u  e.  ~P y )  -> 
( u  u.  {
z } )  C_  ( y  u.  {
z } ) )
189 vex 2791 . . . . . . . . . . . . . . . . 17  |-  u  e. 
_V
190 snex 4216 . . . . . . . . . . . . . . . . 17  |-  { z }  e.  _V
191189, 190unex 4518 . . . . . . . . . . . . . . . 16  |-  ( u  u.  { z } )  e.  _V
192191elpw 3631 . . . . . . . . . . . . . . 15  |-  ( ( u  u.  { z } )  e.  ~P ( y  u.  {
z } )  <->  ( u  u.  { z } ) 
C_  ( y  u. 
{ z } ) )
193188, 192sylibr 203 . . . . . . . . . . . . . 14  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  u  e.  ~P y )  -> 
( u  u.  {
z } )  e. 
~P ( y  u. 
{ z } ) )
194 simpllr 735 . . . . . . . . . . . . . . 15  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  u  e.  ~P y )  ->  -.  z  e.  y
)
195 elpwi 3633 . . . . . . . . . . . . . . . 16  |-  ( ( u  u.  { z } )  e.  ~P y  ->  ( u  u. 
{ z } ) 
C_  y )
196 ssun2 3339 . . . . . . . . . . . . . . . . . . 19  |-  { z }  C_  ( u  u.  { z } )
19727snss 3748 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  ( u  u. 
{ z } )  <->  { z }  C_  ( u  u.  { z } ) )
198196, 197mpbir 200 . . . . . . . . . . . . . . . . . 18  |-  z  e.  ( u  u.  {
z } )
199198a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  u  e.  ~P y )  -> 
z  e.  ( u  u.  { z } ) )
200 ssel 3174 . . . . . . . . . . . . . . . . 17  |-  ( ( u  u.  { z } )  C_  y  ->  ( z  e.  ( u  u.  { z } )  ->  z  e.  y ) )
201199, 200syl5com 26 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  u  e.  ~P y )  -> 
( ( u  u. 
{ z } ) 
C_  y  ->  z  e.  y ) )
202195, 201syl5 28 . . . . . . . . . . . . . . 15  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  u  e.  ~P y )  -> 
( ( u  u. 
{ z } )  e.  ~P y  -> 
z  e.  y ) )
203194, 202mtod 168 . . . . . . . . . . . . . 14  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  u  e.  ~P y )  ->  -.  ( u  u.  {
z } )  e. 
~P y )
204193, 203eldifd 3163 . . . . . . . . . . . . 13  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  u  e.  ~P y )  -> 
( u  u.  {
z } )  e.  ( ~P ( y  u.  { z } )  \  ~P y
) )
205 eldifi 3298 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ( ~P (
y  u.  { z } )  \  ~P y )  ->  s  e.  ~P ( y  u. 
{ z } ) )
206205adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ( ~P ( y  u.  { z } )  \  ~P y
) )  ->  s  e.  ~P ( y  u. 
{ z } ) )
207206elpwid 3634 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ( ~P ( y  u.  { z } )  \  ~P y
) )  ->  s  C_  ( y  u.  {
z } ) )
208 uncom 3319 . . . . . . . . . . . . . . . 16  |-  ( y  u.  { z } )  =  ( { z }  u.  y
)
209207, 208syl6sseq 3224 . . . . . . . . . . . . . . 15  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ( ~P ( y  u.  { z } )  \  ~P y
) )  ->  s  C_  ( { z }  u.  y ) )
210 ssundif 3537 . . . . . . . . . . . . . . 15  |-  ( s 
C_  ( { z }  u.  y )  <-> 
( s  \  {
z } )  C_  y )
211209, 210sylib 188 . . . . . . . . . . . . . 14  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ( ~P ( y  u.  { z } )  \  ~P y
) )  ->  (
s  \  { z } )  C_  y
)
212 vex 2791 . . . . . . . . . . . . . . 15  |-  y  e. 
_V
213212elpw2 4175 . . . . . . . . . . . . . 14  |-  ( ( s  \  { z } )  e.  ~P y 
<->  ( s  \  {
z } )  C_  y )
214211, 213sylibr 203 . . . . . . . . . . . . 13  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ( ~P ( y  u.  { z } )  \  ~P y
) )  ->  (
s  \  { z } )  e.  ~P y )
215 elpwunsn 4568 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  ( ~P (
y  u.  { z } )  \  ~P y )  ->  z  e.  s )
216215ad2antll 709 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  (
u  e.  ~P y  /\  s  e.  ( ~P ( y  u.  {
z } )  \  ~P y ) ) )  ->  z  e.  s )
217 snssi 3759 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  s  ->  { z }  C_  s )
218216, 217syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  (
u  e.  ~P y  /\  s  e.  ( ~P ( y  u.  {
z } )  \  ~P y ) ) )  ->  { z } 
C_  s )
219 ssequn2 3348 . . . . . . . . . . . . . . . . 17  |-  ( { z }  C_  s  <->  ( s  u.  { z } )  =  s )
220218, 219sylib 188 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 )
221220eqcomd 2288 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 } ) )
222 uneq1 3322 . . . . . . . . . . . . . . . . 17  |-  ( u  =  ( s  \  { z } )  ->  ( u  u. 
{ z } )  =  ( ( s 
\  { z } )  u.  { z } ) )
223 undif1 3529 . . . . . . . . . . . . . . . . 17  |-  ( ( s  \  { z } )  u.  {
z } )  =  ( s  u.  {
z } )
224222, 223syl6eq 2331 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( s  \  { z } )  ->  ( u  u. 
{ z } )  =  ( s  u. 
{ z } ) )
225224eqeq2d 2294 . . . . . . . . . . . . . . 15  |-  ( u  =  ( s  \  { z } )  ->  ( s  =  ( u  u.  {
z } )  <->  s  =  ( s  u.  {
z } ) ) )
226221, 225syl5ibrcom 213 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 } ) ) )
227194adantrr 697 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  (
u  e.  ~P y  /\  s  e.  ( ~P ( y  u.  {
z } )  \  ~P y ) ) )  ->  -.  z  e.  y )
228185ad2antrl 708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  (
u  e.  ~P y  /\  s  e.  ( ~P ( y  u.  {
z } )  \  ~P y ) ) )  ->  u  C_  y
)
229228sseld 3179 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  (
u  e.  ~P y  /\  s  e.  ( ~P ( y  u.  {
z } )  \  ~P y ) ) )  ->  ( z  e.  u  ->  z  e.  y ) )
230227, 229mtod 168 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  (
u  e.  ~P y  /\  s  e.  ( ~P ( y  u.  {
z } )  \  ~P y ) ) )  ->  -.  z  e.  u )
231 difsneq 3757 . . . . . . . . . . . . . . . . 17  |-  ( -.  z  e.  u  <->  ( u  \  { z } )  =  u )
232230, 231sylib 188 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  (
u  e.  ~P y  /\  s  e.  ( ~P ( y  u.  {
z } )  \  ~P y ) ) )  ->  ( u  \  { z } )  =  u )
233232eqcomd 2288 . . . . . . . . . . . . . . 15  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  (
u  e.  ~P y  /\  s  e.  ( ~P ( y  u.  {
z } )  \  ~P y ) ) )  ->  u  =  ( u  \  { z } ) )
234 difeq1 3287 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( u  u. 
{ z } )  ->  ( s  \  { z } )  =  ( ( u  u.  { z } )  \  { z } ) )
235 difun2 3533 . . . . . . . . . . . . . . . . 17  |-  ( ( u  u.  { z } )  \  {
z } )  =  ( u  \  {
z } )
236234, 235syl6eq 2331 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( u  u. 
{ z } )  ->  ( s  \  { z } )  =  ( u  \  { z } ) )
237236eqeq2d 2294 . . . . . . . . . . . . . . 15  |-  ( s  =  ( u  u. 
{ z } )  ->  ( u  =  ( s  \  {
z } )  <->  u  =  ( u  \  { z } ) ) )
238233, 237syl5ibrcom 213 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 } ) ) )
239226, 238impbid 183 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 } ) ) )
240184, 204, 214, 239f1o2d 6069 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
241 uneq1 3322 . . . . . . . . . . . . . 14  |-  ( u  =  t  ->  (
u  u.  { z } )  =  ( t  u.  { z } ) )
242 vex 2791 . . . . . . . . . . . . . . 15  |-  t  e. 
_V
243242, 190unex 4518 . . . . . . . . . . . . . 14  |-  ( t  u.  { z } )  e.  _V
244241, 184, 243fvmpt 5602 . . . . . . . . . . . . 13  |-  ( t  e.  ~P y  -> 
( ( u  e. 
~P y  |->  ( u  u.  { z } ) ) `  t
)  =  ( t  u.  { z } ) )
245244adantl 452 . . . . . . . . . . . 12  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  t  e.  ~P y )  -> 
( ( u  e. 
~P y  |->  ( u  u.  { z } ) ) `  t
)  =  ( t  u.  { z } ) )
246205, 172sylan2 460 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
247181, 183, 240, 245, 246fsumf1o 12196 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) ) )
248 uneq1 3322 . . . . . . . . . . . . . . . 16  |-  ( t  =  s  ->  (
t  u.  { z } )  =  ( s  u.  { z } ) )
249248fveq2d 5529 . . . . . . . . . . . . . . 15  |-  ( t  =  s  ->  ( # `
 ( t  u. 
{ z } ) )  =  ( # `  ( s  u.  {
z } ) ) )
250249oveq2d 5874 . . . . . . . . . . . . . 14  |-  ( t  =  s  ->  ( -u 1 ^ ( # `  ( t  u.  {
z } ) ) )  =  ( -u
1 ^ ( # `  ( s  u.  {
z } ) ) ) )
251 inteq 3865 . . . . . . . . . . . . . . . . 17  |-  ( t  =  s  ->  |^| t  =  |^| s )
252251ineq1d 3369 . . . . . . . . . . . . . . . 16  |-  ( t  =  s  ->  ( |^| t  i^i  z
)  =  ( |^| s  i^i  z ) )
253252ineq2d 3370 . . . . . . . . . . . . . . 15  |-  ( t  =  s  ->  (
x  i^i  ( |^| t  i^i  z ) )  =  ( x  i^i  ( |^| s  i^i  z ) ) )
254253fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( t  =  s  ->  ( # `
 ( x  i^i  ( |^| t  i^i  z ) ) )  =  ( # `  (
x  i^i  ( |^| s  i^i  z ) ) ) )
255250, 254oveq12d 5876 . . . . . . . . . . . . 13  |-  ( 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 ) ) ) ) )
256255cbvsumv 12169 . . . . . . . . . . . 12  |-  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 ) ) ) )
25756a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  ->  -u 1  e.  CC )
258147sseli 3176 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ~P y  -> 
s  e.  ~P (
y  u.  { z } ) )
259258, 164sylan2 460 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
( -u 1 ^ ( # `
 s ) )  e.  CC )
260257, 259mulcomd 8856 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) )
261259mulm1d 9231 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
( -u 1  x.  ( -u 1 ^ ( # `  s ) ) )  =  -u ( -u 1 ^ ( # `  s
) ) )
262261eqcomd 2288 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  ->  -u ( -u 1 ^ ( # `  s
) )  =  (
-u 1  x.  ( -u 1 ^ ( # `  s ) ) ) )
263 elpwi 3633 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  ~P y  -> 
s  C_  y )
264 ssfi 7083 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  Fin  /\  s  C_  y )  -> 
s  e.  Fin )
265152, 263, 264syl2an 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
s  e.  Fin )
266 simpllr 735 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  ->  -.  z  e.  y
)
267263adantl 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
s  C_  y )
268267sseld 3179 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
( z  e.  s  ->  z  e.  y ) )
269266, 268mtod 168 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  ->  -.  z  e.  s
)
270 hashunsng 11367 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  _V  ->  (
( s  e.  Fin  /\ 
-.  z  e.  s )  ->  ( # `  (
s  u.  { z } ) )  =  ( ( # `  s
)  +  1 ) ) )
27127, 270ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s  e.  Fin  /\  -.  z  e.  s
)  ->  ( # `  (
s  u.  { z } ) )  =  ( ( # `  s
)  +  1 ) )
272265, 269, 271syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
( # `  ( s  u.  { z } ) )  =  ( ( # `  s
)  +  1 ) )
273272oveq2d 5874 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
( -u 1 ^ ( # `
 ( s  u. 
{ z } ) ) )  =  (
-u 1 ^ (
( # `  s )  +  1 ) ) )
274265, 162syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
( # `  s )  e.  NN0 )
275257, 274expp1d 11246 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
( -u 1 ^ (
( # `  s )  +  1 ) )  =  ( ( -u
1 ^ ( # `  s ) )  x.  -u 1 ) )
276273, 275eqtrd 2315 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
( -u 1 ^ ( # `
 ( s  u. 
{ z } ) ) )  =  ( ( -u 1 ^ ( # `  s
) )  x.  -u 1
) )
277260, 262, 2763eqtr4rd 2326 . . . . . . . . . . . . . . 15  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
( -u 1 ^ ( # `
 ( s  u. 
{ z } ) ) )  =  -u ( -u 1 ^ ( # `
 s ) ) )
278277oveq1d 5873 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) ) ) )
279 inss1 3389 . . . . . . . . . . . . . . . . . . 19  |-  ( x  i^i  ( |^| s  i^i  z ) )  C_  x
280 ssfi 7083 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  Fin  /\  ( x  i^i  ( |^| s  i^i  z
) )  C_  x
)  ->  ( x  i^i  ( |^| s  i^i  z ) )  e. 
Fin )
281165, 279, 280sylancl 643 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P ( y  u. 
{ z } ) )  ->  ( x  i^i  ( |^| s  i^i  z ) )  e. 
Fin )
282 hashcl 11350 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  i^i  ( |^| s  i^i  z ) )  e.  Fin  ->  ( # `
 ( x  i^i  ( |^| s  i^i  z ) ) )  e.  NN0 )
283281, 282syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P ( y  u. 
{ z } ) )  ->  ( # `  (
x  i^i  ( |^| s  i^i  z ) ) )  e.  NN0 )
284283nn0cnd 10020 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P ( y  u. 
{ z } ) )  ->  ( # `  (
x  i^i  ( |^| s  i^i  z ) ) )  e.  CC )
285258, 284sylan2 460 . . . . . . . . . . . . . . 15  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
( # `  ( x  i^i  ( |^| s  i^i  z ) ) )  e.  CC )
286259, 285mulneg1d 9232 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) ) ) )
287278, 286eqtrd 2315 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) ) ) ) )
288287sumeq2dv 12176 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) ) )
289256, 288syl5eq 2327 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) ) )
290164, 284mulcld 8855 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
291258, 290sylan2 460 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
292183, 291fsumneg 12249 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) ) )
293247, 289, 2923eqtrd 2319 . . . . . . . . . 10  |-  ( ( ( 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 ) ) ) ) )
294293oveq2d 5874 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) ) ) )
295147a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ~P y  C_  ~P ( y  u.  { z } ) )
296295sselda 3180 . . . . . . . . . . . 12  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
s  e.  ~P (
y  u.  { z } ) )
297296, 172syldan 456 . . . . . . . . . . 11  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
( ( -u 1 ^ ( # `  s
) )  x.  ( # `
 ( x  i^i  |^| s ) ) )  e.  CC )
298183, 297fsumcl 12206 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  sum_ s  e.  ~P  y ( (
-u 1 ^ ( # `
 s ) )  x.  ( # `  (
x  i^i  |^| s ) ) )  e.  CC )
299296, 290syldan 456 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
300183, 299fsumcl 12206 . . . . . . . . . 10  |-  ( ( ( 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 )
301298, 300negsubd 9163 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) ) ) )
302173, 294, 3013eqtrd 2319 . . . . . . . 8  |-  ( ( ( 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 ) ) ) ) ) )
303302adantr 451 . . . . . . 7  |-  ( ( ( ( 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 ) ) ) ) ) )
304109, 142, 3033eqtr4d 2325 . . . . . 6  |-  ( ( ( ( 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 ) ) ) )
305304ex 423 . . . . 5  |-  ( ( ( 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 ) ) ) ) )
306305ralrimdva 2633 . . . 4  |-  ( ( 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 ) ) ) ) )
307 ineq1 3363 . . . . . . . 8  |-  ( b  =  x  ->  (
b  i^i  ( U. y  u.  z )
)  =  ( x  i^i  ( U. y  u.  z ) ) )
308307fveq2d 5529 . . . . . . 7  |-  ( b  =  x  ->  ( # `
 ( b  i^i  ( U. y  u.  z ) ) )  =  ( # `  (
x  i^i  ( U. y  u.  z )
) ) )
30974, 308oveq12d 5876 . . . . . 6  |-  ( b  =  x  ->  (
( # `  b )  -  ( # `  (
b  i^i  ( U. y  u.  z )
) ) )  =  ( ( # `  x
)  -  ( # `  ( x  i^i  ( U. y  u.  z
) ) ) ) )
310 ineq1 3363 . . . . . . . . 9  |-  ( b  =  x  ->  (
b  i^i  |^| s )  =  ( x  i^i  |^| s ) )
311310fveq2d 5529 . . . . . . . 8  |-  ( b  =  x  ->  ( # `
 ( b  i^i  |^| s ) )  =  ( # `  (
x  i^i  |^| s ) ) )
312311oveq2d 5874 . . . . . . 7  |-  ( b  =  x  ->  (
( -u 1 ^ ( # `
 s ) )  x.  ( # `  (
b  i^i  |^| s ) ) )  =  ( ( -u 1 ^ ( # `  s
) )  x.  ( # `
 ( x  i^i  |^| s ) ) ) )
313312sumeq2sdv 12177 . . . . . 6  |-  ( 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 ) ) ) )
314309, 313eqeq12d 2297 . . . . 5  |-  ( 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 ) ) ) ) )
315314cbvralv 2764 . . . 4  |-  ( 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 ) ) ) )
316306, 315syl6ibr 218 . . 3  |-  ( ( 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 ) ) ) ) )
31716, 24, 38, 46, 73, 316findcard2s 7099 . 2  |-  ( 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 ) ) ) )
318 fveq2 5525 . . . . 5  |-  ( b  =  B  ->  ( # `
 b )  =  ( # `  B
) )
319 ineq1 3363 . . . . . 6  |-  ( b  =  B  ->  (
b  i^i  U. A )  =  ( B  i^i  U. A ) )
320319fveq2d 5529 . . . . 5  |-  ( b  =  B  ->  ( # `
 ( b  i^i  U. A ) )  =  ( # `  ( B  i^i  U. A ) ) )
321318, 320oveq12d 5876 . . . 4  |-  ( b  =  B  ->  (
( # `  b )  -  ( # `  (
b  i^i  U. A ) ) )  =  ( ( # `  B
)  -  ( # `  ( B  i^i  U. A ) ) ) )
322 simpl 443 . . . . . . . 8  |-  ( ( b  =  B  /\  s  e.  ~P A
)  ->  b  =  B )
323322ineq1d 3369 . . . . . . 7  |-  ( ( b  =  B  /\  s  e.  ~P A
)  ->  ( b  i^i  |^| s )  =  ( B  i^i  |^| s ) )
324323fveq2d 5529 . . . . . 6  |-  ( ( b  =  B  /\  s  e.  ~P A
)  ->  ( # `  (
b  i^i  |^| s ) )  =  ( # `  ( B  i^i  |^| s ) ) )
325324oveq2d 5874 . . . . 5  |-  ( ( b  =  B  /\  s  e.  ~P A
)  ->  ( ( -u 1 ^ ( # `  s ) )  x.  ( # `  (
b  i^i  |^| s ) ) )  =  ( ( -u 1 ^ ( # `  s
) )  x.  ( # `
 ( B  i^i  |^| s ) ) ) )
326325sumeq2dv 12176 . . . 4  |-  ( 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 ) ) ) )
327321, 326eqeq12d 2297 . . 3  |-  ( 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 ) ) ) ) )
328327rspccva 2883 . 2  |-  ( ( 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 ) ) ) )
329317, 328sylan 457 1  |-  ( ( 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 ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684   A.wral 2543   _Vcvv 2788    \ cdif 3149    u. cun 3150    i^i cin 3151    C_ wss 3152   (/)c0 3455   ~Pcpw 3625   {csn 3640   U.cuni 3827   |^|cint 3862    e. cmpt 4077   ` cfv 5255  (class class class)co 5858   Fincfn 6863   CCcc 8735   0cc0 8737   1c1 8738    + caddc 8740    x. cmul 8742    - cmin 9037   -ucneg 9038   NN0cn0 9965   ^cexp 11104   #chash 11337   sum_csu 12158
This theorem is referenced by:  incexc  12296
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-inf2 7342  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814  ax-pre-sup 8815
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-se 4353  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-isom 5264  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-1o 6479  df-2o 6480  df-oadd 6483  df-er 6660  df-map 6774  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-sup 7194  df-oi 7225  df-card 7572  df-cda 7794  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-div 9424  df-nn 9747  df-2 9804  df-3 9805  df-n0 9966  df-z 10025  df-uz 10231  df-rp 10355  df-fz 10783  df-fzo 10871  df-seq 11047  df-exp 11105  df-hash 11338  df-cj 11584  df-re 11585  df-im 11586  df-sqr 11720  df-abs 11721  df-clim 11962  df-sum 12159
  Copyright terms: Public domain W3C validator