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

Theorem vdwlem6 13281
Description: Lemma for vdw 13289. (Contributed by Mario Carneiro, 13-Sep-2014.)
Hypotheses
Ref Expression
vdwlem3.v  |-  ( ph  ->  V  e.  NN )
vdwlem3.w  |-  ( ph  ->  W  e.  NN )
vdwlem4.r  |-  ( ph  ->  R  e.  Fin )
vdwlem4.h  |-  ( ph  ->  H : ( 1 ... ( W  x.  ( 2  x.  V
) ) ) --> R )
vdwlem4.f  |-  F  =  ( x  e.  ( 1 ... V ) 
|->  ( y  e.  ( 1 ... W ) 
|->  ( H `  (
y  +  ( W  x.  ( ( x  -  1 )  +  V ) ) ) ) ) )
vdwlem7.m  |-  ( ph  ->  M  e.  NN )
vdwlem7.g  |-  ( ph  ->  G : ( 1 ... W ) --> R )
vdwlem7.k  |-  ( ph  ->  K  e.  ( ZZ>= ` 
2 ) )
vdwlem7.a  |-  ( ph  ->  A  e.  NN )
vdwlem7.d  |-  ( ph  ->  D  e.  NN )
vdwlem7.s  |-  ( ph  ->  ( A (AP `  K ) D ) 
C_  ( `' F " { G } ) )
vdwlem6.b  |-  ( ph  ->  B  e.  NN )
vdwlem6.e  |-  ( ph  ->  E : ( 1 ... M ) --> NN )
vdwlem6.s  |-  ( ph  ->  A. i  e.  ( 1 ... M ) ( ( B  +  ( E `  i ) ) (AP `  K
) ( E `  i ) )  C_  ( `' G " { ( G `  ( B  +  ( E `  i ) ) ) } ) )
vdwlem6.j  |-  J  =  ( i  e.  ( 1 ... M ) 
|->  ( G `  ( B  +  ( E `  i ) ) ) )
vdwlem6.r  |-  ( ph  ->  ( # `  ran  J )  =  M )
vdwlem6.t  |-  T  =  ( B  +  ( W  x.  ( ( A  +  ( V  -  D ) )  -  1 ) ) )
vdwlem6.p  |-  P  =  ( j  e.  ( 1 ... ( M  +  1 ) ) 
|->  ( if ( j  =  ( M  + 
1 ) ,  0 ,  ( E `  j ) )  +  ( W  x.  D
) ) )
Assertion
Ref Expression
vdwlem6  |-  ( ph  ->  ( <. ( M  + 
1 ) ,  K >. PolyAP 
H  \/  ( K  +  1 ) MonoAP  G
) )
Distinct variable groups:    x, y, A    i, j, x, y, G    i, K, j, x, y    i, J, j, x    P, i, x    ph, i, j, x, y    R, i, x, y    B, i, j, x, y   
i, H, x, y   
i, M, j, x, y    D, j, x, y   
i, E, j, x, y    i, W, j, x, y    T, i, x    x, V, y
Allowed substitution hints:    A( i, j)    D( i)    P( y, j)    R( j)    T( y, j)    F( x, y, i, j)    H( j)    J( y)    V( i, j)

Proof of Theorem vdwlem6
Dummy variables  m  n  z  a  d are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 5682 . . . . . . 7  |-  ( G `
 ( B  +  ( E `  i ) ) )  e.  _V
2 vdwlem6.j . . . . . . 7  |-  J  =  ( i  e.  ( 1 ... M ) 
|->  ( G `  ( B  +  ( E `  i ) ) ) )
31, 2fnmpti 5513 . . . . . 6  |-  J  Fn  ( 1 ... M
)
4 fvelrnb 5713 . . . . . 6  |-  ( J  Fn  ( 1 ... M )  ->  (
( G `  B
)  e.  ran  J  <->  E. m  e.  ( 1 ... M ) ( J `  m )  =  ( G `  B ) ) )
53, 4ax-mp 8 . . . . 5  |-  ( ( G `  B )  e.  ran  J  <->  E. m  e.  ( 1 ... M
) ( J `  m )  =  ( G `  B ) )
6 vdwlem4.r . . . . . . . 8  |-  ( ph  ->  R  e.  Fin )
76adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  R  e.  Fin )
8 vdwlem7.k . . . . . . . . 9  |-  ( ph  ->  K  e.  ( ZZ>= ` 
2 ) )
9 eluz2b2 10480 . . . . . . . . . 10  |-  ( K  e.  ( ZZ>= `  2
)  <->  ( K  e.  NN  /\  1  < 
K ) )
109simplbi 447 . . . . . . . . 9  |-  ( K  e.  ( ZZ>= `  2
)  ->  K  e.  NN )
118, 10syl 16 . . . . . . . 8  |-  ( ph  ->  K  e.  NN )
1211adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  K  e.  NN )
13 vdwlem3.w . . . . . . . 8  |-  ( ph  ->  W  e.  NN )
1413adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  W  e.  NN )
15 vdwlem7.g . . . . . . . 8  |-  ( ph  ->  G : ( 1 ... W ) --> R )
1615adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  G : ( 1 ... W ) --> R )
17 vdwlem6.b . . . . . . . 8  |-  ( ph  ->  B  e.  NN )
1817adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  B  e.  NN )
19 vdwlem7.m . . . . . . . 8  |-  ( ph  ->  M  e.  NN )
2019adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  M  e.  NN )
21 vdwlem6.e . . . . . . . 8  |-  ( ph  ->  E : ( 1 ... M ) --> NN )
2221adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  E : ( 1 ... M ) --> NN )
23 vdwlem6.s . . . . . . . 8  |-  ( ph  ->  A. i  e.  ( 1 ... M ) ( ( B  +  ( E `  i ) ) (AP `  K
) ( E `  i ) )  C_  ( `' G " { ( G `  ( B  +  ( E `  i ) ) ) } ) )
2423adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  A. i  e.  ( 1 ... M
) ( ( B  +  ( E `  i ) ) (AP
`  K ) ( E `  i ) )  C_  ( `' G " { ( G `
 ( B  +  ( E `  i ) ) ) } ) )
25 simprl 733 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  m  e.  ( 1 ... M
) )
26 simprr 734 . . . . . . . 8  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  ( J `  m )  =  ( G `  B ) )
27 fveq2 5668 . . . . . . . . . . . 12  |-  ( i  =  m  ->  ( E `  i )  =  ( E `  m ) )
2827oveq2d 6036 . . . . . . . . . . 11  |-  ( i  =  m  ->  ( B  +  ( E `  i ) )  =  ( B  +  ( E `  m ) ) )
2928fveq2d 5672 . . . . . . . . . 10  |-  ( i  =  m  ->  ( G `  ( B  +  ( E `  i ) ) )  =  ( G `  ( B  +  ( E `  m )
) ) )
30 fvex 5682 . . . . . . . . . 10  |-  ( G `
 ( B  +  ( E `  m ) ) )  e.  _V
3129, 2, 30fvmpt 5745 . . . . . . . . 9  |-  ( m  e.  ( 1 ... M )  ->  ( J `  m )  =  ( G `  ( B  +  ( E `  m )
) ) )
3225, 31syl 16 . . . . . . . 8  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  ( J `  m )  =  ( G `  ( B  +  ( E `  m )
) ) )
3326, 32eqtr3d 2421 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  ( G `  B )  =  ( G `  ( B  +  ( E `  m )
) ) )
347, 12, 14, 16, 18, 20, 22, 24, 25, 33vdwlem1 13276 . . . . . 6  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  ( K  +  1 ) MonoAP  G )
3534rexlimdvaa 2774 . . . . 5  |-  ( ph  ->  ( E. m  e.  ( 1 ... M
) ( J `  m )  =  ( G `  B )  ->  ( K  + 
1 ) MonoAP  G )
)
365, 35syl5bi 209 . . . 4  |-  ( ph  ->  ( ( G `  B )  e.  ran  J  ->  ( K  + 
1 ) MonoAP  G )
)
3736imp 419 . . 3  |-  ( (
ph  /\  ( G `  B )  e.  ran  J )  ->  ( K  +  1 ) MonoAP  G
)
3837olcd 383 . 2  |-  ( (
ph  /\  ( G `  B )  e.  ran  J )  ->  ( <. ( M  +  1 ) ,  K >. PolyAP  H  \/  ( K  +  1
) MonoAP  G ) )
39 vdwlem3.v . . . . . . 7  |-  ( ph  ->  V  e.  NN )
40 vdwlem4.h . . . . . . 7  |-  ( ph  ->  H : ( 1 ... ( W  x.  ( 2  x.  V
) ) ) --> R )
41 vdwlem4.f . . . . . . 7  |-  F  =  ( x  e.  ( 1 ... V ) 
|->  ( y  e.  ( 1 ... W ) 
|->  ( H `  (
y  +  ( W  x.  ( ( x  -  1 )  +  V ) ) ) ) ) )
42 vdwlem7.a . . . . . . 7  |-  ( ph  ->  A  e.  NN )
43 vdwlem7.d . . . . . . 7  |-  ( ph  ->  D  e.  NN )
44 vdwlem7.s . . . . . . 7  |-  ( ph  ->  ( A (AP `  K ) D ) 
C_  ( `' F " { G } ) )
45 vdwlem6.r . . . . . . 7  |-  ( ph  ->  ( # `  ran  J )  =  M )
46 vdwlem6.t . . . . . . 7  |-  T  =  ( B  +  ( W  x.  ( ( A  +  ( V  -  D ) )  -  1 ) ) )
47 vdwlem6.p . . . . . . 7  |-  P  =  ( j  e.  ( 1 ... ( M  +  1 ) ) 
|->  ( if ( j  =  ( M  + 
1 ) ,  0 ,  ( E `  j ) )  +  ( W  x.  D
) ) )
4839, 13, 6, 40, 41, 19, 15, 8, 42, 43, 44, 17, 21, 23, 2, 45, 46, 47vdwlem5 13280 . . . . . 6  |-  ( ph  ->  T  e.  NN )
4948adantr 452 . . . . 5  |-  ( (
ph  /\  -.  ( G `  B )  e.  ran  J )  ->  T  e.  NN )
50 0nn0 10168 . . . . . . . . . 10  |-  0  e.  NN0
5150a1i 11 . . . . . . . . 9  |-  ( ( ( ( ph  /\  -.  ( G `  B
)  e.  ran  J
)  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  /\  j  =  ( M  + 
1 ) )  -> 
0  e.  NN0 )
52 nnuz 10453 . . . . . . . . . . . . . . . . 17  |-  NN  =  ( ZZ>= `  1 )
5319, 52syl6eleq 2477 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
5453adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  ( G `  B )  e.  ran  J )  ->  M  e.  ( ZZ>= ` 
1 ) )
55 elfzp1 11029 . . . . . . . . . . . . . . 15  |-  ( M  e.  ( ZZ>= `  1
)  ->  ( j  e.  ( 1 ... ( M  +  1 ) )  <->  ( j  e.  ( 1 ... M
)  \/  j  =  ( M  +  1 ) ) ) )
5654, 55syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( G `  B )  e.  ran  J )  -> 
( j  e.  ( 1 ... ( M  +  1 ) )  <-> 
( j  e.  ( 1 ... M )  \/  j  =  ( M  +  1 ) ) ) )
5756biimpa 471 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  ( G `  B )  e.  ran  J )  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  ->  ( j  e.  ( 1 ... M
)  \/  j  =  ( M  +  1 ) ) )
5857ord 367 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  ( G `  B )  e.  ran  J )  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  ->  ( -.  j  e.  ( 1 ... M )  -> 
j  =  ( M  +  1 ) ) )
5958con1d 118 . . . . . . . . . . 11  |-  ( ( ( ph  /\  -.  ( G `  B )  e.  ran  J )  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  ->  ( -.  j  =  ( M  +  1 )  -> 
j  e.  ( 1 ... M ) ) )
6059imp 419 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  -.  ( G `  B
)  e.  ran  J
)  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  /\  -.  j  =  ( M  +  1 ) )  ->  j  e.  ( 1 ... M ) )
6121ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  ( G `  B )  e.  ran  J )  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  ->  E :
( 1 ... M
) --> NN )
6261ffvelrnda 5809 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  -.  ( G `  B
)  e.  ran  J
)  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  /\  j  e.  ( 1 ... M
) )  ->  ( E `  j )  e.  NN )
6362nnnn0d 10206 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  -.  ( G `  B
)  e.  ran  J
)  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  /\  j  e.  ( 1 ... M
) )  ->  ( E `  j )  e.  NN0 )
6460, 63syldan 457 . . . . . . . . 9  |-  ( ( ( ( ph  /\  -.  ( G `  B
)  e.  ran  J
)  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  /\  -.  j  =  ( M  +  1 ) )  ->  ( E `  j )  e.  NN0 )
6551, 64ifclda 3709 . . . . . . . 8  |-  ( ( ( ph  /\  -.  ( G `  B )  e.  ran  J )  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  ->  if (
j  =  ( M  +  1 ) ,  0 ,  ( E `
 j ) )  e.  NN0 )
6613, 43nnmulcld 9979 . . . . . . . . 9  |-  ( ph  ->  ( W  x.  D
)  e.  NN )
6766ad2antrr 707 . . . . . . . 8  |-  ( ( ( ph  /\  -.  ( G `  B )  e.  ran  J )  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  ->  ( W  x.  D )  e.  NN )
68 nn0nnaddcl 10184 . . . . . . . 8  |-  ( ( if ( j  =  ( M  +  1 ) ,  0 ,  ( E `  j
) )  e.  NN0  /\  ( W  x.  D
)  e.  NN )  ->  ( if ( j  =  ( M  +  1 ) ,  0 ,  ( E `
 j ) )  +  ( W  x.  D ) )  e.  NN )
6965, 67, 68syl2anc 643 . . . . . . 7  |-  ( ( ( ph  /\  -.  ( G `  B )  e.  ran  J )  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  ->  ( if ( j  =  ( M  +  1 ) ,  0 ,  ( E `  j ) )  +  ( W  x.  D ) )  e.  NN )
7069, 47fmptd 5832 . . . . . 6  |-  ( (
ph  /\  -.  ( G `  B )  e.  ran  J )  ->  P : ( 1 ... ( M  +  1 ) ) --> NN )
71 nnex 9938 . . . . . . 7  |-  NN  e.  _V
72 ovex 6045 . . . . . . 7  |-  ( 1 ... ( M  + 
1 ) )  e. 
_V
7371, 72elmap 6978 . . . . . 6  |-  ( P  e.  ( NN  ^m  ( 1 ... ( M  +  1 ) ) )  <->  P :
( 1 ... ( M  +  1 ) ) --> NN )
7470, 73sylibr 204 . . . . 5  |-  ( (
ph  /\  -.  ( G `  B )  e.  ran  J )  ->  P  e.  ( NN  ^m  ( 1 ... ( M  +  1 ) ) ) )
75 elfzp1 11029 . . . . . . . . . 10  |-  ( M  e.  ( ZZ>= `  1
)  ->  ( i  e.  ( 1 ... ( M  +  1 ) )  <->  ( i  e.  ( 1 ... M
)  \/  i  =  ( M  +  1 ) ) ) )
7653, 75syl 16 . . . . . . . . 9  |-  ( ph  ->  ( i  e.  ( 1 ... ( M  +  1 ) )  <-> 
( i  e.  ( 1 ... M )  \/  i  =  ( M  +  1 ) ) ) )
7717adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  B  e.  NN )
7877nncnd 9948 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  B  e.  CC )
7978adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  B  e.  CC )
8021ffvelrnda 5809 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( E `  i )  e.  NN )
8180nncnd 9948 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( E `  i )  e.  CC )
8281adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( E `  i )  e.  CC )
8379, 82addcld 9040 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( B  +  ( E `  i ) )  e.  CC )
84 nnm1nn0 10193 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  e.  NN  ->  ( A  -  1 )  e.  NN0 )
8542, 84syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( A  -  1 )  e.  NN0 )
86 nn0nnaddcl 10184 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( A  -  1 )  e.  NN0  /\  V  e.  NN )  ->  ( ( A  - 
1 )  +  V
)  e.  NN )
8785, 39, 86syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( A  - 
1 )  +  V
)  e.  NN )
8813, 87nnmulcld 9979 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( W  x.  (
( A  -  1 )  +  V ) )  e.  NN )
8988nncnd 9948 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( W  x.  (
( A  -  1 )  +  V ) )  e.  CC )
9089ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  x.  ( ( A  -  1 )  +  V ) )  e.  CC )
91 elfznn0 11015 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  ( 0 ... ( K  -  1 ) )  ->  m  e.  NN0 )
9291adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  m  e.  NN0 )
9392nn0cnd 10208 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  m  e.  CC )
9493adantlr 696 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  m  e.  CC )
9594, 82mulcld 9041 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  ( E `
 i ) )  e.  CC )
9666nnnn0d 10206 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( W  x.  D
)  e.  NN0 )
9796adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  x.  D )  e.  NN0 )
9892, 97nn0mulcld 10211 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  ( W  x.  D ) )  e.  NN0 )
9998nn0cnd 10208 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  ( W  x.  D ) )  e.  CC )
10099adantlr 696 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  ( W  x.  D ) )  e.  CC )
10183, 90, 95, 100add4d 9221 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  +  ( ( m  x.  ( E `  i ) )  +  ( m  x.  ( W  x.  D )
) ) )  =  ( ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) )  +  ( ( W  x.  (
( A  -  1 )  +  V ) )  +  ( m  x.  ( W  x.  D ) ) ) ) )
10266nncnd 9948 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( W  x.  D
)  e.  CC )
103102ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  x.  D )  e.  CC )
10494, 82, 103adddid 9045 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  ( ( E `  i )  +  ( W  x.  D ) ) )  =  ( ( m  x.  ( E `  i ) )  +  ( m  x.  ( W  x.  D )
) ) )
105104oveq2d 6036 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  +  ( m  x.  ( ( E `  i )  +  ( W  x.  D ) ) ) )  =  ( ( ( B  +  ( E `  i ) )  +  ( W  x.  (
( A  -  1 )  +  V ) ) )  +  ( ( m  x.  ( E `  i )
)  +  ( m  x.  ( W  x.  D ) ) ) ) )
10613nncnd 9948 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  W  e.  CC )
107106adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  W  e.  CC )
10887nncnd 9948 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( A  - 
1 )  +  V
)  e.  CC )
109108adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  -  1 )  +  V )  e.  CC )
11043nncnd 9948 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  D  e.  CC )
111110adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  D  e.  CC )
11293, 111mulcld 9041 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  D )  e.  CC )
113107, 109, 112adddid 9045 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  x.  ( (
( A  -  1 )  +  V )  +  ( m  x.  D ) ) )  =  ( ( W  x.  ( ( A  -  1 )  +  V ) )  +  ( W  x.  (
m  x.  D ) ) ) )
11442nncnd 9948 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  A  e.  CC )
115114adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  A  e.  CC )
116 ax-1cn 8981 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  1  e.  CC
117116a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  1  e.  CC )
118115, 112, 117addsubd 9364 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  +  ( m  x.  D ) )  -  1 )  =  ( ( A  -  1 )  +  ( m  x.  D
) ) )
119118oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V )  =  ( ( ( A  -  1 )  +  ( m  x.  D ) )  +  V ) )
12085nn0cnd 10208 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( A  -  1 )  e.  CC )
121120adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  -  1 )  e.  CC )
12239nncnd 9948 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  V  e.  CC )
123122adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  V  e.  CC )
124121, 112, 123add32d 9220 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( A  - 
1 )  +  ( m  x.  D ) )  +  V )  =  ( ( ( A  -  1 )  +  V )  +  ( m  x.  D
) ) )
125119, 124eqtrd 2419 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V )  =  ( ( ( A  -  1 )  +  V )  +  ( m  x.  D
) ) )
126125oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  x.  ( (
( A  +  ( m  x.  D ) )  -  1 )  +  V ) )  =  ( W  x.  ( ( ( A  -  1 )  +  V )  +  ( m  x.  D ) ) ) )
12793, 107, 111mul12d 9207 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  ( W  x.  D ) )  =  ( W  x.  ( m  x.  D
) ) )
128127oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( W  x.  (
( A  -  1 )  +  V ) )  +  ( m  x.  ( W  x.  D ) ) )  =  ( ( W  x.  ( ( A  -  1 )  +  V ) )  +  ( W  x.  (
m  x.  D ) ) ) )
129113, 126, 1283eqtr4d 2429 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  x.  ( (
( A  +  ( m  x.  D ) )  -  1 )  +  V ) )  =  ( ( W  x.  ( ( A  -  1 )  +  V ) )  +  ( m  x.  ( W  x.  D )
) ) )
130129adantlr 696 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  x.  ( (
( A  +  ( m  x.  D ) )  -  1 )  +  V ) )  =  ( ( W  x.  ( ( A  -  1 )  +  V ) )  +  ( m  x.  ( W  x.  D )
) ) )
131130oveq2d 6036 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  - 
1 )  +  V
) ) )  =  ( ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) )  +  ( ( W  x.  (
( A  -  1 )  +  V ) )  +  ( m  x.  ( W  x.  D ) ) ) ) )
132101, 105, 1313eqtr4d 2429 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  +  ( m  x.  ( ( E `  i )  +  ( W  x.  D ) ) ) )  =  ( ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) )  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) ) )
13339ad2antrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  V  e.  NN )
13413ad2antrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  W  e.  NN )
13544adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A (AP `  K ) D )  C_  ( `' F " { G } ) )
136 eqid 2387 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  +  ( m  x.  D ) )  =  ( A  +  ( m  x.  D ) )
137 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  m  ->  (
n  x.  D )  =  ( m  x.  D ) )
138137oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  m  ->  ( A  +  ( n  x.  D ) )  =  ( A  +  ( m  x.  D ) ) )
139138eqeq2d 2398 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  m  ->  (
( A  +  ( m  x.  D ) )  =  ( A  +  ( n  x.  D ) )  <->  ( A  +  ( m  x.  D ) )  =  ( A  +  ( m  x.  D ) ) ) )
140139rspcev 2995 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( m  e.  ( 0 ... ( K  - 
1 ) )  /\  ( A  +  (
m  x.  D ) )  =  ( A  +  ( m  x.  D ) ) )  ->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( A  +  ( m  x.  D ) )  =  ( A  +  ( n  x.  D ) ) )
141136, 140mpan2 653 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  ( 0 ... ( K  -  1 ) )  ->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( A  +  ( m  x.  D
) )  =  ( A  +  ( n  x.  D ) ) )
14211nnnn0d 10206 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  K  e.  NN0 )
143 vdwapval 13268 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( K  e.  NN0  /\  A  e.  NN  /\  D  e.  NN )  ->  (
( A  +  ( m  x.  D ) )  e.  ( A (AP `  K ) D )  <->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( A  +  ( m  x.  D
) )  =  ( A  +  ( n  x.  D ) ) ) )
144142, 42, 43, 143syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( A  +  ( m  x.  D
) )  e.  ( A (AP `  K
) D )  <->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( A  +  ( m  x.  D
) )  =  ( A  +  ( n  x.  D ) ) ) )
145144biimpar 472 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  E. n  e.  ( 0 ... ( K  -  1 ) ) ( A  +  ( m  x.  D
) )  =  ( A  +  ( n  x.  D ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( A (AP `  K ) D ) )
146141, 145sylan2 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( A (AP `  K ) D ) )
147135, 146sseldd 3292 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( `' F " { G } ) )
14839, 13, 6, 40, 41vdwlem4 13279 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  F : ( 1 ... V ) --> ( R  ^m  ( 1 ... W ) ) )
149 ffn 5531 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F : ( 1 ... V ) --> ( R  ^m  ( 1 ... W ) )  ->  F  Fn  ( 1 ... V ) )
150148, 149syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  F  Fn  ( 1 ... V ) )
151 fniniseg 5790 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( F  Fn  ( 1 ... V )  ->  (
( A  +  ( m  x.  D ) )  e.  ( `' F " { G } )  <->  ( ( A  +  ( m  x.  D ) )  e.  ( 1 ... V
)  /\  ( F `  ( A  +  ( m  x.  D ) ) )  =  G ) ) )
152150, 151syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( A  +  ( m  x.  D
) )  e.  ( `' F " { G } )  <->  ( ( A  +  ( m  x.  D ) )  e.  ( 1 ... V
)  /\  ( F `  ( A  +  ( m  x.  D ) ) )  =  G ) ) )
153152biimpa 471 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( A  +  ( m  x.  D ) )  e.  ( `' F " { G } ) )  ->  ( ( A  +  ( m  x.  D ) )  e.  ( 1 ... V
)  /\  ( F `  ( A  +  ( m  x.  D ) ) )  =  G ) )
154147, 153syldan 457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  +  ( m  x.  D ) )  e.  ( 1 ... V )  /\  ( F `  ( A  +  ( m  x.  D ) ) )  =  G ) )
155154simpld 446 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( 1 ... V
) )
156155adantlr 696 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( 1 ... V
) )
15723r19.21bi 2747 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( B  +  ( E `  i ) ) (AP `  K
) ( E `  i ) )  C_  ( `' G " { ( G `  ( B  +  ( E `  i ) ) ) } ) )
158157adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( B  +  ( E `  i ) ) (AP `  K
) ( E `  i ) )  C_  ( `' G " { ( G `  ( B  +  ( E `  i ) ) ) } ) )
159 eqid 2387 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( B  +  ( E `
 i ) )  +  ( m  x.  ( E `  i
) ) )  =  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )
160 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  m  ->  (
n  x.  ( E `
 i ) )  =  ( m  x.  ( E `  i
) ) )
161160oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  m  ->  (
( B  +  ( E `  i ) )  +  ( n  x.  ( E `  i ) ) )  =  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) ) )
162161eqeq2d 2398 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  m  ->  (
( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  =  ( ( B  +  ( E `  i ) )  +  ( n  x.  ( E `  i )
) )  <->  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) )  =  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) ) ) )
163162rspcev 2995 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( m  e.  ( 0 ... ( K  - 
1 ) )  /\  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  =  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) ) )  ->  E. n  e.  (
0 ... ( K  - 
1 ) ) ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  =  ( ( B  +  ( E `  i ) )  +  ( n  x.  ( E `  i )
) ) )
164159, 163mpan2 653 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  ( 0 ... ( K  -  1 ) )  ->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) )  =  ( ( B  +  ( E `  i ) )  +  ( n  x.  ( E `  i ) ) ) )
16511adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  K  e.  NN )
166165nnnn0d 10206 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  K  e.  NN0 )
16777, 80nnaddcld 9978 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( B  +  ( E `  i ) )  e.  NN )
168 vdwapval 13268 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( K  e.  NN0  /\  ( B  +  ( E `  i )
)  e.  NN  /\  ( E `  i )  e.  NN )  -> 
( ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) )  e.  ( ( B  +  ( E `  i ) ) (AP `  K
) ( E `  i ) )  <->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) )  =  ( ( B  +  ( E `  i ) )  +  ( n  x.  ( E `  i ) ) ) ) )
169166, 167, 80, 168syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  e.  ( ( B  +  ( E `  i ) ) (AP
`  K ) ( E `  i ) )  <->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  =  ( ( B  +  ( E `  i ) )  +  ( n  x.  ( E `  i )
) ) ) )
170169biimpar 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  E. n  e.  ( 0 ... ( K  - 
1 ) ) ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  =  ( ( B  +  ( E `  i ) )  +  ( n  x.  ( E `  i )
) ) )  -> 
( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  e.  ( ( B  +  ( E `  i ) ) (AP
`  K ) ( E `  i ) ) )
171164, 170sylan2 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  e.  ( ( B  +  ( E `  i ) ) (AP
`  K ) ( E `  i ) ) )
172158, 171sseldd 3292 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  e.  ( `' G " { ( G `  ( B  +  ( E `  i )
) ) } ) )
173 ffn 5531 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( G : ( 1 ... W ) --> R  ->  G  Fn  ( 1 ... W ) )
17415, 173syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  G  Fn  ( 1 ... W ) )
175174adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  G  Fn  ( 1 ... W
) )
176 fniniseg 5790 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( G  Fn  ( 1 ... W )  ->  (
( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  e.  ( `' G " { ( G `  ( B  +  ( E `  i )
) ) } )  <-> 
( ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) )  e.  ( 1 ... W )  /\  ( G `  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) ) )  =  ( G `
 ( B  +  ( E `  i ) ) ) ) ) )
177175, 176syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  e.  ( `' G " { ( G `  ( B  +  ( E `  i )
) ) } )  <-> 
( ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) )  e.  ( 1 ... W )  /\  ( G `  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) ) )  =  ( G `
 ( B  +  ( E `  i ) ) ) ) ) )
178177biimpa 471 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  (
( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  e.  ( `' G " { ( G `  ( B  +  ( E `  i )
) ) } ) )  ->  ( (
( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  e.  ( 1 ... W )  /\  ( G `  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) ) )  =  ( G `  ( B  +  ( E `  i ) ) ) ) )
179172, 178syldan 457 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  e.  ( 1 ... W )  /\  ( G `  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) ) )  =  ( G `  ( B  +  ( E `  i ) ) ) ) )
180179simpld 446 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  e.  ( 1 ... W ) )
181133, 134, 156, 180vdwlem3 13278 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  - 
1 )  +  V
) ) )  e.  ( 1 ... ( W  x.  ( 2  x.  V ) ) ) )
182132, 181eqeltrd 2461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  +  ( m  x.  ( ( E `  i )  +  ( W  x.  D ) ) ) )  e.  ( 1 ... ( W  x.  ( 2  x.  V ) ) ) )
183 oveq1 6027 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) )  ->  (
y  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) )  =  ( ( ( B  +  ( E `
 i ) )  +  ( m  x.  ( E `  i
) ) )  +  ( W  x.  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V ) ) ) )
184183fveq2d 5672 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) )  ->  ( H `  ( y  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  - 
1 )  +  V
) ) ) )  =  ( H `  ( ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) )  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) ) ) )
185 eqid 2387 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V ) ) ) ) )  =  ( y  e.  ( 1 ... W
)  |->  ( H `  ( y  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) ) ) )
186 fvex 5682 . . . . . . . . . . . . . . . . . . . 20  |-  ( H `
 ( ( ( B  +  ( E `
 i ) )  +  ( m  x.  ( E `  i
) ) )  +  ( W  x.  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V ) ) ) )  e. 
_V
187184, 185, 186fvmpt 5745 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  e.  ( 1 ... W )  ->  (
( y  e.  ( 1 ... W ) 
|->  ( H `  (
y  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) ) ) ) `  (
( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) ) )  =  ( H `
 ( ( ( B  +  ( E `
 i ) )  +  ( m  x.  ( E `  i
) ) )  +  ( W  x.  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V ) ) ) ) )
188180, 187syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( y  e.  ( 1 ... W ) 
|->  ( H `  (
y  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) ) ) ) `  (
( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) ) )  =  ( H `
 ( ( ( B  +  ( E `
 i ) )  +  ( m  x.  ( E `  i
) ) )  +  ( W  x.  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V ) ) ) ) )
189179simprd 450 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( G `  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) ) )  =  ( G `  ( B  +  ( E `  i ) ) ) )
190154simprd 450 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( F `  ( A  +  ( m  x.  D ) ) )  =  G )
191 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  (
x  -  1 )  =  ( ( A  +  ( m  x.  D ) )  - 
1 ) )
192191oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  (
( x  -  1 )  +  V )  =  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) )
193192oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  ( W  x.  ( (
x  -  1 )  +  V ) )  =  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  - 
1 )  +  V
) ) )
194193oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  (
y  +  ( W  x.  ( ( x  -  1 )  +  V ) ) )  =  ( y  +  ( W  x.  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V ) ) ) )
195194fveq2d 5672 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  ( H `  ( y  +  ( W  x.  ( ( x  - 
1 )  +  V
) ) ) )  =  ( H `  ( y  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) ) ) )
196195mpteq2dv 4237 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  (
y  e.  ( 1 ... W )  |->  ( H `  ( y  +  ( W  x.  ( ( x  - 
1 )  +  V
) ) ) ) )  =  ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V ) ) ) ) ) )
197 ovex 6045 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1 ... W )  e. 
_V
198197mptex 5905 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V ) ) ) ) )  e.  _V
199196, 41, 198fvmpt 5745 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  +  ( m  x.  D ) )  e.  ( 1 ... V )  ->  ( F `  ( A  +  ( m  x.  D ) ) )  =  ( y  e.  ( 1 ... W
)  |->  ( H `  ( y  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) ) ) ) )
200155, 199syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( F `  ( A  +  ( m  x.  D ) ) )  =  ( y  e.  ( 1 ... W
)  |->  ( H `  ( y  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) ) ) ) )
201190, 200eqtr3d 2421 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  G  =  ( y  e.  ( 1 ... W
)  |->  ( H `  ( y  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) ) ) ) )
202201adantlr 696 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  G  =  ( y  e.  ( 1 ... W
)  |->  ( H `  ( y  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) ) ) ) )
203202fveq1d 5670 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( G `  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) ) )  =  ( ( y  e.  ( 1 ... W
)  |->  ( H `  ( y  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) ) ) ) `  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) ) ) )
204189, 203eqtr3d 2421 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( G `  ( B  +  ( E `  i ) ) )  =  ( ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V ) ) ) ) ) `
 ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) ) ) )
205132fveq2d 5672 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( H `  ( (
( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  +  ( m  x.  ( ( E `  i )  +  ( W  x.  D ) ) ) ) )  =  ( H `  ( ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) )  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) ) ) )
206188, 204, 2053eqtr4rd 2430 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( H `  ( (
( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  +  ( m  x.  ( ( E `  i )  +  ( W  x.  D ) ) ) ) )  =  ( G `  ( B  +  ( E `  i )
) ) )
207182, 206jca 519 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( ( B  +  ( E `  i ) )  +  ( W  x.  (
( A  -  1 )  +  V ) ) )  +  ( m  x.  ( ( E `  i )  +  ( W  x.  D ) ) ) )  e.  ( 1 ... ( W  x.  ( 2  x.  V
) ) )  /\  ( H `  ( ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  +  ( m  x.  ( ( E `  i )  +  ( W  x.  D ) ) ) ) )  =  ( G `  ( B  +  ( E `  i )
) ) ) )
208 eleq1 2447 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( ( ( B  +  ( E `
 i ) )  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) )  +  ( m  x.  (
( E `  i
)  +  ( W  x.  D ) ) ) )  ->  (
x  e.  ( 1 ... ( W  x.  ( 2  x.  V
) ) )  <->  ( (
( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  +  ( m  x.  ( ( E `  i )  +  ( W  x.  D ) ) ) )  e.  ( 1 ... ( W  x.  ( 2  x.  V ) ) ) ) )
209 fveq2 5668 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( ( ( B  +  ( E `
 i ) )  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) )  +  ( m  x.  (
( E `  i
)  +  ( W  x.  D ) ) ) )  ->  ( H `  x )  =  ( H `  ( ( ( B  +  ( E `  i ) )  +  ( W  x.  (
( A  -  1 )  +  V ) ) )  +  ( m  x.  ( ( E `  i )  +  ( W  x.  D ) ) ) ) ) )
210209eqeq1d 2395 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( ( ( B  +  ( E `
 i ) )  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) )  +  ( m  x.  (
( E `  i
)  +  ( W  x.  D ) ) ) )  ->  (
( H `  x
)  =  ( G `
 ( B  +  ( E `  i ) ) )  <->  ( H `  ( ( ( B  +  ( E `  i ) )  +  ( W  x.  (
( A  -  1 )  +  V ) ) )  +  ( m  x.  ( ( E `  i )  +  ( W  x.  D ) ) ) ) )  =  ( G `  ( B  +  ( E `  i ) ) ) ) )
211208, 210anbi12d 692 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( ( ( B  +  ( E `
 i ) )  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) )  +  ( m  x.  (
( E `  i
)  +  ( W  x.  D ) ) ) )  ->  (
( x  e.  ( 1 ... ( W  x.  ( 2  x.  V ) ) )  /\  ( H `  x )  =  ( G `  ( B  +  ( E `  i ) ) ) )  <->  ( ( ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  +  ( m  x.  ( ( E `  i )  +  ( W  x.  D ) ) ) )  e.  ( 1 ... ( W  x.  ( 2  x.  V ) ) )  /\  ( H `
 ( ( ( B  +  ( E `
 i ) )  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) )  +  ( m  x.  (
( E `  i
)  +  ( W  x.  D ) ) ) ) )  =  ( G `  ( B  +  ( E `  i ) ) ) ) ) )
212207, 211syl5ibrcom 214 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
x  =  ( ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  +  ( m  x.  ( ( E `  i )  +  ( W  x.  D ) ) ) )  -> 
( x  e.  ( 1 ... ( W  x.  ( 2  x.  V ) ) )  /\  ( H `  x )  =  ( G `  ( B  +  ( E `  i ) ) ) ) ) )
213212rexlimdva 2773 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( E. m  e.  (
0 ... ( K  - 
1 ) ) x  =  ( ( ( B  +  ( E `
 i ) )  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) )  +  ( m  x.  (
( E `  i
)  +  ( W  x.  D ) ) ) )  ->  (
x  e.  ( 1 ... ( W  x.  ( 2  x.  V
) ) )  /\  ( H `  x )  =  ( G `  ( B  +  ( E `  i )
) ) ) ) )
21488adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( W  x.  ( ( A  -  1 )  +  V ) )  e.  NN )
215167, 214nnaddcld 9978 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  e.  NN )
21666adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( W  x.  D )  e.  NN )
21780, 216nnaddcld 9978 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( E `  i
)  +  ( W  x.  D ) )  e.  NN )
218 vdwapval 13268 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  NN0  /\  ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  e.  NN  /\  (
( E `  i
)  +  ( W  x.  D ) )  e.  NN )  -> 
( x  e.  ( ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) (AP `  K ) ( ( E `  i )  +  ( W  x.  D ) ) )  <->  E. m  e.  ( 0 ... ( K  -  1 ) ) x  =  ( ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  +  ( m  x.  ( ( E `  i )  +  ( W  x.  D ) ) ) ) ) )
219166, 215, 217, 218syl3anc 1184 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
x  e.  ( ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) (AP `  K ) ( ( E `  i )  +  ( W  x.  D ) ) )  <->  E. m  e.  ( 0 ... ( K  -  1 ) ) x  =  ( ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  +  ( m  x.  ( ( E `  i )  +  ( W  x.  D ) ) ) ) ) )
220 ffn 5531 . . . . . . . . . . . . . . . . 17  |-  ( H : ( 1 ... ( W  x.  (
2  x.  V ) ) ) --> R  ->  H  Fn  ( 1 ... ( W  x.  ( 2  x.  V
) ) ) )
22140, 220syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  H  Fn  ( 1 ... ( W  x.  ( 2  x.  V
) ) ) )
222221adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  H  Fn  ( 1 ... ( W  x.  ( 2  x.  V ) ) ) )
223 fniniseg 5790 . . . . . . . . . . . . . . 15  |-  ( H  Fn  ( 1 ... ( W  x.  (
2  x.  V ) ) )  ->  (
x  e.  ( `' H " { ( G `  ( B  +  ( E `  i ) ) ) } )  <->  ( x  e.  ( 1 ... ( W  x.  ( 2  x.  V ) ) )  /\  ( H `
 x )  =  ( G `  ( B  +  ( E `  i ) ) ) ) ) )
224222, 223syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
x  e.  ( `' H " { ( G `  ( B  +  ( E `  i ) ) ) } )  <->  ( x  e.  ( 1 ... ( W  x.  ( 2  x.  V ) ) )  /\  ( H `
 x )  =  ( G `  ( B  +  ( E `  i ) ) ) ) ) )
225213, 219, 2243imtr4d 260 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
x  e.  ( ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) (AP `  K ) ( ( E `  i )  +  ( W  x.  D ) ) )  ->  x  e.  ( `' H " { ( G `  ( B  +  ( E `  i )
) ) } ) ) )
226225ssrdv 3297 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) (AP `  K ) ( ( E `  i )  +  ( W  x.  D ) ) )  C_  ( `' H " { ( G `  ( B  +  ( E `  i ) ) ) } ) )
227 ssun1 3453 . . . . . . . . . . . . . . . . . . 19  |-  ( 1 ... M )  C_  ( ( 1 ... M )  u.  {
( M  +  1 ) } )
228 fzsuc 11028 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  e.  ( ZZ>= `  1
)  ->  ( 1 ... ( M  + 
1 ) )  =  ( ( 1 ... M )  u.  {
( M  +  1 ) } ) )
22953, 228syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( 1 ... ( M  +  1 ) )  =  ( ( 1 ... M )  u.  { ( M  +  1 ) } ) )
230227, 229syl5sseqr 3340 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 1 ... M
)  C_  ( 1 ... ( M  + 
1 ) ) )
231230sselda 3291 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  i  e.  ( 1 ... ( M  +  1 ) ) )
232 eqeq1 2393 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  i  ->  (
j  =  ( M  +  1 )  <->  i  =  ( M  +  1
) ) )
233 fveq2 5668 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  i  ->  ( E `  j )  =  ( E `  i ) )
234232, 233ifbieq2d 3702 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  i  ->  if ( j  =  ( M  +  1 ) ,  0 ,  ( E `  j ) )  =  if ( i  =  ( M  +  1 ) ,  0 ,  ( E `
 i ) ) )
235234oveq1d 6035 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  i  ->  ( if ( j  =  ( M  +  1 ) ,  0 ,  ( E `  j ) )  +  ( W  x.  D ) )  =  ( if ( i  =  ( M  +  1 ) ,  0 ,  ( E `
 i ) )  +  ( W  x.  D ) ) )
236 ovex 6045 . . . . . . . . . . . . . . . . . 18  |-  ( if ( i  =  ( M  +  1 ) ,  0 ,  ( E `  i ) )  +  ( W  x.  D ) )  e.  _V
237235, 47, 236fvmpt 5745 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... ( M  +  1 ) )  ->  ( P `  i )  =  ( if ( i  =  ( M  +  1 ) ,  0 ,  ( E `
 i ) )  +  ( W  x.  D ) ) )
238231, 237syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( P `  i )  =  ( if ( i  =  ( M  +  1 ) ,  0 ,  ( E `
 i ) )  +  ( W  x.  D ) ) )
239 elfzle2 10993 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... M )  ->  i  <_  M )
24019nnred 9947 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  M  e.  RR )
241240ltp1d 9873 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  M  <  ( M  +  1 ) )
242 peano2re 9171 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( M  e.  RR  ->  ( M  +  1 )  e.  RR )
243240, 242syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( M  +  1 )  e.  RR )
244240, 243ltnled 9152 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( M  <  ( M  +  1 )  <->  -.  ( M  +  1 )  <_  M )
)
245241, 244mpbid 202 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  -.  ( M  + 
1 )  <_  M
)
246 breq1 4156 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  ( M  + 
1 )  ->  (
i  <_  M  <->  ( M  +  1 )  <_  M ) )
247246notbid 286 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  =  ( M  + 
1 )  ->  ( -.  i  <_  M  <->  -.  ( M  +  1 )  <_  M ) )
248245, 247syl5ibrcom 214 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( i  =  ( M  +  1 )  ->  -.  i  <_  M ) )
249248con2d 109 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( i  <_  M  ->  -.  i  =  ( M  +  1 ) ) )
250239, 249syl5 30 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( i  e.  ( 1 ... M )  ->  -.  i  =  ( M  +  1
) ) )
251250imp 419 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  -.  i  =  ( M  +  1 ) )
252 iffalse 3689 . . . . . . . . . . . . . . . . . 18  |-  ( -.  i  =  ( M  +  1 )  ->  if ( i  =  ( M  +  1 ) ,  0 ,  ( E `  i ) )  =  ( E `
 i ) )
253252oveq1d 6035 . . . . . . . . . . . . . . . . 17  |-  ( -.  i  =  ( M  +  1 )  -> 
( if ( i  =  ( M  + 
1 ) ,  0 ,  ( E `  i ) )  +  ( W  x.  D
) )  =  ( ( E `  i
)  +  ( W  x.  D ) ) )
254251, 253syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( if ( i  =  ( M  +  1 ) ,  0 ,  ( E `  i ) )  +  ( W  x.  D ) )  =  ( ( E `
 i )  +  ( W  x.  D
) ) )
255238, 254eqtrd 2419 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( P `  i )  =  ( ( E `
 i )  +  ( W  x.  D
) ) )
256255oveq2d 6036 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( T  +  ( P `  i ) )  =  ( T  +  ( ( E `  i
)  +  ( W  x.  D ) ) ) )
25748nncnd 9948 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  e.  CC )
258257adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  T  e.  CC )
259102adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( W  x.  D )  e.  CC )
260258, 81, 259add12d 9219 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( T  +  ( ( E `  i )  +  ( W  x.  D ) ) )  =  ( ( E `
 i )  +  ( T  +  ( W  x.  D ) ) ) )
26146oveq1i 6030 . . . . . . . . . . . . . . . . . 18  |-  ( T  +  ( W  x.  D ) )  =  ( ( B  +  ( W  x.  (
( A  +  ( V  -  D ) )  -  1 ) ) )  +  ( W  x.  D ) )
26217nncnd 9948 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  B  e.  CC )
263122, 110subcld 9343 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( V  -  D
)  e.  CC )
264114, 263addcld 9040 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( A  +  ( V  -  D ) )  e.  CC )
265 subcl 9237 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  +  ( V  -  D ) )  e.  CC  /\  1  e.  CC )  ->  ( ( A  +  ( V  -  D
) )  -  1 )  e.  CC )
266264, 116, 265sylancl 644 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( A  +  ( V  -  D
) )  -  1 )  e.  CC )
267106, 266mulcld 9041 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( W  x.  (
( A  +  ( V  -  D ) )  -  1 ) )  e.  CC )
268262, 267, 102addassd 9043 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( B  +  ( W  x.  (
( A  +  ( V  -  D ) )  -  1 ) ) )  +  ( W  x.  D ) )  =  ( B  +  ( ( W  x.  ( ( A  +  ( V  -  D ) )  - 
1 ) )  +  ( W  x.  D
) ) ) )
269106, 266, 110adddid 9045 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( W  x.  (
( ( A  +  ( V  -  D
) )  -  1 )  +  D ) )  =  ( ( W  x.  ( ( A  +  ( V  -  D ) )  -  1 ) )  +  ( W  x.  D ) ) )
270114, 263, 110addassd 9043 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( A  +  ( V  -  D
) )  +  D
)  =  ( A  +  ( ( V  -  D )  +  D ) ) )
271122, 110npcand 9347 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( V  -  D )  +  D
)  =  V )
272271oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( A  +  ( ( V  -  D
)  +  D ) )  =  ( A  +  V ) )
273270, 272eqtrd 2419 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( A  +  ( V  -  D
) )  +  D
)  =  ( A  +  V ) )
274273oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( A  +  ( V  -  D ) )  +  D )  -  1 )  =  ( ( A  +  V )  -  1 ) )
275116a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  1  e.  CC )
276264, 110, 275addsubd 9364 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( A  +  ( V  -  D ) )  +  D )  -  1 )  =  ( ( ( A  +  ( V  -  D ) )  -  1 )  +  D ) )
277114, 122, 275addsubd 9364 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( A  +  V )  -  1 )  =  ( ( A  -  1 )  +  V ) )
278274, 276, 2773eqtr3d 2427 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( A  +  ( V  -  D ) )  - 
1 )  +  D
)  =  ( ( A  -  1 )  +  V ) )
279278oveq2d 6036 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( W  x.  (
( ( A  +  ( V  -  D
) )  -  1 )  +  D ) )  =  ( W  x.  ( ( A  -  1 )  +  V ) ) )
280269, 279eqtr3d 2421 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( W  x.  ( ( A  +  ( V  -  D
) )  -  1 ) )  +  ( W  x.  D ) )  =  ( W  x.  ( ( A  -  1 )  +  V ) ) )
281280oveq2d 6036 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( B  +  ( ( W  x.  (
( A  +  ( V  -  D ) )  -  1 ) )  +  ( W  x.  D ) ) )  =  ( B  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) ) )
282268, 281eqtrd 2419 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  +  ( W  x.  (
( A  +  ( V  -  D ) )  -  1 ) ) )  +  ( W  x.  D ) )  =  ( B  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) ) )
283261, 282syl5eq 2431 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( T  +  ( W  x.  D ) )  =  ( B  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) ) )
284283oveq2d 6036 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( E `  i )  +  ( T  +  ( W  x.  D ) ) )  =  ( ( E `  i )  +  ( B  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) )
285284adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( E `  i
)  +  ( T  +  ( W  x.  D ) ) )  =  ( ( E `
 i )  +  ( B  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) )
28689adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( W  x.  ( ( A  -  1 )  +  V ) )  e.  CC )
28781, 78, 286addassd 9043 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( E `  i )  +  B
)  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  =  ( ( E `
 i )  +  ( B  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) )
28881, 78addcomd 9200 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( E `  i
)  +  B )  =  ( B  +  ( E `  i ) ) )
289288oveq1d 6035 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( E `  i )  +  B
)  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  =  ( ( B  +  ( E `  i ) )  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) )
290285, 287, 2893eqtr2d 2425 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( E `  i
)  +  ( T  +  ( W  x.  D ) ) )  =  ( ( B  +  ( E `  i ) )  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) )
291256, 260, 2903eqtrd 2423 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( T  +  ( P `  i ) )  =  ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) )
292291, 255oveq12d 6038 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( T  +  ( P `  i ) ) (AP `  K
) ( P `  i ) )  =  ( ( ( B  +  ( E `  i ) )  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) (AP `  K ) ( ( E `  i )  +  ( W  x.  D ) ) ) )
293 cnvimass 5164 . . . . . . . . . . . . . . . . . . 19  |-  ( `' G " { ( G `  ( B  +  ( E `  i ) ) ) } )  C_  dom  G
294 fdm 5535 . . . . . . . . . . . . . . . . . . . 20  |-  ( G : ( 1 ... W ) --> R  ->  dom  G  =  ( 1 ... W ) )
29515, 294syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  dom  G  =  ( 1 ... W ) )
296293, 295syl5sseq 3339 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( `' G " { ( G `  ( B  +  ( E `  i )
) ) } ) 
C_  ( 1 ... W ) )
297296adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( `' G " { ( G `  ( B  +  ( E `  i ) ) ) } )  C_  (
1 ... W ) )
298 vdwapid1 13270 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  NN  /\  ( B  +  ( E `  i )
)  e.  NN  /\  ( E `  i )  e.  NN )  -> 
( B  +  ( E `  i ) )  e.  ( ( B  +  ( E `
 i ) ) (AP `  K ) ( E `  i
) ) )
299165, 167, 80, 298syl3anc 1184 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( B  +  ( E `  i ) )  e.  ( ( B  +  ( E `  i ) ) (AP `  K
) ( E `  i ) ) )
300157, 299sseldd 3292 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( B  +  ( E `  i ) )  e.  ( `' G " { ( G `  ( B  +  ( E `  i )
) ) } ) )
301297, 300sseldd 3292 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( B  +  ( E `  i ) )  e.  ( 1 ... W
) )
302 oveq1 6027 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( B  +  ( E `  i ) )  ->  ( y  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) )  =  ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) )
303302fveq2d 5672 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( B  +  ( E `  i ) )  ->  ( H `  ( y  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) )  =  ( H `  ( ( B  +  ( E `
 i ) )  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) ) ) )
304 eqid 2387 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) )  =  ( y  e.  ( 1 ... W
)  |->  ( H `  ( y  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) )
305 fvex 5682 . . . . . . . . . . . . . . . . 17  |-  ( H `
 ( ( B  +  ( E `  i ) )  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) )  e. 
_V
306303, 304, 305fvmpt 5745 . . . . . . . . . . . . . . . 16  |-  ( ( B  +  ( E `
 i ) )  e.  ( 1 ... W )  ->  (
( y  e.  ( 1 ... W ) 
|->  ( H `  (
y  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) ) `  ( B  +  ( E `  i ) ) )  =  ( H `  ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) )
307301, 306syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( y  e.  ( 1 ... W ) 
|->  ( H `  (
y  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) ) `  ( B  +  ( E `  i ) ) )  =  ( H `  ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) )
308 vdwapid1 13270 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( K  e.  NN  /\  A  e.  NN  /\  D  e.  NN )  ->  A  e.  ( A (AP `  K ) D ) )
30911, 42, 43, 308syl3anc 1184 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  e.  ( A (AP `  K ) D ) )
31044, 309sseldd 3292 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A  e.  ( `' F " { G } ) )
311 fniniseg 5790 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F  Fn  ( 1 ... V )  ->  ( A  e.  ( `' F " { G }
)  <->  ( A  e.  ( 1 ... V
)  /\  ( F `  A )  =  G ) ) )
312150, 311syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( A  e.  ( `' F " { G } )  <->  ( A  e.  ( 1 ... V
)  /\  ( F `  A )  =  G ) ) )
313310, 312mpbid 202 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( A  e.  ( 1 ... V )  /\  ( F `  A )  =  G ) )
314313simprd 450 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( F `  A
)  =  G )
315313simpld 446 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  ( 1 ... V ) )
316 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  A  ->  (
x  -  1 )  =  ( A  - 
1 ) )
317316oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  A  ->  (
( x  -  1 )  +  V )  =  ( ( A  -  1 )  +  V ) )
318317oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  A  ->  ( W  x.  ( (
x  -  1 )  +  V ) )  =  ( W  x.  ( ( A  - 
1 )  +  V
) ) )
319318oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  A  ->  (
y  +  ( W  x.  ( ( x  -  1 )  +  V ) ) )  =  ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) )
320319fveq2d 5672 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  A  ->  ( H `  ( y  +  ( W  x.  ( ( x  - 
1 )  +  V
) ) ) )  =  ( H `  ( y  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) )
321320mpteq2dv 4237 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  A  ->  (
y  e.  ( 1 ... W )  |->  ( H `  ( y  +  ( W  x.  ( ( x  - 
1 )  +  V
) ) ) ) )  =  ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) ) )
322197mptex 5905 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) )  e.  _V
323321, 41, 322fvmpt 5745 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  ( 1 ... V )  ->  ( F `  A )  =  ( y  e.  ( 1 ... W
)  |->  ( H `  ( y  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) ) )
324315, 323syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( F `  A
)  =  ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) ) )
325314, 324eqtr3d 2421 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  G  =  ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) ) )
326325fveq1d 5670 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( G `  ( B  +  ( E `  i ) ) )  =  ( ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) ) `
 ( B  +  ( E `  i ) ) ) )
327326adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( G `  ( B  +  ( E `  i ) ) )  =  ( ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) ) `
 ( B  +  ( E `  i ) ) ) )
328291fveq2d 5672 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( H `  ( T  +  ( P `  i ) ) )  =  ( H `  ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) )
329307, 327, 3283eqtr4rd 2430 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( H `  ( T  +  ( P `  i ) ) )  =  ( G `  ( B  +  ( E `  i )
) ) )
330329sneqd 3770 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  { ( H `  ( T  +  ( P `  i ) ) ) }  =  { ( G `  ( B  +  ( E `  i ) ) ) } )
331330imaeq2d 5143 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( `' H " { ( H `  ( T  +  ( P `  i ) ) ) } )  =  ( `' H " { ( G `  ( B  +  ( E `  i ) ) ) } ) )
332226, 292, 3313sstr4d 3334 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( T  +  ( P `  i ) ) (AP `  K
) ( P `  i ) )  C_  ( `' H " { ( H `  ( T  +  ( P `  i ) ) ) } ) )
333332ex 424 . . . . . . . . . 10  |-  ( ph  ->  ( i  e.  ( 1 ... M )  ->  ( ( T  +  ( P `  i ) ) (AP
`  K ) ( P `  i ) )  C_  ( `' H " { ( H `
 ( T  +  ( P `  i ) ) ) } ) ) )
334262adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  B  e.  CC )
33589adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  x.  ( ( A  -  1 )  +  V ) )  e.  CC )
336334, 335, 99addassd 9043 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( B  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  +  ( m  x.  ( W  x.  D ) ) )  =  ( B  +  ( ( W  x.  ( ( A  - 
1 )  +  V
) )  +  ( m  x.  ( W  x.  D ) ) ) ) )
337129oveq2d 6036 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( B  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  - 
1 )  +  V
) ) )  =  ( B  +  ( ( W  x.  (
( A  -  1 )  +  V ) )  +  ( m  x.  ( W  x.  D ) ) ) ) )
338336, 337eqtr4d 2422 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( B  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  +  ( m  x.  ( W  x.  D ) ) )  =  ( B  +  ( W  x.  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V ) ) ) )
33939adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  V  e.  NN )
34013adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  W  e.  NN )
341 eluzfz1 10996 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... M
) )
34253, 341syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  1  e.  ( 1 ... M ) )
343 ne0i 3577 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1  e.  ( 1 ... M )  ->  (
1 ... M )  =/=  (/) )
344342, 343syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 1 ... M
)  =/=  (/) )
345 elfzuz3 10988 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( B  +  ( E `
 i ) )  e.  ( 1 ... W )  ->  W  e.  ( ZZ>= `  ( B  +  ( E `  i ) ) ) )
346301, 345syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  W  e.  ( ZZ>= `  ( B  +  ( E `  i ) ) ) )
34717nnzd 10306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  B  e.  ZZ )
348 uzid 10432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( B  e.  ZZ  ->  B  e.  ( ZZ>= `  B )
)
349347, 348syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  B  e.  ( ZZ>= `  B ) )
350349adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  B  e.  ( ZZ>= `  B )
)
35180nnnn0d 10206 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( E `  i )  e.  NN0 )
352 uzaddcl 10465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( B  e.  ( ZZ>= `  B )  /\  ( E `  i )  e.  NN0 )  ->  ( B  +  ( E `  i ) )  e.  ( ZZ>= `  B )
)
353350, 351, 352syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( B  +  ( E `  i ) )  e.  ( ZZ>= `  B )
)
354 uztrn 10434 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( W  e.  ( ZZ>= `  ( B  +  ( E `  i )
) )  /\  ( B  +  ( E `  i ) )  e.  ( ZZ>= `  B )
)  ->  W  e.  ( ZZ>= `  B )
)
355346, 353, 354syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  W  e.  ( ZZ>= `  B )
)
356 eluzle 10430 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( W  e.  ( ZZ>= `  B
)  ->  B  <_  W )
357355, 356syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  B  <_  W )
358357ralrimiva 2732 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A. i  e.  ( 1 ... M ) B  <_  W )
359 r19.2z 3660 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 1 ... M
)  =/=  (/)  /\  A. i  e.  ( 1 ... M ) B  <_  W )  ->  E. i  e.  (
1 ... M ) B  <_  W )
360344, 358, 359syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  E. i  e.  ( 1 ... M ) B  <_  W )
361 idd 22 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ( 1 ... M )  ->  ( B  <_  W  ->  B  <_  W ) )
362361rexlimiv 2767 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E. i  e.  ( 1 ... M ) B  <_  W  ->  B  <_  W )
363360, 362syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  <_  W )
36413nnzd 10306 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  W  e.  ZZ )
365 fznn 11045 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( W  e.  ZZ  ->  ( B  e.  ( 1 ... W )  <->  ( B  e.  NN  /\  B  <_  W ) ) )
366364, 365syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( B  e.  ( 1 ... W )  <-> 
( B  e.  NN  /\  B  <_  W )
) )
36717, 363, 366mpbir2and 889 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  B  e.  ( 1 ... W ) )
368367adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  B  e.  ( 1 ... W
) )
369339, 340, 155, 368