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

Theorem vdwlem6 13035
Description: Lemma for vdw 13043. (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 5541 . . . . . . 7  |-  ( G `
 ( B  +  ( E `  i ) ) )  e.  _V
2 vdwlem6.j . . . . . . 7  |-  J  =  ( i  e.  ( 1 ... M ) 
|->  ( G `  ( B  +  ( E `  i ) ) ) )
31, 2fnmpti 5374 . . . . . 6  |-  J  Fn  ( 1 ... M
)
4 fvelrnb 5572 . . . . . 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 . . . . . . . . 9  |-  ( ph  ->  R  e.  Fin )
76adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  R  e.  Fin )
8 vdwlem7.k . . . . . . . . . 10  |-  ( ph  ->  K  e.  ( ZZ>= ` 
2 ) )
9 eluz2b2 10292 . . . . . . . . . . 11  |-  ( K  e.  ( ZZ>= `  2
)  <->  ( K  e.  NN  /\  1  < 
K ) )
109simplbi 446 . . . . . . . . . 10  |-  ( K  e.  ( ZZ>= `  2
)  ->  K  e.  NN )
118, 10syl 15 . . . . . . . . 9  |-  ( ph  ->  K  e.  NN )
1211adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  K  e.  NN )
13 vdwlem3.w . . . . . . . . 9  |-  ( ph  ->  W  e.  NN )
1413adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  W  e.  NN )
15 vdwlem7.g . . . . . . . . 9  |-  ( ph  ->  G : ( 1 ... W ) --> R )
1615adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  G : ( 1 ... W ) --> R )
17 vdwlem6.b . . . . . . . . 9  |-  ( ph  ->  B  e.  NN )
1817adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  B  e.  NN )
19 vdwlem7.m . . . . . . . . 9  |-  ( ph  ->  M  e.  NN )
2019adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  M  e.  NN )
21 vdwlem6.e . . . . . . . . 9  |-  ( ph  ->  E : ( 1 ... M ) --> NN )
2221adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  E : ( 1 ... M ) --> NN )
23 vdwlem6.s . . . . . . . . 9  |-  ( ph  ->  A. i  e.  ( 1 ... M ) ( ( B  +  ( E `  i ) ) (AP `  K
) ( E `  i ) )  C_  ( `' G " { ( G `  ( B  +  ( E `  i ) ) ) } ) )
2423adantr 451 . . . . . . . 8  |-  ( (
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 732 . . . . . . . 8  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  m  e.  ( 1 ... M
) )
26 simprr 733 . . . . . . . . 9  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  ( J `  m )  =  ( G `  B ) )
27 fveq2 5527 . . . . . . . . . . . . 13  |-  ( i  =  m  ->  ( E `  i )  =  ( E `  m ) )
2827oveq2d 5876 . . . . . . . . . . . 12  |-  ( i  =  m  ->  ( B  +  ( E `  i ) )  =  ( B  +  ( E `  m ) ) )
2928fveq2d 5531 . . . . . . . . . . 11  |-  ( i  =  m  ->  ( G `  ( B  +  ( E `  i ) ) )  =  ( G `  ( B  +  ( E `  m )
) ) )
30 fvex 5541 . . . . . . . . . . 11  |-  ( G `
 ( B  +  ( E `  m ) ) )  e.  _V
3129, 2, 30fvmpt 5604 . . . . . . . . . 10  |-  ( m  e.  ( 1 ... M )  ->  ( J `  m )  =  ( G `  ( B  +  ( E `  m )
) ) )
3225, 31syl 15 . . . . . . . . 9  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  ( J `  m )  =  ( G `  ( B  +  ( E `  m )
) ) )
3326, 32eqtr3d 2319 . . . . . . . 8  |-  ( (
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 13030 . . . . . . 7  |-  ( (
ph  /\  ( m  e.  ( 1 ... M
)  /\  ( J `  m )  =  ( G `  B ) ) )  ->  ( K  +  1 ) MonoAP  G )
3534expr 598 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 ... M
) )  ->  (
( J `  m
)  =  ( G `
 B )  -> 
( K  +  1 ) MonoAP  G ) )
3635rexlimdva 2669 . . . . 5  |-  ( ph  ->  ( E. m  e.  ( 1 ... M
) ( J `  m )  =  ( G `  B )  ->  ( K  + 
1 ) MonoAP  G )
)
375, 36syl5bi 208 . . . 4  |-  ( ph  ->  ( ( G `  B )  e.  ran  J  ->  ( K  + 
1 ) MonoAP  G )
)
3837imp 418 . . 3  |-  ( (
ph  /\  ( G `  B )  e.  ran  J )  ->  ( K  +  1 ) MonoAP  G
)
3938olcd 382 . 2  |-  ( (
ph  /\  ( G `  B )  e.  ran  J )  ->  ( <. ( M  +  1 ) ,  K >. PolyAP  H  \/  ( K  +  1
) MonoAP  G ) )
40 vdwlem3.v . . . . . . 7  |-  ( ph  ->  V  e.  NN )
41 vdwlem4.h . . . . . . 7  |-  ( ph  ->  H : ( 1 ... ( W  x.  ( 2  x.  V
) ) ) --> R )
42 vdwlem4.f . . . . . . 7  |-  F  =  ( x  e.  ( 1 ... V ) 
|->  ( y  e.  ( 1 ... W ) 
|->  ( H `  (
y  +  ( W  x.  ( ( x  -  1 )  +  V ) ) ) ) ) )
43 vdwlem7.a . . . . . . 7  |-  ( ph  ->  A  e.  NN )
44 vdwlem7.d . . . . . . 7  |-  ( ph  ->  D  e.  NN )
45 vdwlem7.s . . . . . . 7  |-  ( ph  ->  ( A (AP `  K ) D ) 
C_  ( `' F " { G } ) )
46 vdwlem6.r . . . . . . 7  |-  ( ph  ->  ( # `  ran  J )  =  M )
47 vdwlem6.t . . . . . . 7  |-  T  =  ( B  +  ( W  x.  ( ( A  +  ( V  -  D ) )  -  1 ) ) )
48 vdwlem6.p . . . . . . 7  |-  P  =  ( j  e.  ( 1 ... ( M  +  1 ) ) 
|->  ( if ( j  =  ( M  + 
1 ) ,  0 ,  ( E `  j ) )  +  ( W  x.  D
) ) )
4940, 13, 6, 41, 42, 19, 15, 8, 43, 44, 45, 17, 21, 23, 2, 46, 47, 48vdwlem5 13034 . . . . . 6  |-  ( ph  ->  T  e.  NN )
5049adantr 451 . . . . 5  |-  ( (
ph  /\  -.  ( G `  B )  e.  ran  J )  ->  T  e.  NN )
51 0nn0 9982 . . . . . . . . . 10  |-  0  e.  NN0
5251a1i 10 . . . . . . . . 9  |-  ( ( ( ( ph  /\  -.  ( G `  B
)  e.  ran  J
)  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  /\  j  =  ( M  + 
1 ) )  -> 
0  e.  NN0 )
53 nnuz 10265 . . . . . . . . . . . . . . . . 17  |-  NN  =  ( ZZ>= `  1 )
5419, 53syl6eleq 2375 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
5554adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  ( G `  B )  e.  ran  J )  ->  M  e.  ( ZZ>= ` 
1 ) )
56 elfzp1 10838 . . . . . . . . . . . . . . 15  |-  ( M  e.  ( ZZ>= `  1
)  ->  ( j  e.  ( 1 ... ( M  +  1 ) )  <->  ( j  e.  ( 1 ... M
)  \/  j  =  ( M  +  1 ) ) ) )
5755, 56syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( G `  B )  e.  ran  J )  -> 
( j  e.  ( 1 ... ( M  +  1 ) )  <-> 
( j  e.  ( 1 ... M )  \/  j  =  ( M  +  1 ) ) ) )
5857biimpa 470 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  ( G `  B )  e.  ran  J )  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  ->  ( j  e.  ( 1 ... M
)  \/  j  =  ( M  +  1 ) ) )
5958ord 366 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  ( G `  B )  e.  ran  J )  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  ->  ( -.  j  e.  ( 1 ... M )  -> 
j  =  ( M  +  1 ) ) )
6059con1d 116 . . . . . . . . . . 11  |-  ( ( ( ph  /\  -.  ( G `  B )  e.  ran  J )  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  ->  ( -.  j  =  ( M  +  1 )  -> 
j  e.  ( 1 ... M ) ) )
6160imp 418 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  -.  ( G `  B
)  e.  ran  J
)  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  /\  -.  j  =  ( M  +  1 ) )  ->  j  e.  ( 1 ... M ) )
6221ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  ( G `  B )  e.  ran  J )  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  ->  E :
( 1 ... M
) --> NN )
63 ffvelrn 5665 . . . . . . . . . . . 12  |-  ( ( E : ( 1 ... M ) --> NN 
/\  j  e.  ( 1 ... M ) )  ->  ( E `  j )  e.  NN )
6462, 63sylan 457 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  -.  ( G `  B
)  e.  ran  J
)  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  /\  j  e.  ( 1 ... M
) )  ->  ( E `  j )  e.  NN )
6564nnnn0d 10020 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  -.  ( G `  B
)  e.  ran  J
)  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  /\  j  e.  ( 1 ... M
) )  ->  ( E `  j )  e.  NN0 )
6661, 65syldan 456 . . . . . . . . 9  |-  ( ( ( ( ph  /\  -.  ( G `  B
)  e.  ran  J
)  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  /\  -.  j  =  ( M  +  1 ) )  ->  ( E `  j )  e.  NN0 )
6752, 66ifclda 3594 . . . . . . . 8  |-  ( ( ( ph  /\  -.  ( G `  B )  e.  ran  J )  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  ->  if (
j  =  ( M  +  1 ) ,  0 ,  ( E `
 j ) )  e.  NN0 )
6813, 44nnmulcld 9795 . . . . . . . . 9  |-  ( ph  ->  ( W  x.  D
)  e.  NN )
6968ad2antrr 706 . . . . . . . 8  |-  ( ( ( ph  /\  -.  ( G `  B )  e.  ran  J )  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  ->  ( W  x.  D )  e.  NN )
70 nn0nnaddcl 9998 . . . . . . . 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 )
7167, 69, 70syl2anc 642 . . . . . . 7  |-  ( ( ( ph  /\  -.  ( G `  B )  e.  ran  J )  /\  j  e.  ( 1 ... ( M  +  1 ) ) )  ->  ( if ( j  =  ( M  +  1 ) ,  0 ,  ( E `  j ) )  +  ( W  x.  D ) )  e.  NN )
7271, 48fmptd 5686 . . . . . 6  |-  ( (
ph  /\  -.  ( G `  B )  e.  ran  J )  ->  P : ( 1 ... ( M  +  1 ) ) --> NN )
73 nnex 9754 . . . . . . 7  |-  NN  e.  _V
74 ovex 5885 . . . . . . 7  |-  ( 1 ... ( M  + 
1 ) )  e. 
_V
7573, 74elmap 6798 . . . . . 6  |-  ( P  e.  ( NN  ^m  ( 1 ... ( M  +  1 ) ) )  <->  P :
( 1 ... ( M  +  1 ) ) --> NN )
7672, 75sylibr 203 . . . . 5  |-  ( (
ph  /\  -.  ( G `  B )  e.  ran  J )  ->  P  e.  ( NN  ^m  ( 1 ... ( M  +  1 ) ) ) )
77 elfzp1 10838 . . . . . . . . . 10  |-  ( M  e.  ( ZZ>= `  1
)  ->  ( i  e.  ( 1 ... ( M  +  1 ) )  <->  ( i  e.  ( 1 ... M
)  \/  i  =  ( M  +  1 ) ) ) )
7854, 77syl 15 . . . . . . . . 9  |-  ( ph  ->  ( i  e.  ( 1 ... ( M  +  1 ) )  <-> 
( i  e.  ( 1 ... M )  \/  i  =  ( M  +  1 ) ) ) )
7917adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  B  e.  NN )
8079nncnd 9764 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  B  e.  CC )
8180adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  B  e.  CC )
82 ffvelrn 5665 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( E : ( 1 ... M ) --> NN 
/\  i  e.  ( 1 ... M ) )  ->  ( E `  i )  e.  NN )
8321, 82sylan 457 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( E `  i )  e.  NN )
8483nncnd 9764 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( E `  i )  e.  CC )
8584adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( E `  i )  e.  CC )
8681, 85addcld 8856 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( B  +  ( E `  i ) )  e.  CC )
87 nnm1nn0 10007 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  e.  NN  ->  ( A  -  1 )  e.  NN0 )
8843, 87syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( A  -  1 )  e.  NN0 )
89 nn0nnaddcl 9998 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( A  -  1 )  e.  NN0  /\  V  e.  NN )  ->  ( ( A  - 
1 )  +  V
)  e.  NN )
9088, 40, 89syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( A  - 
1 )  +  V
)  e.  NN )
9113, 90nnmulcld 9795 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( W  x.  (
( A  -  1 )  +  V ) )  e.  NN )
9291nncnd 9764 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( W  x.  (
( A  -  1 )  +  V ) )  e.  CC )
9392ad2antrr 706 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  x.  ( ( A  -  1 )  +  V ) )  e.  CC )
94 elfznn0 10824 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  ( 0 ... ( K  -  1 ) )  ->  m  e.  NN0 )
9594adantl 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  m  e.  NN0 )
9695nn0cnd 10022 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  m  e.  CC )
9796adantlr 695 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  m  e.  CC )
9897, 85mulcld 8857 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  ( E `
 i ) )  e.  CC )
9968nnnn0d 10020 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( W  x.  D
)  e.  NN0 )
10099adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  x.  D )  e.  NN0 )
10195, 100nn0mulcld 10025 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  ( W  x.  D ) )  e.  NN0 )
102101nn0cnd 10022 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  ( W  x.  D ) )  e.  CC )
103102adantlr 695 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  ( W  x.  D ) )  e.  CC )
10486, 93, 98, 103add4d 9037 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
10568nncnd 9764 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( W  x.  D
)  e.  CC )
106105ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  x.  D )  e.  CC )
10797, 85, 106adddid 8861 . . . . . . . . . . . . . . . . . . . 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 )
) ) )
108107oveq2d 5876 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
10913nncnd 9764 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  W  e.  CC )
110109adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  W  e.  CC )
11190nncnd 9764 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( A  - 
1 )  +  V
)  e.  CC )
112111adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  -  1 )  +  V )  e.  CC )
11344nncnd 9764 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  D  e.  CC )
114113adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  D  e.  CC )
11596, 114mulcld 8857 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  D )  e.  CC )
116110, 112, 115adddid 8861 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
11743nncnd 9764 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  A  e.  CC )
118117adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  A  e.  CC )
119 ax-1cn 8797 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  1  e.  CC
120119a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  1  e.  CC )
121118, 115, 120addsubd 9180 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  +  ( m  x.  D ) )  -  1 )  =  ( ( A  -  1 )  +  ( m  x.  D
) ) )
122121oveq1d 5875 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V )  =  ( ( ( A  -  1 )  +  ( m  x.  D ) )  +  V ) )
12388nn0cnd 10022 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( A  -  1 )  e.  CC )
124123adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  -  1 )  e.  CC )
12540nncnd 9764 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  V  e.  CC )
126125adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  V  e.  CC )
127124, 115, 126add32d 9036 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( A  - 
1 )  +  ( m  x.  D ) )  +  V )  =  ( ( ( A  -  1 )  +  V )  +  ( m  x.  D
) ) )
128122, 127eqtrd 2317 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V )  =  ( ( ( A  -  1 )  +  V )  +  ( m  x.  D
) ) )
129128oveq2d 5876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  x.  ( (
( A  +  ( m  x.  D ) )  -  1 )  +  V ) )  =  ( W  x.  ( ( ( A  -  1 )  +  V )  +  ( m  x.  D ) ) ) )
13096, 110, 114mul12d 9023 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  ( W  x.  D ) )  =  ( W  x.  ( m  x.  D
) ) )
131130oveq2d 5876 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
132116, 129, 1313eqtr4d 2327 . . . . . . . . . . . . . . . . . . . . 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 )
) ) )
133132adantlr 695 . . . . . . . . . . . . . . . . . . . 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 )
) ) )
134133oveq2d 5876 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
135104, 108, 1343eqtr4d 2327 . . . . . . . . . . . . . . . . . 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 ) ) ) )
13640ad2antrr 706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  V  e.  NN )
13713ad2antrr 706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  W  e.  NN )
13845adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A (AP `  K ) D )  C_  ( `' F " { G } ) )
139 eqid 2285 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  +  ( m  x.  D ) )  =  ( A  +  ( m  x.  D ) )
140 oveq1 5867 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  m  ->  (
n  x.  D )  =  ( m  x.  D ) )
141140oveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  m  ->  ( A  +  ( n  x.  D ) )  =  ( A  +  ( m  x.  D ) ) )
142141eqeq2d 2296 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  m  ->  (
( A  +  ( m  x.  D ) )  =  ( A  +  ( n  x.  D ) )  <->  ( A  +  ( m  x.  D ) )  =  ( A  +  ( m  x.  D ) ) ) )
143142rspcev 2886 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
144139, 143mpan2 652 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  ( 0 ... ( K  -  1 ) )  ->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( A  +  ( m  x.  D
) )  =  ( A  +  ( n  x.  D ) ) )
14511nnnn0d 10020 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  K  e.  NN0 )
146 vdwapval 13022 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
147145, 43, 44, 146syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
148147biimpar 471 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
149144, 148sylan2 460 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( A (AP `  K ) D ) )
150138, 149sseldd 3183 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( `' F " { G } ) )
15140, 13, 6, 41, 42vdwlem4 13033 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  F : ( 1 ... V ) --> ( R  ^m  ( 1 ... W ) ) )
152 ffn 5391 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F : ( 1 ... V ) --> ( R  ^m  ( 1 ... W ) )  ->  F  Fn  ( 1 ... V ) )
153151, 152syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  F  Fn  ( 1 ... V ) )
154 fniniseg 5648 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
155153, 154syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( A  +  ( m  x.  D
) )  e.  ( `' F " { G } )  <->  ( ( A  +  ( m  x.  D ) )  e.  ( 1 ... V
)  /\  ( F `  ( A  +  ( m  x.  D ) ) )  =  G ) ) )
156155biimpa 470 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( A  +  ( m  x.  D ) )  e.  ( `' F " { G } ) )  ->  ( ( A  +  ( m  x.  D ) )  e.  ( 1 ... V
)  /\  ( F `  ( A  +  ( m  x.  D ) ) )  =  G ) )
157150, 156syldan 456 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  +  ( m  x.  D ) )  e.  ( 1 ... V )  /\  ( F `  ( A  +  ( m  x.  D ) ) )  =  G ) )
158157simpld 445 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( 1 ... V
) )
159158adantlr 695 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( 1 ... V
) )
16023r19.21bi 2643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( B  +  ( E `  i ) ) (AP `  K
) ( E `  i ) )  C_  ( `' G " { ( G `  ( B  +  ( E `  i ) ) ) } ) )
161160adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( B  +  ( E `  i ) ) (AP `  K
) ( E `  i ) )  C_  ( `' G " { ( G `  ( B  +  ( E `  i ) ) ) } ) )
162 eqid 2285 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( B  +  ( E `
 i ) )  +  ( m  x.  ( E `  i
) ) )  =  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )
163 oveq1 5867 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  m  ->  (
n  x.  ( E `
 i ) )  =  ( m  x.  ( E `  i
) ) )
164163oveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  m  ->  (
( B  +  ( E `  i ) )  +  ( n  x.  ( E `  i ) ) )  =  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) ) )
165164eqeq2d 2296 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
166165rspcev 2886 . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) )
167162, 166mpan2 652 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
16811adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  K  e.  NN )
169168nnnn0d 10020 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  K  e.  NN0 )
17079, 83nnaddcld 9794 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( B  +  ( E `  i ) )  e.  NN )
171 vdwapval 13022 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
172169, 170, 83, 171syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )
173172biimpar 471 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
174167, 173sylan2 460 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
175161, 174sseldd 3183 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  e.  ( `' G " { ( G `  ( B  +  ( E `  i )
) ) } ) )
176 ffn 5391 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( G : ( 1 ... W ) --> R  ->  G  Fn  ( 1 ... W ) )
17715, 176syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  G  Fn  ( 1 ... W ) )
178177adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  G  Fn  ( 1 ... W
) )
179 fniniseg 5648 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
180178, 179syl 15 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
181180biimpa 470 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
182175, 181syldan 456 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
183182simpld 445 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i ) ) )  e.  ( 1 ... W ) )
184136, 137, 159, 183vdwlem3 13032 . . . . . . . . . . . . . . . . . 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 ) ) ) )
185135, 184eqeltrd 2359 . . . . . . . . . . . . . . . . 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 ) ) ) )
186 oveq1 5867 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
187186fveq2d 5531 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
188 eqid 2285 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
189 fvex 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( H `
 ( ( ( B  +  ( E `
 i ) )  +  ( m  x.  ( E `  i
) ) )  +  ( W  x.  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V ) ) ) )  e. 
_V
190187, 188, 189fvmpt 5604 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
191183, 190syl 15 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
192182simprd 449 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 1 ... M
) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( G `  ( ( B  +  ( E `  i ) )  +  ( m  x.  ( E `  i )
) ) )  =  ( G `  ( B  +  ( E `  i ) ) ) )
193157simprd 449 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( F `  ( A  +  ( m  x.  D ) ) )  =  G )
194 oveq1 5867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  (
x  -  1 )  =  ( ( A  +  ( m  x.  D ) )  - 
1 ) )
195194oveq1d 5875 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  (
( x  -  1 )  +  V )  =  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) )
196195oveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  ( W  x.  ( (
x  -  1 )  +  V ) )  =  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  - 
1 )  +  V
) ) )
197196oveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  (
y  +  ( W  x.  ( ( x  -  1 )  +  V ) ) )  =  ( y  +  ( W  x.  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V ) ) ) )
198197fveq2d 5531 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  ( H `  ( y  +  ( W  x.  ( ( x  - 
1 )  +  V
) ) ) )  =  ( H `  ( y  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) ) ) )
199198mpteq2dv 4109 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
200 ovex 5885 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1 ... W )  e. 
_V
201200mptex 5748 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( ( A  +  ( m  x.  D
) )  -  1 )  +  V ) ) ) ) )  e.  _V
202199, 42, 201fvmpt 5604 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
203158, 202syl 15 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
204193, 203eqtr3d 2319 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  G  =  ( y  e.  ( 1 ... W
)  |->  ( H `  ( y  +  ( W  x.  ( ( ( A  +  ( m  x.  D ) )  -  1 )  +  V ) ) ) ) ) )
205204adantlr 695 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
206205fveq1d 5529 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
207192, 206eqtr3d 2319 . . . . . . . . . . . . . . . . . 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 )
) ) ) )
208135fveq2d 5531 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
209191, 207, 2083eqtr4rd 2328 . . . . . . . . . . . . . . . . 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 )
) ) )
210185, 209jca 518 . . . . . . . . . . . . . . . 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 )
) ) ) )
211 eleq1 2345 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
212 fveq2 5527 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
213212eqeq1d 2293 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
214211, 213anbi12d 691 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
215210, 214syl5ibrcom 213 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
216215rexlimdva 2669 . . . . . . . . . . . . . 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 )
) ) ) ) )
21791adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( W  x.  ( ( A  -  1 )  +  V ) )  e.  NN )
218170, 217nnaddcld 9794 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  e.  NN )
21968adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( W  x.  D )  e.  NN )
22083, 219nnaddcld 9794 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( E `  i
)  +  ( W  x.  D ) )  e.  NN )
221 vdwapval 13022 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
222169, 218, 220, 221syl3anc 1182 . . . . . . . . . . . . . 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 ) ) ) ) ) )
223 ffn 5391 . . . . . . . . . . . . . . . . 17  |-  ( H : ( 1 ... ( W  x.  (
2  x.  V ) ) ) --> R  ->  H  Fn  ( 1 ... ( W  x.  ( 2  x.  V
) ) ) )
22441, 223syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  H  Fn  ( 1 ... ( W  x.  ( 2  x.  V
) ) ) )
225224adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  H  Fn  ( 1 ... ( W  x.  ( 2  x.  V ) ) ) )
226 fniniseg 5648 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
227225, 226syl 15 . . . . . . . . . . . . . 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 ) ) ) ) ) )
228216, 222, 2273imtr4d 259 . . . . . . . . . . . . 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 )
) ) } ) ) )
229228ssrdv 3187 . . . . . . . . . . . 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 ) ) ) } ) )
230 ssun1 3340 . . . . . . . . . . . . . . . . . . 19  |-  ( 1 ... M )  C_  ( ( 1 ... M )  u.  {
( M  +  1 ) } )
231 fzsuc 10837 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  e.  ( ZZ>= `  1
)  ->  ( 1 ... ( M  + 
1 ) )  =  ( ( 1 ... M )  u.  {
( M  +  1 ) } ) )
23254, 231syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( 1 ... ( M  +  1 ) )  =  ( ( 1 ... M )  u.  { ( M  +  1 ) } ) )
233230, 232syl5sseqr 3229 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 1 ... M
)  C_  ( 1 ... ( M  + 
1 ) ) )
234233sselda 3182 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  i  e.  ( 1 ... ( M  +  1 ) ) )
235 eqeq1 2291 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  i  ->  (
j  =  ( M  +  1 )  <->  i  =  ( M  +  1
) ) )
236 fveq2 5527 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  i  ->  ( E `  j )  =  ( E `  i ) )
237235, 236ifbieq2d 3587 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  i  ->  if ( j  =  ( M  +  1 ) ,  0 ,  ( E `  j ) )  =  if ( i  =  ( M  +  1 ) ,  0 ,  ( E `
 i ) ) )
238237oveq1d 5875 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  i  ->  ( if ( j  =  ( M  +  1 ) ,  0 ,  ( E `  j ) )  +  ( W  x.  D ) )  =  ( if ( i  =  ( M  +  1 ) ,  0 ,  ( E `
 i ) )  +  ( W  x.  D ) ) )
239 ovex 5885 . . . . . . . . . . . . . . . . . 18  |-  ( if ( i  =  ( M  +  1 ) ,  0 ,  ( E `  i ) )  +  ( W  x.  D ) )  e.  _V
240238, 48, 239fvmpt 5604 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... ( M  +  1 ) )  ->  ( P `  i )  =  ( if ( i  =  ( M  +  1 ) ,  0 ,  ( E `
 i ) )  +  ( W  x.  D ) ) )
241234, 240syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( P `  i )  =  ( if ( i  =  ( M  +  1 ) ,  0 ,  ( E `
 i ) )  +  ( W  x.  D ) ) )
242 elfzle2 10802 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... M )  ->  i  <_  M )
24319nnred 9763 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  M  e.  RR )
244243ltp1d 9689 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  M  <  ( M  +  1 ) )
245 peano2re 8987 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( M  e.  RR  ->  ( M  +  1 )  e.  RR )
246243, 245syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( M  +  1 )  e.  RR )
247243, 246ltnled 8968 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( M  <  ( M  +  1 )  <->  -.  ( M  +  1 )  <_  M )
)
248244, 247mpbid 201 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  -.  ( M  + 
1 )  <_  M
)
249 breq1 4028 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  ( M  + 
1 )  ->  (
i  <_  M  <->  ( M  +  1 )  <_  M ) )
250249notbid 285 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  =  ( M  + 
1 )  ->  ( -.  i  <_  M  <->  -.  ( M  +  1 )  <_  M ) )
251248, 250syl5ibrcom 213 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( i  =  ( M  +  1 )  ->  -.  i  <_  M ) )
252251con2d 107 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( i  <_  M  ->  -.  i  =  ( M  +  1 ) ) )
253242, 252syl5 28 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( i  e.  ( 1 ... M )  ->  -.  i  =  ( M  +  1
) ) )
254253imp 418 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  -.  i  =  ( M  +  1 ) )
255 iffalse 3574 . . . . . . . . . . . . . . . . . 18  |-  ( -.  i  =  ( M  +  1 )  ->  if ( i  =  ( M  +  1 ) ,  0 ,  ( E `  i ) )  =  ( E `
 i ) )
256255oveq1d 5875 . . . . . . . . . . . . . . . . 17  |-  ( -.  i  =  ( M  +  1 )  -> 
( if ( i  =  ( M  + 
1 ) ,  0 ,  ( E `  i ) )  +  ( W  x.  D
) )  =  ( ( E `  i
)  +  ( W  x.  D ) ) )
257254, 256syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( if ( i  =  ( M  +  1 ) ,  0 ,  ( E `  i ) )  +  ( W  x.  D ) )  =  ( ( E `
 i )  +  ( W  x.  D
) ) )
258241, 257eqtrd 2317 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( P `  i )  =  ( ( E `
 i )  +  ( W  x.  D
) ) )
259258oveq2d 5876 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( T  +  ( P `  i ) )  =  ( T  +  ( ( E `  i
)  +  ( W  x.  D ) ) ) )
26049nncnd 9764 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  e.  CC )
261260adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  T  e.  CC )
262105adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( W  x.  D )  e.  CC )
263261, 84, 262add12d 9035 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( T  +  ( ( E `  i )  +  ( W  x.  D ) ) )  =  ( ( E `
 i )  +  ( T  +  ( W  x.  D ) ) ) )
26447oveq1i 5870 . . . . . . . . . . . . . . . . . 18  |-  ( T  +  ( W  x.  D ) )  =  ( ( B  +  ( W  x.  (
( A  +  ( V  -  D ) )  -  1 ) ) )  +  ( W  x.  D ) )
26517nncnd 9764 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  B  e.  CC )
266125, 113subcld 9159 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( V  -  D
)  e.  CC )
267117, 266addcld 8856 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( A  +  ( V  -  D ) )  e.  CC )
268 subcl 9053 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  +  ( V  -  D ) )  e.  CC  /\  1  e.  CC )  ->  ( ( A  +  ( V  -  D
) )  -  1 )  e.  CC )
269267, 119, 268sylancl 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( A  +  ( V  -  D
) )  -  1 )  e.  CC )
270109, 269mulcld 8857 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( W  x.  (
( A  +  ( V  -  D ) )  -  1 ) )  e.  CC )
271265, 270, 105addassd 8859 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( B  +  ( W  x.  (
( A  +  ( V  -  D ) )  -  1 ) ) )  +  ( W  x.  D ) )  =  ( B  +  ( ( W  x.  ( ( A  +  ( V  -  D ) )  - 
1 ) )  +  ( W  x.  D
) ) ) )
272109, 269, 113adddid 8861 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( W  x.  (
( ( A  +  ( V  -  D
) )  -  1 )  +  D ) )  =  ( ( W  x.  ( ( A  +  ( V  -  D ) )  -  1 ) )  +  ( W  x.  D ) ) )
273117, 266, 113addassd 8859 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( A  +  ( V  -  D
) )  +  D
)  =  ( A  +  ( ( V  -  D )  +  D ) ) )
274125, 113npcand 9163 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( V  -  D )  +  D
)  =  V )
275274oveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( A  +  ( ( V  -  D
)  +  D ) )  =  ( A  +  V ) )
276273, 275eqtrd 2317 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( A  +  ( V  -  D
) )  +  D
)  =  ( A  +  V ) )
277276oveq1d 5875 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( A  +  ( V  -  D ) )  +  D )  -  1 )  =  ( ( A  +  V )  -  1 ) )
278119a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  1  e.  CC )
279267, 113, 278addsubd 9180 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( A  +  ( V  -  D ) )  +  D )  -  1 )  =  ( ( ( A  +  ( V  -  D ) )  -  1 )  +  D ) )
280117, 125, 278addsubd 9180 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( A  +  V )  -  1 )  =  ( ( A  -  1 )  +  V ) )
281277, 279, 2803eqtr3d 2325 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( A  +  ( V  -  D ) )  - 
1 )  +  D
)  =  ( ( A  -  1 )  +  V ) )
282281oveq2d 5876 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( W  x.  (
( ( A  +  ( V  -  D
) )  -  1 )  +  D ) )  =  ( W  x.  ( ( A  -  1 )  +  V ) ) )
283272, 282eqtr3d 2319 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( W  x.  ( ( A  +  ( V  -  D
) )  -  1 ) )  +  ( W  x.  D ) )  =  ( W  x.  ( ( A  -  1 )  +  V ) ) )
284283oveq2d 5876 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( B  +  ( ( W  x.  (
( A  +  ( V  -  D ) )  -  1 ) )  +  ( W  x.  D ) ) )  =  ( B  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) ) )
285271, 284eqtrd 2317 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  +  ( W  x.  (
( A  +  ( V  -  D ) )  -  1 ) ) )  +  ( W  x.  D ) )  =  ( B  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) ) )
286264, 285syl5eq 2329 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( T  +  ( W  x.  D ) )  =  ( B  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) ) )
287286oveq2d 5876 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( E `  i )  +  ( T  +  ( W  x.  D ) ) )  =  ( ( E `  i )  +  ( B  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) )
288287adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( E `  i
)  +  ( T  +  ( W  x.  D ) ) )  =  ( ( E `
 i )  +  ( B  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) )
28992adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( W  x.  ( ( A  -  1 )  +  V ) )  e.  CC )
29084, 80, 289addassd 8859 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( E `  i )  +  B
)  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  =  ( ( E `
 i )  +  ( B  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) )
29184, 80addcomd 9016 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( E `  i
)  +  B )  =  ( B  +  ( E `  i ) ) )
292291oveq1d 5875 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( E `  i )  +  B
)  +  ( W  x.  ( ( A  -  1 )  +  V ) ) )  =  ( ( B  +  ( E `  i ) )  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) )
293288, 290, 2923eqtr2d 2323 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( E `  i
)  +  ( T  +  ( W  x.  D ) ) )  =  ( ( B  +  ( E `  i ) )  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) )
294259, 263, 2933eqtrd 2321 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( T  +  ( P `  i ) )  =  ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) )
295294, 258oveq12d 5878 . . . . . . . . . . . 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 ) ) ) )
296 cnvimass 5035 . . . . . . . . . . . . . . . . . . 19  |-  ( `' G " { ( G `  ( B  +  ( E `  i ) ) ) } )  C_  dom  G
297 fdm 5395 . . . . . . . . . . . . . . . . . . . 20  |-  ( G : ( 1 ... W ) --> R  ->  dom  G  =  ( 1 ... W ) )
29815, 297syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  dom  G  =  ( 1 ... W ) )
299296, 298syl5sseq 3228 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( `' G " { ( G `  ( B  +  ( E `  i )
) ) } ) 
C_  ( 1 ... W ) )
300299adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( `' G " { ( G `  ( B  +  ( E `  i ) ) ) } )  C_  (
1 ... W ) )
301 vdwapid1 13024 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  NN  /\  ( B  +  ( E `  i )
)  e.  NN  /\  ( E `  i )  e.  NN )  -> 
( B  +  ( E `  i ) )  e.  ( ( B  +  ( E `
 i ) ) (AP `  K ) ( E `  i
) ) )
302168, 170, 83, 301syl3anc 1182 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( B  +  ( E `  i ) )  e.  ( ( B  +  ( E `  i ) ) (AP `  K
) ( E `  i ) ) )
303160, 302sseldd 3183 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( B  +  ( E `  i ) )  e.  ( `' G " { ( G `  ( B  +  ( E `  i )
) ) } ) )
304300, 303sseldd 3183 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( B  +  ( E `  i ) )  e.  ( 1 ... W
) )
305 oveq1 5867 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( B  +  ( E `  i ) )  ->  ( y  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) )  =  ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) )
306305fveq2d 5531 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( B  +  ( E `  i ) )  ->  ( H `  ( y  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) )  =  ( H `  ( ( B  +  ( E `
 i ) )  +  ( W  x.  ( ( A  - 
1 )  +  V
) ) ) ) )
307 eqid 2285 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) )  =  ( y  e.  ( 1 ... W
)  |->  ( H `  ( y  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) )
308 fvex 5541 . . . . . . . . . . . . . . . . 17  |-  ( H `
 ( ( B  +  ( E `  i ) )  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) )  e. 
_V
309306, 307, 308fvmpt 5604 . . . . . . . . . . . . . . . 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 ) ) ) ) )
310304, 309syl 15 . . . . . . . . . . . . . . 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 ) ) ) ) )
311 vdwapid1 13024 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( K  e.  NN  /\  A  e.  NN  /\  D  e.  NN )  ->  A  e.  ( A (AP `  K ) D ) )
31211, 43, 44, 311syl3anc 1182 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  e.  ( A (AP `  K ) D ) )
31345, 312sseldd 3183 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A  e.  ( `' F " { G } ) )
314 fniniseg 5648 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F  Fn  ( 1 ... V )  ->  ( A  e.  ( `' F " { G }
)  <->  ( A  e.  ( 1 ... V
)  /\  ( F `  A )  =  G ) ) )
315153, 314syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( A  e.  ( `' F " { G } )  <->  ( A  e.  ( 1 ... V
)  /\  ( F `  A )  =  G ) ) )
316313, 315mpbid 201 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( A  e.  ( 1 ... V )  /\  ( F `  A )  =  G ) )
317316simprd 449 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( F `  A
)  =  G )
318316simpld 445 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  ( 1 ... V ) )
319 oveq1 5867 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  A  ->  (
x  -  1 )  =  ( A  - 
1 ) )
320319oveq1d 5875 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  A  ->  (
( x  -  1 )  +  V )  =  ( ( A  -  1 )  +  V ) )
321320oveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  A  ->  ( W  x.  ( (
x  -  1 )  +  V ) )  =  ( W  x.  ( ( A  - 
1 )  +  V
) ) )
322321oveq2d 5876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  A  ->  (
y  +  ( W  x.  ( ( x  -  1 )  +  V ) ) )  =  ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) )
323322fveq2d 5531 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  A  ->  ( H `  ( y  +  ( W  x.  ( ( x  - 
1 )  +  V
) ) ) )  =  ( H `  ( y  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) )
324323mpteq2dv 4109 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
325200mptex 5748 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) )  e.  _V
326324, 42, 325fvmpt 5604 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  ( 1 ... V )  ->  ( F `  A )  =  ( y  e.  ( 1 ... W
)  |->  ( H `  ( y  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) ) )
327318, 326syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( F `  A
)  =  ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) ) )
328317, 327eqtr3d 2319 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  G  =  ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) ) )
329328fveq1d 5529 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( G `  ( B  +  ( E `  i ) ) )  =  ( ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) ) `
 ( B  +  ( E `  i ) ) ) )
330329adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( G `  ( B  +  ( E `  i ) ) )  =  ( ( y  e.  ( 1 ... W )  |->  ( H `
 ( y  +  ( W  x.  (
( A  -  1 )  +  V ) ) ) ) ) `
 ( B  +  ( E `  i ) ) ) )
331294fveq2d 5531 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( H `  ( T  +  ( P `  i ) ) )  =  ( H `  ( ( B  +  ( E `  i ) )  +  ( W  x.  ( ( A  -  1 )  +  V ) ) ) ) )
332310, 330, 3313eqtr4rd 2328 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( H `  ( T  +  ( P `  i ) ) )  =  ( G `  ( B  +  ( E `  i )
) ) )
333332sneqd 3655 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  { ( H `  ( T  +  ( P `  i ) ) ) }  =  { ( G `  ( B  +  ( E `  i ) ) ) } )
334333imaeq2d 5014 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( `' H " { ( H `  ( T  +  ( P `  i ) ) ) } )  =  ( `' H " { ( G `  ( B  +  ( E `  i ) ) ) } ) )
335229, 295, 3343sstr4d 3223 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( T  +  ( P `  i ) ) (AP `  K
) ( P `  i ) )  C_  ( `' H " { ( H `  ( T  +  ( P `  i ) ) ) } ) )
336335ex 423 . . . . . . . . . 10  |-  ( ph  ->  ( i  e.  ( 1 ... M )  ->  ( ( T  +  ( P `  i ) ) (AP
`  K ) ( P `  i ) )  C_  ( `' H " { ( H `
 ( T  +  ( P `  i ) ) ) } ) ) )
337265adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  B  e.  CC )
33892adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  x.  ( ( A  -  1 )  +  V ) )  e.  CC )
339337, 338, 102addassd 8859 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
340132oveq2d 5876 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
341339, 340eqtr4d 2320 . . . . . . . . . . . . . . . . . 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 ) ) ) )
34240adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  V  e.  NN )
34313adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  W  e.  NN )
344 eluzfz1 10805 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... M
) )
34554, 344syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  1  e.  ( 1 ... M ) )
346 ne0i 3463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1  e.  ( 1 ... M )  ->  (
1 ... M )  =/=  (/) )
347345, 346syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 1 ... M
)  =/=  (/) )
348 elfzuz3 10797 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( B  +  ( E `
 i ) )  e.  ( 1 ... W )  ->  W  e.  ( ZZ>= `  ( B  +  ( E `  i ) ) ) )
349304, 348syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  W  e.  ( ZZ>= `  ( B  +  ( E `  i ) ) ) )
35017nnzd 10118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  B  e.  ZZ )
351 uzid 10244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( B  e.  ZZ  ->  B  e.  ( ZZ>= `  B )
)
352350, 351syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  B  e.  ( ZZ>= `  B ) )
353352adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  B  e.  ( ZZ>= `  B )
)
35483nnnn0d 10020 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( E `  i )  e.  NN0 )
355 uzaddcl 10277 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( B  e.  ( ZZ>= `  B )  /\  ( E `  i )  e.  NN0 )  ->  ( B  +  ( E `  i ) )  e.  ( ZZ>= `  B )
)
356353, 354, 355syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( B  +  ( E `  i ) )  e.  ( ZZ>= `  B )
)
357 uztrn 10246 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( W  e.  ( ZZ>= `  ( B  +  ( E `  i )
) )  /\  ( B  +  ( E `  i ) )  e.  ( ZZ>= `  B )
)  ->  W  e.  ( ZZ>= `  B )
)
358349, 356, 357syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  W  e.  ( ZZ>= `  B )
)
359 eluzle 10242 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( W  e.  ( ZZ>= `  B
)  ->  B  <_  W )
360358, 359syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  B  <_  W )
361360ralrimiva 2628 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A. i  e.  ( 1 ... M ) B  <_  W )
362 r19.2z 3545 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 1 ... M
)  =/=  (/)  /\  A. i  e.  ( 1 ... M ) B  <_  W )  ->  E. i  e.  (
1 ... M ) B  <_  W )
363347, 361, 362syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  E. i  e.  ( 1 ... M ) B  <_  W )
364 idd 21 . . . . . . . . . . . . . . . . . . . . . . 23  |-