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

Theorem incexclem 12342
Description: Lemma for incexc 12343. (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 3873 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  U. x  =  U. (/) )
2 uni0 3891 . . . . . . . . . . 11  |-  U. (/)  =  (/)
31, 2syl6eq 2364 . . . . . . . . . 10  |-  ( x  =  (/)  ->  U. x  =  (/) )
43ineq2d 3404 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( b  i^i  U. x )  =  ( b  i^i  (/) ) )
5 in0 3514 . . . . . . . . 9  |-  ( b  i^i  (/) )  =  (/)
64, 5syl6eq 2364 . . . . . . . 8  |-  ( x  =  (/)  ->  ( b  i^i  U. x )  =  (/) )
76fveq2d 5567 . . . . . . 7  |-  ( x  =  (/)  ->  ( # `  ( b  i^i  U. x ) )  =  ( # `  (/) ) )
8 hash0 11402 . . . . . . 7  |-  ( # `  (/) )  =  0
97, 8syl6eq 2364 . . . . . 6  |-  ( x  =  (/)  ->  ( # `  ( b  i^i  U. x ) )  =  0 )
109oveq2d 5916 . . . . 5  |-  ( x  =  (/)  ->  ( (
# `  b )  -  ( # `  (
b  i^i  U. x
) ) )  =  ( ( # `  b
)  -  0 ) )
11 pweq 3662 . . . . . . 7  |-  ( x  =  (/)  ->  ~P x  =  ~P (/) )
12 pw0 3799 . . . . . . 7  |-  ~P (/)  =  { (/)
}
1311, 12syl6eq 2364 . . . . . 6  |-  ( x  =  (/)  ->  ~P x  =  { (/) } )
1413sumeq1d 12221 . . . . 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 2330 . . . 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 2597 . . 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 3873 . . . . . . . 8  |-  ( x  =  y  ->  U. x  =  U. y )
1817ineq2d 3404 . . . . . . 7  |-  ( x  =  y  ->  (
b  i^i  U. x
)  =  ( b  i^i  U. y ) )
1918fveq2d 5567 . . . . . 6  |-  ( x  =  y  ->  ( # `
 ( b  i^i  U. x ) )  =  ( # `  (
b  i^i  U. y
) ) )
2019oveq2d 5916 . . . . 5  |-  ( x  =  y  ->  (
( # `  b )  -  ( # `  (
b  i^i  U. x
) ) )  =  ( ( # `  b
)  -  ( # `  ( b  i^i  U. y ) ) ) )
21 pweq 3662 . . . . . 6  |-  ( x  =  y  ->  ~P x  =  ~P y
)
2221sumeq1d 12221 . . . . 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 2330 . . . 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 2597 . . 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 3873 . . . . . . . . 9  |-  ( x  =  ( y  u. 
{ z } )  ->  U. x  =  U. ( y  u.  {
z } ) )
26 uniun 3883 . . . . . . . . . 10  |-  U. (
y  u.  { z } )  =  ( U. y  u.  U. { z } )
27 vex 2825 . . . . . . . . . . . 12  |-  z  e. 
_V
2827unisn 3880 . . . . . . . . . . 11  |-  U. {
z }  =  z
2928uneq2i 3360 . . . . . . . . . 10  |-  ( U. y  u.  U. { z } )  =  ( U. y  u.  z
)
3026, 29eqtri 2336 . . . . . . . . 9  |-  U. (
y  u.  { z } )  =  ( U. y  u.  z
)
3125, 30syl6eq 2364 . . . . . . . 8  |-  ( x  =  ( y  u. 
{ z } )  ->  U. x  =  ( U. y  u.  z
) )
3231ineq2d 3404 . . . . . . 7  |-  ( x  =  ( y  u. 
{ z } )  ->  ( b  i^i  U. x )  =  ( b  i^i  ( U. y  u.  z )
) )
3332fveq2d 5567 . . . . . 6  |-  ( x  =  ( y  u. 
{ z } )  ->  ( # `  (
b  i^i  U. x
) )  =  (
# `  ( b  i^i  ( U. y  u.  z ) ) ) )
3433oveq2d 5916 . . . . 5  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ( # `  b )  -  ( # `
 ( b  i^i  U. x ) ) )  =  ( ( # `  b )  -  ( # `
 ( b  i^i  ( U. y  u.  z ) ) ) ) )
35 pweq 3662 . . . . . 6  |-  ( x  =  ( y  u. 
{ z } )  ->  ~P x  =  ~P ( y  u. 
{ z } ) )
3635sumeq1d 12221 . . . . 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 2330 . . . 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 2597 . . 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 3873 . . . . . . . 8  |-  ( x  =  A  ->  U. x  =  U. A )
4039ineq2d 3404 . . . . . . 7  |-  ( x  =  A  ->  (
b  i^i  U. x
)  =  ( b  i^i  U. A ) )
4140fveq2d 5567 . . . . . 6  |-  ( x  =  A  ->  ( # `
 ( b  i^i  U. x ) )  =  ( # `  (
b  i^i  U. A ) ) )
4241oveq2d 5916 . . . . 5  |-  ( x  =  A  ->  (
( # `  b )  -  ( # `  (
b  i^i  U. x
) ) )  =  ( ( # `  b
)  -  ( # `  ( b  i^i  U. A ) ) ) )
43 pweq 3662 . . . . . 6  |-  ( x  =  A  ->  ~P x  =  ~P A
)
4443sumeq1d 12221 . . . . 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 2330 . . . 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 2597 . . 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 11397 . . . . . . 7  |-  ( b  e.  Fin  ->  ( # `
 b )  e. 
NN0 )
4847nn0cnd 10067 . . . . . 6  |-  ( b  e.  Fin  ->  ( # `
 b )  e.  CC )
4948mulid2d 8898 . . . . 5  |-  ( b  e.  Fin  ->  (
1  x.  ( # `  b ) )  =  ( # `  b
) )
50 0ex 4187 . . . . . . 7  |-  (/)  e.  _V
5150a1i 10 . . . . . 6  |-  ( b  e.  Fin  ->  (/)  e.  _V )
5249, 48eqeltrd 2390 . . . . . 6  |-  ( b  e.  Fin  ->  (
1  x.  ( # `  b ) )  e.  CC )
53 fveq2 5563 . . . . . . . . . . 11  |-  ( s  =  (/)  ->  ( # `  s )  =  (
# `  (/) ) )
5453, 8syl6eq 2364 . . . . . . . . . 10  |-  ( s  =  (/)  ->  ( # `  s )  =  0 )
5554oveq2d 5916 . . . . . . . . 9  |-  ( s  =  (/)  ->  ( -u
1 ^ ( # `  s ) )  =  ( -u 1 ^ 0 ) )
56 neg1cn 9858 . . . . . . . . . 10  |-  -u 1  e.  CC
57 exp0 11155 . . . . . . . . . 10  |-  ( -u
1  e.  CC  ->  (
-u 1 ^ 0 )  =  1 )
5856, 57ax-mp 8 . . . . . . . . 9  |-  ( -u
1 ^ 0 )  =  1
5955, 58syl6eq 2364 . . . . . . . 8  |-  ( s  =  (/)  ->  ( -u
1 ^ ( # `  s ) )  =  1 )
60 ssv 3232 . . . . . . . . . . 11  |-  b  C_  _V
61 inteq 3902 . . . . . . . . . . . 12  |-  ( s  =  (/)  ->  |^| s  =  |^| (/) )
62 int0 3913 . . . . . . . . . . . 12  |-  |^| (/)  =  _V
6361, 62syl6eq 2364 . . . . . . . . . . 11  |-  ( s  =  (/)  ->  |^| s  =  _V )
6460, 63syl5sseqr 3261 . . . . . . . . . 10  |-  ( s  =  (/)  ->  b  C_  |^| s )
65 df-ss 3200 . . . . . . . . . 10  |-  ( b 
C_  |^| s  <->  ( b  i^i  |^| s )  =  b )
6664, 65sylib 188 . . . . . . . . 9  |-  ( s  =  (/)  ->  ( b  i^i  |^| s )  =  b )
6766fveq2d 5567 . . . . . . . 8  |-  ( s  =  (/)  ->  ( # `  ( b  i^i  |^| s ) )  =  ( # `  b
) )
6859, 67oveq12d 5918 . . . . . . 7  |-  ( s  =  (/)  ->  ( (
-u 1 ^ ( # `
 s ) )  x.  ( # `  (
b  i^i  |^| s ) ) )  =  ( 1  x.  ( # `  b ) ) )
6968sumsn 12260 . . . . . 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 9191 . . . . 5  |-  ( b  e.  Fin  ->  (
( # `  b )  -  0 )  =  ( # `  b
) )
7249, 70, 713eqtr4rd 2359 . . . 4  |-  ( b  e.  Fin  ->  (
( # `  b )  -  0 )  = 
sum_ s  e.  { (/)
}  ( ( -u
1 ^ ( # `  s ) )  x.  ( # `  (
b  i^i  |^| s ) ) ) )
7372rgen 2642 . . 3  |-  A. b  e.  Fin  ( ( # `  b )  -  0 )  =  sum_ s  e.  { (/) }  ( (
-u 1 ^ ( # `
 s ) )  x.  ( # `  (
b  i^i  |^| s ) ) )
74 fveq2 5563 . . . . . . . . . . . 12  |-  ( b  =  x  ->  ( # `
 b )  =  ( # `  x
) )
75 ineq1 3397 . . . . . . . . . . . . 13  |-  ( b  =  x  ->  (
b  i^i  U. y
)  =  ( x  i^i  U. y ) )
7675fveq2d 5567 . . . . . . . . . . . 12  |-  ( b  =  x  ->  ( # `
 ( b  i^i  U. y ) )  =  ( # `  (
x  i^i  U. y
) ) )
7774, 76oveq12d 5918 . . . . . . . . . . 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 3403 . . . . . . . . . . . . . 14  |-  ( ( b  =  x  /\  s  e.  ~P y
)  ->  ( b  i^i  |^| s )  =  ( x  i^i  |^| s ) )
8079fveq2d 5567 . . . . . . . . . . . . 13  |-  ( ( b  =  x  /\  s  e.  ~P y
)  ->  ( # `  (
b  i^i  |^| s ) )  =  ( # `  ( x  i^i  |^| s ) ) )
8180oveq2d 5916 . . . . . . . . . . . 12  |-  ( ( b  =  x  /\  s  e.  ~P y
)  ->  ( ( -u 1 ^ ( # `  s ) )  x.  ( # `  (
b  i^i  |^| s ) ) )  =  ( ( -u 1 ^ ( # `  s
) )  x.  ( # `
 ( x  i^i  |^| s ) ) ) )
8281sumeq2dv 12223 . . . . . . . . . . 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 2330 . . . . . . . . . 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 2916 . . . . . . . . 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 3423 . . . . . . . . . 10  |-  ( x  i^i  z )  C_  x
88 ssfi 7126 . . . . . . . . . 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 5563 . . . . . . . . . . . 12  |-  ( b  =  ( x  i^i  z )  ->  ( # `
 b )  =  ( # `  (
x  i^i  z )
) )
91 ineq1 3397 . . . . . . . . . . . . . 14  |-  ( b  =  ( x  i^i  z )  ->  (
b  i^i  U. y
)  =  ( ( x  i^i  z )  i^i  U. y ) )
92 in32 3415 . . . . . . . . . . . . . . 15  |-  ( ( x  i^i  z )  i^i  U. y )  =  ( ( x  i^i  U. y )  i^i  z )
93 inass 3413 . . . . . . . . . . . . . . 15  |-  ( ( x  i^i  U. y
)  i^i  z )  =  ( x  i^i  ( U. y  i^i  z ) )
9492, 93eqtri 2336 . . . . . . . . . . . . . 14  |-  ( ( x  i^i  z )  i^i  U. y )  =  ( x  i^i  ( U. y  i^i  z ) )
9591, 94syl6eq 2364 . . . . . . . . . . . . 13  |-  ( b  =  ( x  i^i  z )  ->  (
b  i^i  U. y
)  =  ( x  i^i  ( U. y  i^i  z ) ) )
9695fveq2d 5567 . . . . . . . . . . . 12  |-  ( b  =  ( x  i^i  z )  ->  ( # `
 ( b  i^i  U. y ) )  =  ( # `  (
x  i^i  ( U. y  i^i  z ) ) ) )
9790, 96oveq12d 5918 . . . . . . . . . . 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 3397 . . . . . . . . . . . . . . 15  |-  ( b  =  ( x  i^i  z )  ->  (
b  i^i  |^| s )  =  ( ( x  i^i  z )  i^i  |^| s ) )
99 in32 3415 . . . . . . . . . . . . . . . 16  |-  ( ( x  i^i  z )  i^i  |^| s )  =  ( ( x  i^i  |^| s )  i^i  z
)
100 inass 3413 . . . . . . . . . . . . . . . 16  |-  ( ( x  i^i  |^| s
)  i^i  z )  =  ( x  i^i  ( |^| s  i^i  z ) )
10199, 100eqtri 2336 . . . . . . . . . . . . . . 15  |-  ( ( x  i^i  z )  i^i  |^| s )  =  ( x  i^i  ( |^| s  i^i  z
) )
10298, 101syl6eq 2364 . . . . . . . . . . . . . 14  |-  ( b  =  ( x  i^i  z )  ->  (
b  i^i  |^| s )  =  ( x  i^i  ( |^| s  i^i  z ) ) )
103102fveq2d 5567 . . . . . . . . . . . . 13  |-  ( b  =  ( x  i^i  z )  ->  ( # `
 ( b  i^i  |^| s ) )  =  ( # `  (
x  i^i  ( |^| s  i^i  z ) ) ) )
104103oveq2d 5916 . . . . . . . . . . . 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 12224 . . . . . . . . . . 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 2330 . . . . . . . . . 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 2916 . . . . . . . . 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 5918 . . . . . . 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 3423 . . . . . . . . . . . . . 14  |-  ( x  i^i  U. y ) 
C_  x
111 ssfi 7126 . . . . . . . . . . . . . 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 11413 . . . . . . . . . . . . 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 3449 . . . . . . . . . . . . 13  |-  ( x  i^i  ( U. y  u.  z ) )  =  ( ( x  i^i  U. y )  u.  (
x  i^i  z )
)
116115fveq2i 5566 . . . . . . . . . . . 12  |-  ( # `  ( x  i^i  ( U. y  u.  z
) ) )  =  ( # `  (
( x  i^i  U. y )  u.  (
x  i^i  z )
) )
117 inindi 3420 . . . . . . . . . . . . . 14  |-  ( x  i^i  ( U. y  i^i  z ) )  =  ( ( x  i^i  U. y )  i^i  (
x  i^i  z )
)
118117fveq2i 5566 . . . . . . . . . . . . 13  |-  ( # `  ( x  i^i  ( U. y  i^i  z
) ) )  =  ( # `  (
( x  i^i  U. y )  i^i  (
x  i^i  z )
) )
119118oveq2i 5911 . . . . . . . . . . . 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 2373 . . . . . . . . . . 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 11397 . . . . . . . . . . . . . 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 10067 . . . . . . . . . . . 12  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ( # `
 ( x  i^i  U. y ) )  e.  CC )
124 hashcl 11397 . . . . . . . . . . . . . 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 10067 . . . . . . . . . . . 12  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ( # `
 ( x  i^i  z ) )  e.  CC )
127 inss1 3423 . . . . . . . . . . . . . . 15  |-  ( x  i^i  ( U. y  i^i  z ) )  C_  x
128 ssfi 7126 . . . . . . . . . . . . . . 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 11397 . . . . . . . . . . . . . 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 10067 . . . . . . . . . . . 12  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ( # `
 ( x  i^i  ( U. y  i^i  z ) ) )  e.  CC )
133123, 126, 132addsubassd 9222 . . . . . . . . . . 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 2348 . . . . . . . . . 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 5916 . . . . . . . . 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 11397 . . . . . . . . . . . 12  |-  ( x  e.  Fin  ->  ( # `
 x )  e. 
NN0 )
137136adantl 452 . . . . . . . . . . 11  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ( # `
 x )  e. 
NN0 )
138137nn0cnd 10067 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  x  e. 
Fin )  ->  ( # `
 x )  e.  CC )
139126, 132subcld 9202 . . . . . . . . . 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 9233 . . . . . . . . 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 2351 . . . . . . . 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 3560 . . . . . . . . . . 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 3372 . . . . . . . . . . . . . 14  |-  y  C_  ( y  u.  {
z } )
146 sspwb 4260 . . . . . . . . . . . . . 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 3568 . . . . . . . . . . . . 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 2320 . . . . . . . . . . 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 6984 . . . . . . . . . . . 12  |-  { z }  e.  Fin
154 unfi 7169 . . . . . . . . . . . 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 7196 . . . . . . . . . . 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 3667 . . . . . . . . . . . . . 14  |-  ( s  e.  ~P ( y  u.  { z } )  ->  s  C_  ( y  u.  {
z } ) )
160 ssfi 7126 . . . . . . . . . . . . . 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 11397 . . . . . . . . . . . . 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 11292 . . . . . . . . . . 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 3423 . . . . . . . . . . . . . 14  |-  ( x  i^i  |^| s )  C_  x
167 ssfi 7126 . . . . . . . . . . . . . 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 11397 . . . . . . . . . . . . 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 10067 . . . . . . . . . . 11  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P ( y  u. 
{ z } ) )  ->  ( # `  (
x  i^i  |^| s ) )  e.  CC )
172164, 171mulcld 8900 . . . . . . . . . 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 12259 . . . . . . . . 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 5563 . . . . . . . . . . . . . 14  |-  ( s  =  ( t  u. 
{ z } )  ->  ( # `  s
)  =  ( # `  ( t  u.  {
z } ) ) )
175174oveq2d 5916 . . . . . . . . . . . . 13  |-  ( s  =  ( t  u. 
{ z } )  ->  ( -u 1 ^ ( # `  s
) )  =  (
-u 1 ^ ( # `
 ( t  u. 
{ z } ) ) ) )
176 inteq 3902 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( t  u. 
{ z } )  ->  |^| s  =  |^| ( t  u.  {
z } ) )
17727intunsn 3938 . . . . . . . . . . . . . . . 16  |-  |^| (
t  u.  { z } )  =  (
|^| t  i^i  z
)
178176, 177syl6eq 2364 . . . . . . . . . . . . . . 15  |-  ( s  =  ( t  u. 
{ z } )  ->  |^| s  =  (
|^| t  i^i  z
) )
179178ineq2d 3404 . . . . . . . . . . . . . 14  |-  ( s  =  ( t  u. 
{ z } )  ->  ( x  i^i  |^| s )  =  ( x  i^i  ( |^| t  i^i  z ) ) )
180179fveq2d 5567 . . . . . . . . . . . . 13  |-  ( s  =  ( t  u. 
{ z } )  ->  ( # `  (
x  i^i  |^| s ) )  =  ( # `  ( x  i^i  ( |^| t  i^i  z
) ) ) )
181175, 180oveq12d 5918 . . . . . . . . . . . 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 7196 . . . . . . . . . . . . 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 2316 . . . . . . . . . . . . 13  |-  ( u  e.  ~P y  |->  ( u  u.  { z } ) )  =  ( u  e.  ~P y  |->  ( u  u. 
{ z } ) )
185 elpwi 3667 . . . . . . . . . . . . . . . . 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 3378 . . . . . . . . . . . . . . . 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 2825 . . . . . . . . . . . . . . . . 17  |-  u  e. 
_V
190 snex 4253 . . . . . . . . . . . . . . . . 17  |-  { z }  e.  _V
191189, 190unex 4555 . . . . . . . . . . . . . . . 16  |-  ( u  u.  { z } )  e.  _V
192191elpw 3665 . . . . . . . . . . . . . . 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 3667 . . . . . . . . . . . . . . . 16  |-  ( ( u  u.  { z } )  e.  ~P y  ->  ( u  u. 
{ z } ) 
C_  y )
196 ssun2 3373 . . . . . . . . . . . . . . . . . . 19  |-  { z }  C_  ( u  u.  { z } )
19727snss 3782 . . . . . . . . . . . . . . . . . . 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 3208 . . . . . . . . . . . . . . . . 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 3197 . . . . . . . . . . . . 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 3332 . . . . . . . . . . . . . . . . . 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 3668 . . . . . . . . . . . . . . . 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 3353 . . . . . . . . . . . . . . . 16  |-  ( y  u.  { z } )  =  ( { z }  u.  y
)
209207, 208syl6sseq 3258 . . . . . . . . . . . . . . 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 3571 . . . . . . . . . . . . . . 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 2825 . . . . . . . . . . . . . . 15  |-  y  e. 
_V
213212elpw2 4212 . . . . . . . . . . . . . 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 4605 . . . . . . . . . . . . . . . . . . 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 3796 . . . . . . . . . . . . . . . . . 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 3382 . . . . . . . . . . . . . . . . 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 2321 . . . . . . . . . . . . . . 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 3356 . . . . . . . . . . . . . . . . 17  |-  ( u  =  ( s  \  { z } )  ->  ( u  u. 
{ z } )  =  ( ( s 
\  { z } )  u.  { z } ) )
223 undif1 3563 . . . . . . . . . . . . . . . . 17  |-  ( ( s  \  { z } )  u.  {
z } )  =  ( s  u.  {
z } )
224222, 223syl6eq 2364 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( s  \  { z } )  ->  ( u  u. 
{ z } )  =  ( s  u. 
{ z } ) )
225224eqeq2d 2327 . . . . . . . . . . . . . . 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 3213 . . . . . . . . . . . . . . . . . 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 difsnb 3794 . . . . . . . . . . . . . . . . 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 2321 . . . . . . . . . . . . . . 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 3321 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( u  u. 
{ z } )  ->  ( s  \  { z } )  =  ( ( u  u.  { z } )  \  { z } ) )
235 difun2 3567 . . . . . . . . . . . . . . . . 17  |-  ( ( u  u.  { z } )  \  {
z } )  =  ( u  \  {
z } )
236234, 235syl6eq 2364 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( u  u. 
{ z } )  ->  ( s  \  { z } )  =  ( u  \  { z } ) )
237236eqeq2d 2327 . . . . . . . . . . . . . . 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 6111 . . . . . . . . . . . 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 3356 . . . . . . . . . . . . . 14  |-  ( u  =  t  ->  (
u  u.  { z } )  =  ( t  u.  { z } ) )
242 vex 2825 . . . . . . . . . . . . . . 15  |-  t  e. 
_V
243242, 190unex 4555 . . . . . . . . . . . . . 14  |-  ( t  u.  { z } )  e.  _V
244241, 184, 243fvmpt 5640 . . . . . . . . . . . . 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 12243 . . . . . . . . . . 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 3356 . . . . . . . . . . . . . . . 16  |-  ( t  =  s  ->  (
t  u.  { z } )  =  ( s  u.  { z } ) )
249248fveq2d 5567 . . . . . . . . . . . . . . 15  |-  ( t  =  s  ->  ( # `
 ( t  u. 
{ z } ) )  =  ( # `  ( s  u.  {
z } ) ) )
250249oveq2d 5916 . . . . . . . . . . . . . 14  |-  ( t  =  s  ->  ( -u 1 ^ ( # `  ( t  u.  {
z } ) ) )  =  ( -u
1 ^ ( # `  ( s  u.  {
z } ) ) ) )
251 inteq 3902 . . . . . . . . . . . . . . . . 17  |-  ( t  =  s  ->  |^| t  =  |^| s )
252251ineq1d 3403 . . . . . . . . . . . . . . . 16  |-  ( t  =  s  ->  ( |^| t  i^i  z
)  =  ( |^| s  i^i  z ) )
253252ineq2d 3404 . . . . . . . . . . . . . . 15  |-  ( t  =  s  ->  (
x  i^i  ( |^| t  i^i  z ) )  =  ( x  i^i  ( |^| s  i^i  z ) ) )
254253fveq2d 5567 . . . . . . . . . . . . . 14  |-  ( t  =  s  ->  ( # `
 ( x  i^i  ( |^| t  i^i  z ) ) )  =  ( # `  (
x  i^i  ( |^| s  i^i  z ) ) ) )
255250, 254oveq12d 5918 . . . . . . . . . . . . 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 12216 . . . . . . . . . . . 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 3210 . . . . . . . . . . . . . . . . . 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 8901 . . . . . . . . . . . . . . . 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 9276 . . . . . . . . . . . . . . . . 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 2321 . . . . . . . . . . . . . . . 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 3667 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  ~P y  -> 
s  C_  y )
264 ssfi 7126 . . . . . . . . . . . . . . . . . . . 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 3213 . . . . . . . . . . . . . . . . . . . 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 11414 . . . . . . . . . . . . . . . . . . . 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 5916 . . . . . . . . . . . . . . . . 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 11293 . . . . . . . . . . . . . . . . 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 2348 . . . . . . . . . . . . . . . 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 2359 . . . . . . . . . . . . . . 15  |-  ( ( ( ( y  e. 
Fin  /\  -.  z  e.  y )  /\  x  e.  Fin )  /\  s  e.  ~P y )  -> 
( -u 1 ^ ( # `
 ( s  u. 
{ z } ) ) )  =  -u ( -u 1 ^ ( # `
 s ) ) )
278277oveq1d 5915 . . . . . . . . . . . . . 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 3423 . . . . . . . . . . . . . . . . . . 19  |-  ( x  i^i  ( |^| s  i^i  z ) )  C_  x
280 ssfi 7126 . . . . . . . . . . . . . . . . . . 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 11397 . . . . . . . . . . . . . . . . . 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 10067 . . . . . . . . . . . . . . . 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 9277 . . . . . . . . . . . . . 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 2348 . . . . . . . . . . . . 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 12223 . . . . . . . . . . . 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 2360 . . . . . . . . . . 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 8900 . . . . . . . . . . . . 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 12296 . . . . . . . . . . 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 2352 . . . . . . . . . 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 5916 . . . . . . . . 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 3214 . . . . . . . . . . . 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 12253 . . . . . . . . . 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 12253 . . . . . . . . . 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 9208 . . . . . . . . 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 2352 . . . . . . . 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 2358 . . . . . 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 2667 . . . 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 3397 . . . . . . . 8  |-  ( b  =  x  ->  (
b  i^i  ( U. y  u.  z )
)  =  ( x  i^i  ( U. y  u.  z ) ) )
308307fveq2d 5567 . . . . . . 7  |-  ( b  =  x  ->  ( # `
 ( b  i^i  ( U. y  u.  z ) ) )  =  ( # `  (
x  i^i  ( U. y  u.  z )
) ) )
30974, 308oveq12d 5918 . . . . . 6  |-  ( b  =  x  ->  (
( # `  b )  -  ( # `  (
b  i^i  ( U. y  u.  z )
) ) )  =  ( ( # `  x
)  -  ( # `  ( x  i^i  ( U. y  u.  z
) ) ) ) )
310 ineq1 3397 . . . . . . . . 9  |-  ( b  =  x  ->  (
b  i^i  |^| s )  =  ( x  i^i  |^| s ) )
311310fveq2d 5567 . . . . . . . 8  |-  ( b  =  x  ->  ( # `
 ( b  i^i  |^| s ) )  =  ( # `  (
x  i^i  |^| s ) ) )
312311oveq2d 5916 . . . . . . 7  |-  ( b  =  x  ->  (
( -u 1 ^ ( # `
 s ) )  x.  ( # `  (
b  i^i  |^| s ) ) )  =  ( ( -u 1 ^ ( # `  s
) )  x.  ( # `
 ( x  i^i  |^| s ) ) ) )
313312sumeq2sdv 12224 . . . . . 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 2330 . . . . 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 2798 . . . 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 7144 . 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 5563 . . . . 5  |-  ( b  =  B  ->  ( # `
 b )  =  ( # `  B
) )
319 ineq1 3397 . . . . . 6  |-  ( b  =  B  ->  (
b  i^i  U. A )  =  ( B  i^i  U. A ) )
320319fveq2d 5567 . . . . 5  |-  ( b  =  B  ->  ( # `
 ( b  i^i  U. A ) )  =  ( # `  ( B  i^i  U. A ) ) )
321318, 320oveq12d 5918 . . . 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 3403 . . . . . . 7  |-  ( ( b  =  B  /\  s  e.  ~P A
)  ->  ( b  i^i  |^| s )  =  ( B  i^i  |^| s ) )
324323fveq2d 5567 . . . . . 6  |-  ( ( b  =  B  /\  s  e.  ~P A
)  ->  ( # `  (
b  i^i  |^| s ) )  =  ( # `  ( B  i^i  |^| s ) ) )
325324oveq2d 5916 . . . . 5  |-  ( ( b  =  B  /\  s  e.  ~P A
)  ->  ( ( -u 1 ^ ( # `  s ) )  x.  ( # `  (
b  i^i  |^| s ) ) )  =  ( ( -u 1 ^ ( # `  s
) )  x.  ( # `
 ( B  i^i  |^| s ) ) ) )
326325sumeq2dv 12223 . . . 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 2330 . . 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 2917 . 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 1633    e. wcel 1701   A.wral 2577   _Vcvv 2822    \ cdif 3183    u. cun 3184    i^i cin 3185    C_ wss 3186   (/)c0 3489   ~Pcpw 3659   {csn 3674   U.cuni 3864   |^|cint 3899    e. cmpt 4114   ` cfv 5292  (class class class)co 5900   Fincfn 6906   CCcc 8780   0cc0 8782   1c1 8783    + caddc 8785    x. cmul 8787    - cmin 9082   -ucneg 9083   NN0cn0 10012   ^cexp 11151   #chash 11384   sum_csu 12205
This theorem is referenced by:  incexc  12343
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-inf2 7387  ax-cnex 8838  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-mulcom 8846  ax-addass 8847  ax-mulass 8848  ax-distr 8849  ax-i2m1 8850  ax-1ne0 8851  ax-1rid 8852  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855  ax-pre-lttri 8856  ax-pre-lttrn 8857  ax-pre-ltadd 8858  ax-pre-mulgt0 8859  ax-pre-sup 8860
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 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rmo 2585  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-int 3900  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-se 4390  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-isom 5301  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-1st 6164  df-2nd 6165  df-riota 6346  df-recs 6430  df-rdg 6465  df-1o 6521  df-2o 6522  df-oadd 6525  df-er 6702  df-map 6817  df-en 6907  df-dom 6908  df-sdom 6909  df-fin 6910  df-sup 7239  df-oi 7270  df-card 7617  df-cda 7839  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-sub 9084  df-neg 9085  df-div 9469  df-nn 9792  df-2 9849  df-3 9850  df-n0 10013  df-z 10072  df-uz 10278  df-rp 10402  df-fz 10830  df-fzo 10918  df-seq 11094  df-exp 11152  df-hash 11385  df-cj 11631  df-re 11632  df-im 11633  df-sqr 11767  df-abs 11768  df-clim 12009  df-sum 12206
  Copyright terms: Public domain W3C validator