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

Theorem vdwlem8 14881
Description: Lemma for vdw 14887. (Contributed by Mario Carneiro, 18-Aug-2014.)
Hypotheses
Ref Expression
vdwlem8.r  |-  ( ph  ->  R  e.  Fin )
vdwlem8.k  |-  ( ph  ->  K  e.  ( ZZ>= ` 
2 ) )
vdwlem8.w  |-  ( ph  ->  W  e.  NN )
vdwlem8.f  |-  ( ph  ->  F : ( 1 ... ( 2  x.  W ) ) --> R )
vdwlem8.c  |-  C  e. 
_V
vdwlem8.a  |-  ( ph  ->  A  e.  NN )
vdwlem8.d  |-  ( ph  ->  D  e.  NN )
vdwlem8.s  |-  ( ph  ->  ( A (AP `  K ) D ) 
C_  ( `' G " { C } ) )
vdwlem8.g  |-  G  =  ( x  e.  ( 1 ... W ) 
|->  ( F `  (
x  +  W ) ) )
Assertion
Ref Expression
vdwlem8  |-  ( ph  -> 
<. 1 ,  K >. PolyAP 
F )
Distinct variable groups:    x, A    x, D    x, F    ph, x    x, C    x, K    x, W
Allowed substitution hints:    R( x)    G( x)

Proof of Theorem vdwlem8
Dummy variables  a 
d  i  m  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vdwlem8.a . . . . . . . . . 10  |-  ( ph  ->  A  e.  NN )
21nncnd 10576 . . . . . . . . 9  |-  ( ph  ->  A  e.  CC )
3 vdwlem8.d . . . . . . . . . 10  |-  ( ph  ->  D  e.  NN )
43nncnd 10576 . . . . . . . . 9  |-  ( ph  ->  D  e.  CC )
52, 4addcomd 9786 . . . . . . . 8  |-  ( ph  ->  ( A  +  D
)  =  ( D  +  A ) )
65oveq2d 6265 . . . . . . 7  |-  ( ph  ->  ( W  -  ( A  +  D )
)  =  ( W  -  ( D  +  A ) ) )
7 vdwlem8.w . . . . . . . . 9  |-  ( ph  ->  W  e.  NN )
87nncnd 10576 . . . . . . . 8  |-  ( ph  ->  W  e.  CC )
98, 4, 2subsub4d 9968 . . . . . . 7  |-  ( ph  ->  ( ( W  -  D )  -  A
)  =  ( W  -  ( D  +  A ) ) )
106, 9eqtr4d 2465 . . . . . 6  |-  ( ph  ->  ( W  -  ( A  +  D )
)  =  ( ( W  -  D )  -  A ) )
1110oveq2d 6265 . . . . 5  |-  ( ph  ->  ( ( A  +  A )  +  ( W  -  ( A  +  D ) ) )  =  ( ( A  +  A )  +  ( ( W  -  D )  -  A ) ) )
128, 4subcld 9937 . . . . . 6  |-  ( ph  ->  ( W  -  D
)  e.  CC )
132, 2, 12ppncand 9977 . . . . 5  |-  ( ph  ->  ( ( A  +  A )  +  ( ( W  -  D
)  -  A ) )  =  ( A  +  ( W  -  D ) ) )
1411, 13eqtrd 2462 . . . 4  |-  ( ph  ->  ( ( A  +  A )  +  ( W  -  ( A  +  D ) ) )  =  ( A  +  ( W  -  D ) ) )
151, 1nnaddcld 10607 . . . . 5  |-  ( ph  ->  ( A  +  A
)  e.  NN )
16 vdwlem8.s . . . . . . . 8  |-  ( ph  ->  ( A (AP `  K ) D ) 
C_  ( `' G " { C } ) )
17 cnvimass 5150 . . . . . . . . 9  |-  ( `' G " { C } )  C_  dom  G
18 fvex 5835 . . . . . . . . . 10  |-  ( F `
 ( x  +  W ) )  e. 
_V
19 vdwlem8.g . . . . . . . . . 10  |-  G  =  ( x  e.  ( 1 ... W ) 
|->  ( F `  (
x  +  W ) ) )
2018, 19dmmpti 5668 . . . . . . . . 9  |-  dom  G  =  ( 1 ... W )
2117, 20sseqtri 3439 . . . . . . . 8  |-  ( `' G " { C } )  C_  (
1 ... W )
2216, 21syl6ss 3419 . . . . . . 7  |-  ( ph  ->  ( A (AP `  K ) D ) 
C_  ( 1 ... W ) )
23 ssun2 3573 . . . . . . . . 9  |-  ( ( A  +  D ) (AP `  ( K  -  1 ) ) D )  C_  ( { A }  u.  (
( A  +  D
) (AP `  ( K  -  1 ) ) D ) )
24 vdwlem8.k . . . . . . . . . . 11  |-  ( ph  ->  K  e.  ( ZZ>= ` 
2 ) )
25 uz2m1nn 11184 . . . . . . . . . . 11  |-  ( K  e.  ( ZZ>= `  2
)  ->  ( K  -  1 )  e.  NN )
2624, 25syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( K  -  1 )  e.  NN )
271, 3nnaddcld 10607 . . . . . . . . . 10  |-  ( ph  ->  ( A  +  D
)  e.  NN )
28 vdwapid1 14868 . . . . . . . . . 10  |-  ( ( ( K  -  1 )  e.  NN  /\  ( A  +  D
)  e.  NN  /\  D  e.  NN )  ->  ( A  +  D
)  e.  ( ( A  +  D ) (AP `  ( K  -  1 ) ) D ) )
2926, 27, 3, 28syl3anc 1264 . . . . . . . . 9  |-  ( ph  ->  ( A  +  D
)  e.  ( ( A  +  D ) (AP `  ( K  -  1 ) ) D ) )
3023, 29sseldi 3405 . . . . . . . 8  |-  ( ph  ->  ( A  +  D
)  e.  ( { A }  u.  (
( A  +  D
) (AP `  ( K  -  1 ) ) D ) ) )
31 eluz2nn 11148 . . . . . . . . . . . . . 14  |-  ( K  e.  ( ZZ>= `  2
)  ->  K  e.  NN )
3224, 31syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  K  e.  NN )
3332nncnd 10576 . . . . . . . . . . . 12  |-  ( ph  ->  K  e.  CC )
34 ax-1cn 9548 . . . . . . . . . . . 12  |-  1  e.  CC
35 npcan 9835 . . . . . . . . . . . 12  |-  ( ( K  e.  CC  /\  1  e.  CC )  ->  ( ( K  - 
1 )  +  1 )  =  K )
3633, 34, 35sylancl 666 . . . . . . . . . . 11  |-  ( ph  ->  ( ( K  - 
1 )  +  1 )  =  K )
3736fveq2d 5829 . . . . . . . . . 10  |-  ( ph  ->  (AP `  ( ( K  -  1 )  +  1 ) )  =  (AP `  K
) )
3837oveqd 6266 . . . . . . . . 9  |-  ( ph  ->  ( A (AP `  ( ( K  - 
1 )  +  1 ) ) D )  =  ( A (AP
`  K ) D ) )
3926nnnn0d 10876 . . . . . . . . . 10  |-  ( ph  ->  ( K  -  1 )  e.  NN0 )
40 vdwapun 14867 . . . . . . . . . 10  |-  ( ( ( K  -  1 )  e.  NN0  /\  A  e.  NN  /\  D  e.  NN )  ->  ( A (AP `  ( ( K  -  1 )  +  1 ) ) D )  =  ( { A }  u.  ( ( A  +  D ) (AP `  ( K  -  1
) ) D ) ) )
4139, 1, 3, 40syl3anc 1264 . . . . . . . . 9  |-  ( ph  ->  ( A (AP `  ( ( K  - 
1 )  +  1 ) ) D )  =  ( { A }  u.  ( ( A  +  D )
(AP `  ( K  -  1 ) ) D ) ) )
4238, 41eqtr3d 2464 . . . . . . . 8  |-  ( ph  ->  ( A (AP `  K ) D )  =  ( { A }  u.  ( ( A  +  D )
(AP `  ( K  -  1 ) ) D ) ) )
4330, 42eleqtrrd 2509 . . . . . . 7  |-  ( ph  ->  ( A  +  D
)  e.  ( A (AP `  K ) D ) )
4422, 43sseldd 3408 . . . . . 6  |-  ( ph  ->  ( A  +  D
)  e.  ( 1 ... W ) )
45 elfzuz3 11748 . . . . . 6  |-  ( ( A  +  D )  e.  ( 1 ... W )  ->  W  e.  ( ZZ>= `  ( A  +  D ) ) )
46 uznn0sub 11141 . . . . . 6  |-  ( W  e.  ( ZZ>= `  ( A  +  D )
)  ->  ( W  -  ( A  +  D ) )  e. 
NN0 )
4744, 45, 463syl 18 . . . . 5  |-  ( ph  ->  ( W  -  ( A  +  D )
)  e.  NN0 )
48 nnnn0addcl 10851 . . . . 5  |-  ( ( ( A  +  A
)  e.  NN  /\  ( W  -  ( A  +  D )
)  e.  NN0 )  ->  ( ( A  +  A )  +  ( W  -  ( A  +  D ) ) )  e.  NN )
4915, 47, 48syl2anc 665 . . . 4  |-  ( ph  ->  ( ( A  +  A )  +  ( W  -  ( A  +  D ) ) )  e.  NN )
5014, 49eqeltrrd 2507 . . 3  |-  ( ph  ->  ( A  +  ( W  -  D ) )  e.  NN )
51 1nn 10571 . . . . . . . 8  |-  1  e.  NN
52 f1osng 5813 . . . . . . . 8  |-  ( ( 1  e.  NN  /\  D  e.  NN )  ->  { <. 1 ,  D >. } : { 1 } -1-1-onto-> { D } )
5351, 3, 52sylancr 667 . . . . . . 7  |-  ( ph  ->  { <. 1 ,  D >. } : { 1 } -1-1-onto-> { D } )
54 f1of 5774 . . . . . . 7  |-  ( {
<. 1 ,  D >. } : { 1 } -1-1-onto-> { D }  ->  {
<. 1 ,  D >. } : { 1 } --> { D }
)
5553, 54syl 17 . . . . . 6  |-  ( ph  ->  { <. 1 ,  D >. } : { 1 } --> { D }
)
563snssd 4088 . . . . . 6  |-  ( ph  ->  { D }  C_  NN )
5755, 56fssd 5698 . . . . 5  |-  ( ph  ->  { <. 1 ,  D >. } : { 1 } --> NN )
58 1z 10918 . . . . . . 7  |-  1  e.  ZZ
59 fzsn 11791 . . . . . . 7  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
6058, 59ax-mp 5 . . . . . 6  |-  ( 1 ... 1 )  =  { 1 }
6160feq2i 5682 . . . . 5  |-  ( {
<. 1 ,  D >. } : ( 1 ... 1 ) --> NN  <->  {
<. 1 ,  D >. } : { 1 } --> NN )
6257, 61sylibr 215 . . . 4  |-  ( ph  ->  { <. 1 ,  D >. } : ( 1 ... 1 ) --> NN )
63 nnex 10566 . . . . 5  |-  NN  e.  _V
64 ovex 6277 . . . . 5  |-  ( 1 ... 1 )  e. 
_V
6563, 64elmap 7455 . . . 4  |-  ( {
<. 1 ,  D >. }  e.  ( NN 
^m  ( 1 ... 1 ) )  <->  { <. 1 ,  D >. } : ( 1 ... 1 ) --> NN )
6662, 65sylibr 215 . . 3  |-  ( ph  ->  { <. 1 ,  D >. }  e.  ( NN 
^m  ( 1 ... 1 ) ) )
671, 7nnaddcld 10607 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  +  W
)  e.  NN )
6867adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  W )  e.  NN )
69 elfznn0 11838 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 0 ... ( K  -  1 ) )  ->  m  e.  NN0 )
703nnnn0d 10876 . . . . . . . . . . . . . 14  |-  ( ph  ->  D  e.  NN0 )
71 nn0mulcl 10857 . . . . . . . . . . . . . 14  |-  ( ( m  e.  NN0  /\  D  e.  NN0 )  -> 
( m  x.  D
)  e.  NN0 )
7269, 70, 71syl2anr 480 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  D )  e.  NN0 )
73 nnnn0addcl 10851 . . . . . . . . . . . . 13  |-  ( ( ( A  +  W
)  e.  NN  /\  ( m  x.  D
)  e.  NN0 )  ->  ( ( A  +  W )  +  ( m  x.  D ) )  e.  NN )
7468, 72, 73syl2anc 665 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  +  W
)  +  ( m  x.  D ) )  e.  NN )
75 nnuz 11145 . . . . . . . . . . . 12  |-  NN  =  ( ZZ>= `  1 )
7674, 75syl6eleq 2516 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  +  W
)  +  ( m  x.  D ) )  e.  ( ZZ>= `  1
) )
7716adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A (AP `  K ) D )  C_  ( `' G " { C } ) )
78 eqid 2428 . . . . . . . . . . . . . . . . . 18  |-  ( A  +  ( m  x.  D ) )  =  ( A  +  ( m  x.  D ) )
79 oveq1 6256 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  m  ->  (
n  x.  D )  =  ( m  x.  D ) )
8079oveq2d 6265 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  m  ->  ( A  +  ( n  x.  D ) )  =  ( A  +  ( m  x.  D ) ) )
8180eqeq2d 2438 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  m  ->  (
( A  +  ( m  x.  D ) )  =  ( A  +  ( n  x.  D ) )  <->  ( A  +  ( m  x.  D ) )  =  ( A  +  ( m  x.  D ) ) ) )
8281rspcev 3125 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) )
8378, 82mpan2 675 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  ( 0 ... ( K  -  1 ) )  ->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( A  +  ( m  x.  D
) )  =  ( A  +  ( n  x.  D ) ) )
8432nnnn0d 10876 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  K  e.  NN0 )
85 vdwapval 14866 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) ) ) )
8684, 1, 3, 85syl3anc 1264 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( A  +  ( m  x.  D
) )  e.  ( A (AP `  K
) D )  <->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( A  +  ( m  x.  D
) )  =  ( A  +  ( n  x.  D ) ) ) )
8786biimpar 487 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  E. n  e.  ( 0 ... ( K  -  1 ) ) ( A  +  ( m  x.  D
) )  =  ( A  +  ( n  x.  D ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( A (AP `  K ) D ) )
8883, 87sylan2 476 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( A (AP `  K ) D ) )
8977, 88sseldd 3408 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( `' G " { C } ) )
9018, 19fnmpti 5667 . . . . . . . . . . . . . . . 16  |-  G  Fn  ( 1 ... W
)
91 fniniseg 5962 . . . . . . . . . . . . . . . 16  |-  ( G  Fn  ( 1 ... W )  ->  (
( A  +  ( m  x.  D ) )  e.  ( `' G " { C } )  <->  ( ( A  +  ( m  x.  D ) )  e.  ( 1 ... W
)  /\  ( G `  ( A  +  ( m  x.  D ) ) )  =  C ) ) )
9290, 91ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( ( A  +  ( m  x.  D ) )  e.  ( `' G " { C } )  <-> 
( ( A  +  ( m  x.  D
) )  e.  ( 1 ... W )  /\  ( G `  ( A  +  (
m  x.  D ) ) )  =  C ) )
9389, 92sylib 199 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  +  ( m  x.  D ) )  e.  ( 1 ... W )  /\  ( G `  ( A  +  ( m  x.  D ) ) )  =  C ) )
9493simpld 460 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( 1 ... W
) )
95 elfzuz3 11748 . . . . . . . . . . . . 13  |-  ( ( A  +  ( m  x.  D ) )  e.  ( 1 ... W )  ->  W  e.  ( ZZ>= `  ( A  +  ( m  x.  D ) ) ) )
96 eluzelz 11119 . . . . . . . . . . . . . 14  |-  ( W  e.  ( ZZ>= `  ( A  +  ( m  x.  D ) ) )  ->  W  e.  ZZ )
97 eluzadd 11138 . . . . . . . . . . . . . 14  |-  ( ( W  e.  ( ZZ>= `  ( A  +  (
m  x.  D ) ) )  /\  W  e.  ZZ )  ->  ( W  +  W )  e.  ( ZZ>= `  ( ( A  +  ( m  x.  D ) )  +  W ) ) )
9896, 97mpdan 672 . . . . . . . . . . . . 13  |-  ( W  e.  ( ZZ>= `  ( A  +  ( m  x.  D ) ) )  ->  ( W  +  W )  e.  (
ZZ>= `  ( ( A  +  ( m  x.  D ) )  +  W ) ) )
9994, 95, 983syl 18 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  +  W )  e.  ( ZZ>= `  ( ( A  +  ( m  x.  D ) )  +  W ) ) )
10082timesd 10806 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2  x.  W
)  =  ( W  +  W ) )
101100adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
2  x.  W )  =  ( W  +  W ) )
1022adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  A  e.  CC )
1038adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  W  e.  CC )
10472nn0cnd 10878 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  D )  e.  CC )
105102, 103, 104add32d 9808 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  +  W
)  +  ( m  x.  D ) )  =  ( ( A  +  ( m  x.  D ) )  +  W ) )
106105fveq2d 5829 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( ZZ>=
`  ( ( A  +  W )  +  ( m  x.  D
) ) )  =  ( ZZ>= `  ( ( A  +  ( m  x.  D ) )  +  W ) ) )
10799, 101, 1063eltr4d 2521 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
2  x.  W )  e.  ( ZZ>= `  (
( A  +  W
)  +  ( m  x.  D ) ) ) )
108 elfzuzb 11745 . . . . . . . . . . 11  |-  ( ( ( A  +  W
)  +  ( m  x.  D ) )  e.  ( 1 ... ( 2  x.  W
) )  <->  ( (
( A  +  W
)  +  ( m  x.  D ) )  e.  ( ZZ>= `  1
)  /\  ( 2  x.  W )  e.  ( ZZ>= `  ( ( A  +  W )  +  ( m  x.  D ) ) ) ) )
10976, 107, 108sylanbrc 668 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  +  W
)  +  ( m  x.  D ) )  e.  ( 1 ... ( 2  x.  W
) ) )
110105fveq2d 5829 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( F `  ( ( A  +  W )  +  ( m  x.  D ) ) )  =  ( F `  ( ( A  +  ( m  x.  D
) )  +  W
) ) )
111 oveq1 6256 . . . . . . . . . . . . . 14  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  (
x  +  W )  =  ( ( A  +  ( m  x.  D ) )  +  W ) )
112111fveq2d 5829 . . . . . . . . . . . . 13  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  ( F `  ( x  +  W ) )  =  ( F `  (
( A  +  ( m  x.  D ) )  +  W ) ) )
113 fvex 5835 . . . . . . . . . . . . 13  |-  ( F `
 ( ( A  +  ( m  x.  D ) )  +  W ) )  e. 
_V
114112, 19, 113fvmpt 5908 . . . . . . . . . . . 12  |-  ( ( A  +  ( m  x.  D ) )  e.  ( 1 ... W )  ->  ( G `  ( A  +  ( m  x.  D ) ) )  =  ( F `  ( ( A  +  ( m  x.  D
) )  +  W
) ) )
11594, 114syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( G `  ( A  +  ( m  x.  D ) ) )  =  ( F `  ( ( A  +  ( m  x.  D
) )  +  W
) ) )
11693simprd 464 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( G `  ( A  +  ( m  x.  D ) ) )  =  C )
117110, 115, 1163eqtr2d 2468 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( F `  ( ( A  +  W )  +  ( m  x.  D ) ) )  =  C )
118109, 117jca 534 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( A  +  W )  +  ( m  x.  D ) )  e.  ( 1 ... ( 2  x.  W ) )  /\  ( F `  ( ( A  +  W )  +  ( m  x.  D ) ) )  =  C ) )
119 eleq1 2494 . . . . . . . . . 10  |-  ( x  =  ( ( A  +  W )  +  ( m  x.  D
) )  ->  (
x  e.  ( 1 ... ( 2  x.  W ) )  <->  ( ( A  +  W )  +  ( m  x.  D ) )  e.  ( 1 ... (
2  x.  W ) ) ) )
120 fveq2 5825 . . . . . . . . . . 11  |-  ( x  =  ( ( A  +  W )  +  ( m  x.  D
) )  ->  ( F `  x )  =  ( F `  ( ( A  +  W )  +  ( m  x.  D ) ) ) )
121120eqeq1d 2430 . . . . . . . . . 10  |-  ( x  =  ( ( A  +  W )  +  ( m  x.  D
) )  ->  (
( F `  x
)  =  C  <->  ( F `  ( ( A  +  W )  +  ( m  x.  D ) ) )  =  C ) )
122119, 121anbi12d 715 . . . . . . . . 9  |-  ( x  =  ( ( A  +  W )  +  ( m  x.  D
) )  ->  (
( x  e.  ( 1 ... ( 2  x.  W ) )  /\  ( F `  x )  =  C )  <->  ( ( ( A  +  W )  +  ( m  x.  D ) )  e.  ( 1 ... (
2  x.  W ) )  /\  ( F `
 ( ( A  +  W )  +  ( m  x.  D
) ) )  =  C ) ) )
123118, 122syl5ibrcom 225 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
x  =  ( ( A  +  W )  +  ( m  x.  D ) )  -> 
( x  e.  ( 1 ... ( 2  x.  W ) )  /\  ( F `  x )  =  C ) ) )
124123rexlimdva 2856 . . . . . . 7  |-  ( ph  ->  ( E. m  e.  ( 0 ... ( K  -  1 ) ) x  =  ( ( A  +  W
)  +  ( m  x.  D ) )  ->  ( x  e.  ( 1 ... (
2  x.  W ) )  /\  ( F `
 x )  =  C ) ) )
125 vdwapval 14866 . . . . . . . 8  |-  ( ( K  e.  NN0  /\  ( A  +  W
)  e.  NN  /\  D  e.  NN )  ->  ( x  e.  ( ( A  +  W
) (AP `  K
) D )  <->  E. m  e.  ( 0 ... ( K  -  1 ) ) x  =  ( ( A  +  W
)  +  ( m  x.  D ) ) ) )
12684, 67, 3, 125syl3anc 1264 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( ( A  +  W
) (AP `  K
) D )  <->  E. m  e.  ( 0 ... ( K  -  1 ) ) x  =  ( ( A  +  W
)  +  ( m  x.  D ) ) ) )
127 vdwlem8.f . . . . . . . 8  |-  ( ph  ->  F : ( 1 ... ( 2  x.  W ) ) --> R )
128 ffn 5689 . . . . . . . 8  |-  ( F : ( 1 ... ( 2  x.  W
) ) --> R  ->  F  Fn  ( 1 ... ( 2  x.  W ) ) )
129 fniniseg 5962 . . . . . . . 8  |-  ( F  Fn  ( 1 ... ( 2  x.  W
) )  ->  (
x  e.  ( `' F " { C } )  <->  ( x  e.  ( 1 ... (
2  x.  W ) )  /\  ( F `
 x )  =  C ) ) )
130127, 128, 1293syl 18 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( `' F " { C } )  <->  ( x  e.  ( 1 ... (
2  x.  W ) )  /\  ( F `
 x )  =  C ) ) )
131124, 126, 1303imtr4d 271 . . . . . 6  |-  ( ph  ->  ( x  e.  ( ( A  +  W
) (AP `  K
) D )  ->  x  e.  ( `' F " { C }
) ) )
132131ssrdv 3413 . . . . 5  |-  ( ph  ->  ( ( A  +  W ) (AP `  K ) D ) 
C_  ( `' F " { C } ) )
133 fvsng 6057 . . . . . . . . 9  |-  ( ( 1  e.  NN  /\  D  e.  NN )  ->  ( { <. 1 ,  D >. } `  1
)  =  D )
13451, 3, 133sylancr 667 . . . . . . . 8  |-  ( ph  ->  ( { <. 1 ,  D >. } `  1
)  =  D )
135134oveq2d 6265 . . . . . . 7  |-  ( ph  ->  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) )  =  ( ( A  +  ( W  -  D ) )  +  D ) )
1362, 12, 4addassd 9616 . . . . . . 7  |-  ( ph  ->  ( ( A  +  ( W  -  D
) )  +  D
)  =  ( A  +  ( ( W  -  D )  +  D ) ) )
1378, 4npcand 9941 . . . . . . . 8  |-  ( ph  ->  ( ( W  -  D )  +  D
)  =  W )
138137oveq2d 6265 . . . . . . 7  |-  ( ph  ->  ( A  +  ( ( W  -  D
)  +  D ) )  =  ( A  +  W ) )
139135, 136, 1383eqtrd 2466 . . . . . 6  |-  ( ph  ->  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) )  =  ( A  +  W ) )
140139, 134oveq12d 6267 . . . . 5  |-  ( ph  ->  ( ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `  1
) ) (AP `  K ) ( {
<. 1 ,  D >. } `  1 ) )  =  ( ( A  +  W ) (AP `  K ) D ) )
141139fveq2d 5829 . . . . . . . 8  |-  ( ph  ->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) )  =  ( F `  ( A  +  W ) ) )
142 vdwapid1 14868 . . . . . . . . . . . . 13  |-  ( ( K  e.  NN  /\  A  e.  NN  /\  D  e.  NN )  ->  A  e.  ( A (AP `  K ) D ) )
14332, 1, 3, 142syl3anc 1264 . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  ( A (AP `  K ) D ) )
14416, 143sseldd 3408 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  ( `' G " { C } ) )
145 fniniseg 5962 . . . . . . . . . . . 12  |-  ( G  Fn  ( 1 ... W )  ->  ( A  e.  ( `' G " { C }
)  <->  ( A  e.  ( 1 ... W
)  /\  ( G `  A )  =  C ) ) )
14690, 145ax-mp 5 . . . . . . . . . . 11  |-  ( A  e.  ( `' G " { C } )  <-> 
( A  e.  ( 1 ... W )  /\  ( G `  A )  =  C ) )
147144, 146sylib 199 . . . . . . . . . 10  |-  ( ph  ->  ( A  e.  ( 1 ... W )  /\  ( G `  A )  =  C ) )
148147simpld 460 . . . . . . . . 9  |-  ( ph  ->  A  e.  ( 1 ... W ) )
149 oveq1 6256 . . . . . . . . . . 11  |-  ( x  =  A  ->  (
x  +  W )  =  ( A  +  W ) )
150149fveq2d 5829 . . . . . . . . . 10  |-  ( x  =  A  ->  ( F `  ( x  +  W ) )  =  ( F `  ( A  +  W )
) )
151 fvex 5835 . . . . . . . . . 10  |-  ( F `
 ( A  +  W ) )  e. 
_V
152150, 19, 151fvmpt 5908 . . . . . . . . 9  |-  ( A  e.  ( 1 ... W )  ->  ( G `  A )  =  ( F `  ( A  +  W
) ) )
153148, 152syl 17 . . . . . . . 8  |-  ( ph  ->  ( G `  A
)  =  ( F `
 ( A  +  W ) ) )
154147simprd 464 . . . . . . . 8  |-  ( ph  ->  ( G `  A
)  =  C )
155141, 153, 1543eqtr2d 2468 . . . . . . 7  |-  ( ph  ->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) )  =  C )
156155sneqd 3953 . . . . . 6  |-  ( ph  ->  { ( F `  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) ) ) }  =  { C } )
157156imaeq2d 5130 . . . . 5  |-  ( ph  ->  ( `' F " { ( F `  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) ) ) } )  =  ( `' F " { C } ) )
158132, 140, 1573sstr4d 3450 . . . 4  |-  ( ph  ->  ( ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `  1
) ) (AP `  K ) ( {
<. 1 ,  D >. } `  1 ) )  C_  ( `' F " { ( F `
 ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `  1
) ) ) } ) )
159158ralrimivw 2780 . . 3  |-  ( ph  ->  A. i  e.  ( 1 ... 1 ) ( ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `  1
) ) (AP `  K ) ( {
<. 1 ,  D >. } `  1 ) )  C_  ( `' F " { ( F `
 ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `  1
) ) ) } ) )
160155mpteq2dv 4454 . . . . . . . 8  |-  ( ph  ->  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) ) )  =  ( i  e.  ( 1 ... 1 ) 
|->  C ) )
161 fconstmpt 4840 . . . . . . . 8  |-  ( ( 1 ... 1 )  X.  { C }
)  =  ( i  e.  ( 1 ... 1 )  |->  C )
162160, 161syl6eqr 2480 . . . . . . 7  |-  ( ph  ->  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) ) )  =  ( ( 1 ... 1 )  X.  { C } ) )
163162rneqd 5024 . . . . . 6  |-  ( ph  ->  ran  ( i  e.  ( 1 ... 1
)  |->  ( F `  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) ) ) )  =  ran  ( ( 1 ... 1 )  X. 
{ C } ) )
164 elfz3 11760 . . . . . . . 8  |-  ( 1  e.  ZZ  ->  1  e.  ( 1 ... 1
) )
165 ne0i 3710 . . . . . . . 8  |-  ( 1  e.  ( 1 ... 1 )  ->  (
1 ... 1 )  =/=  (/) )
16658, 164, 165mp2b 10 . . . . . . 7  |-  ( 1 ... 1 )  =/=  (/)
167 rnxp 5229 . . . . . . 7  |-  ( ( 1 ... 1 )  =/=  (/)  ->  ran  ( ( 1 ... 1 )  X.  { C }
)  =  { C } )
168166, 167ax-mp 5 . . . . . 6  |-  ran  (
( 1 ... 1
)  X.  { C } )  =  { C }
169163, 168syl6eq 2478 . . . . 5  |-  ( ph  ->  ran  ( i  e.  ( 1 ... 1
)  |->  ( F `  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) ) ) )  =  { C } )
170169fveq2d 5829 . . . 4  |-  ( ph  ->  ( # `  ran  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) ) ) )  =  ( # `  { C } ) )
171 vdwlem8.c . . . . 5  |-  C  e. 
_V
172 hashsng 12499 . . . . 5  |-  ( C  e.  _V  ->  ( # `
 { C }
)  =  1 )
173171, 172ax-mp 5 . . . 4  |-  ( # `  { C } )  =  1
174170, 173syl6eq 2478 . . 3  |-  ( ph  ->  ( # `  ran  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) ) ) )  =  1 )
175 oveq1 6256 . . . . . . . 8  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  (
a  +  ( d `
 i ) )  =  ( ( A  +  ( W  -  D ) )  +  ( d `  i
) ) )
176175oveq1d 6264 . . . . . . 7  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  (
( a  +  ( d `  i ) ) (AP `  K
) ( d `  i ) )  =  ( ( ( A  +  ( W  -  D ) )  +  ( d `  i
) ) (AP `  K ) ( d `
 i ) ) )
177175fveq2d 5829 . . . . . . . . 9  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  ( F `  ( a  +  ( d `  i ) ) )  =  ( F `  ( ( A  +  ( W  -  D
) )  +  ( d `  i ) ) ) )
178177sneqd 3953 . . . . . . . 8  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  { ( F `  ( a  +  ( d `  i ) ) ) }  =  { ( F `  ( ( A  +  ( W  -  D ) )  +  ( d `  i ) ) ) } )
179178imaeq2d 5130 . . . . . . 7  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } )  =  ( `' F " { ( F `  ( ( A  +  ( W  -  D ) )  +  ( d `  i ) ) ) } ) )
180176, 179sseq12d 3436 . . . . . 6  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  (
( ( a  +  ( d `  i
) ) (AP `  K ) ( d `
 i ) ) 
C_  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } )  <-> 
( ( ( A  +  ( W  -  D ) )  +  ( d `  i
) ) (AP `  K ) ( d `
 i ) ) 
C_  ( `' F " { ( F `  ( ( A  +  ( W  -  D
) )  +  ( d `  i ) ) ) } ) ) )
181180ralbidv 2804 . . . . 5  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  ( A. i  e.  (
1 ... 1 ) ( ( a  +  ( d `  i ) ) (AP `  K
) ( d `  i ) )  C_  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } )  <->  A. i  e.  ( 1 ... 1
) ( ( ( A  +  ( W  -  D ) )  +  ( d `  i ) ) (AP
`  K ) ( d `  i ) )  C_  ( `' F " { ( F `
 ( ( A  +  ( W  -  D ) )  +  ( d `  i
) ) ) } ) ) )
182177mpteq2dv 4454 . . . . . . . 8  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  (
i  e.  ( 1 ... 1 )  |->  ( F `  ( a  +  ( d `  i ) ) ) )  =  ( i  e.  ( 1 ... 1 )  |->  ( F `
 ( ( A  +  ( W  -  D ) )  +  ( d `  i
) ) ) ) )
183182rneqd 5024 . . . . . . 7  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  ran  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
a  +  ( d `
 i ) ) ) )  =  ran  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
( A  +  ( W  -  D ) )  +  ( d `
 i ) ) ) ) )
184183fveq2d 5829 . . . . . 6  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  ( # `
 ran  ( i  e.  ( 1 ... 1
)  |->  ( F `  ( a  +  ( d `  i ) ) ) ) )  =  ( # `  ran  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
( A  +  ( W  -  D ) )  +  ( d `
 i ) ) ) ) ) )
185184eqeq1d 2430 . . . . 5  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  (
( # `  ran  (
i  e.  ( 1 ... 1 )  |->  ( F `  ( a  +  ( d `  i ) ) ) ) )  =  1  <-> 
( # `  ran  (
i  e.  ( 1 ... 1 )  |->  ( F `  ( ( A  +  ( W  -  D ) )  +  ( d `  i ) ) ) ) )  =  1 ) )
186181, 185anbi12d 715 . . . 4  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  (
( A. i  e.  ( 1 ... 1
) ( ( a  +  ( d `  i ) ) (AP
`  K ) ( d `  i ) )  C_  ( `' F " { ( F `
 ( a  +  ( d `  i
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... 1
)  |->  ( F `  ( a  +  ( d `  i ) ) ) ) )  =  1 )  <->  ( A. i  e.  ( 1 ... 1 ) ( ( ( A  +  ( W  -  D
) )  +  ( d `  i ) ) (AP `  K
) ( d `  i ) )  C_  ( `' F " { ( F `  ( ( A  +  ( W  -  D ) )  +  ( d `  i ) ) ) } )  /\  ( # `
 ran  ( i  e.  ( 1 ... 1
)  |->  ( F `  ( ( A  +  ( W  -  D
) )  +  ( d `  i ) ) ) ) )  =  1 ) ) )
187 fveq1 5824 . . . . . . . . . 10  |-  ( d  =  { <. 1 ,  D >. }  ->  (
d `  i )  =  ( { <. 1 ,  D >. } `
 i ) )
188 elfz1eq 11761 . . . . . . . . . . 11  |-  ( i  e.  ( 1 ... 1 )  ->  i  =  1 )
189188fveq2d 5829 . . . . . . . . . 10  |-  ( i  e.  ( 1 ... 1 )  ->  ( { <. 1 ,  D >. } `  i )  =  ( { <. 1 ,  D >. } `
 1 ) )
190187, 189sylan9eq 2482 . . . . . . . . 9  |-  ( ( d  =  { <. 1 ,  D >. }  /\  i  e.  ( 1 ... 1 ) )  ->  ( d `  i )  =  ( { <. 1 ,  D >. } `  1 ) )
191190oveq2d 6265 . . . . . . . 8  |-  ( ( d  =  { <. 1 ,  D >. }  /\  i  e.  ( 1 ... 1 ) )  ->  ( ( A  +  ( W  -  D ) )  +  ( d `  i
) )  =  ( ( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) )
192191, 190oveq12d 6267 . . . . . . 7  |-  ( ( d  =  { <. 1 ,  D >. }  /\  i  e.  ( 1 ... 1 ) )  ->  ( (
( A  +  ( W  -  D ) )  +  ( d `
 i ) ) (AP `  K ) ( d `  i
) )  =  ( ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) ) (AP `  K
) ( { <. 1 ,  D >. } `
 1 ) ) )
193191fveq2d 5829 . . . . . . . . 9  |-  ( ( d  =  { <. 1 ,  D >. }  /\  i  e.  ( 1 ... 1 ) )  ->  ( F `  ( ( A  +  ( W  -  D
) )  +  ( d `  i ) ) )  =  ( F `  ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `
 1 ) ) ) )
194193sneqd 3953 . . . . . . . 8  |-  ( ( d  =  { <. 1 ,  D >. }  /\  i  e.  ( 1 ... 1 ) )  ->  { ( F `  ( ( A  +  ( W  -  D ) )  +  ( d `  i
) ) ) }  =  { ( F `
 ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `  1
) ) ) } )
195194imaeq2d 5130 . . . . . . 7  |-  ( ( d  =  { <. 1 ,  D >. }  /\  i  e.  ( 1 ... 1 ) )  ->  ( `' F " { ( F `
 ( ( A  +  ( W  -  D ) )  +  ( d `  i
) ) ) } )  =  ( `' F " { ( F `  ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `
 1 ) ) ) } ) )
196192, 195sseq12d 3436 . . . . . 6  |-  ( ( d  =  { <. 1 ,  D >. }  /\  i  e.  ( 1 ... 1 ) )  ->  ( (
( ( A  +  ( W  -  D
) )  +  ( d `  i ) ) (AP `  K
) ( d `  i ) )  C_  ( `' F " { ( F `  ( ( A  +  ( W  -  D ) )  +  ( d `  i ) ) ) } )  <->  ( (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) (AP `  K
) ( { <. 1 ,  D >. } `
 1 ) ) 
C_  ( `' F " { ( F `  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) ) ) } ) ) )
197196ralbidva 2801 . . . . 5  |-  ( d  =  { <. 1 ,  D >. }  ->  ( A. i  e.  (
1 ... 1 ) ( ( ( A  +  ( W  -  D
) )  +  ( d `  i ) ) (AP `  K
) ( d `  i ) )  C_  ( `' F " { ( F `  ( ( A  +  ( W  -  D ) )  +  ( d `  i ) ) ) } )  <->  A. i  e.  ( 1 ... 1
) ( ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `
 1 ) ) (AP `  K ) ( { <. 1 ,  D >. } `  1
) )  C_  ( `' F " { ( F `  ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `
 1 ) ) ) } ) ) )
198193mpteq2dva 4453 . . . . . . . 8  |-  ( d  =  { <. 1 ,  D >. }  ->  (
i  e.  ( 1 ... 1 )  |->  ( F `  ( ( A  +  ( W  -  D ) )  +  ( d `  i ) ) ) )  =  ( i  e.  ( 1 ... 1 )  |->  ( F `
 ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `  1
) ) ) ) )
199198rneqd 5024 . . . . . . 7  |-  ( d  =  { <. 1 ,  D >. }  ->  ran  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
( A  +  ( W  -  D ) )  +  ( d `
 i ) ) ) )  =  ran  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) ) ) )
200199fveq2d 5829 . . . . . 6  |-  ( d  =  { <. 1 ,  D >. }  ->  ( # `
 ran  ( i  e.  ( 1 ... 1
)  |->  ( F `  ( ( A  +  ( W  -  D
) )  +  ( d `  i ) ) ) ) )  =  ( # `  ran  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) ) ) ) )
201200eqeq1d 2430 . . . . 5  |-  ( d  =  { <. 1 ,  D >. }  ->  (
( # `  ran  (
i  e.  ( 1 ... 1 )  |->  ( F `  ( ( A  +  ( W  -  D ) )  +  ( d `  i ) ) ) ) )  =  1  <-> 
( # `  ran  (
i  e.  ( 1 ... 1 )  |->  ( F `  ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `
 1 ) ) ) ) )  =  1 ) )
202197, 201anbi12d 715 . . . 4  |-  ( d  =  { <. 1 ,  D >. }  ->  (
( A. i  e.  ( 1 ... 1
) ( ( ( A  +  ( W  -  D ) )  +  ( d `  i ) ) (AP
`  K ) ( d `  i ) )  C_  ( `' F " { ( F `
 ( ( A  +  ( W  -  D ) )  +  ( d `  i
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... 1
)  |->  ( F `  ( ( A  +  ( W  -  D
) )  +  ( d `  i ) ) ) ) )  =  1 )  <->  ( A. i  e.  ( 1 ... 1 ) ( ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) ) (AP `  K
) ( { <. 1 ,  D >. } `
 1 ) ) 
C_  ( `' F " { ( F `  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) ) ) )  =  1 ) ) )
203186, 202rspc2ev 3136 . . 3  |-  ( ( ( A  +  ( W  -  D ) )  e.  NN  /\  {
<. 1 ,  D >. }  e.  ( NN 
^m  ( 1 ... 1 ) )  /\  ( A. i  e.  ( 1 ... 1 ) ( ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `  1
) ) (AP `  K ) ( {
<. 1 ,  D >. } `  1 ) )  C_  ( `' F " { ( F `
 ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `  1
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... 1
)  |->  ( F `  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) ) ) ) )  =  1 ) )  ->  E. a  e.  NN  E. d  e.  ( NN 
^m  ( 1 ... 1 ) ) ( A. i  e.  ( 1 ... 1 ) ( ( a  +  ( d `  i
) ) (AP `  K ) ( d `
 i ) ) 
C_  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
a  +  ( d `
 i ) ) ) ) )  =  1 ) )
20450, 66, 159, 174, 203syl112anc 1268 . 2  |-  ( ph  ->  E. a  e.  NN  E. d  e.  ( NN 
^m  ( 1 ... 1 ) ) ( A. i  e.  ( 1 ... 1 ) ( ( a  +  ( d `  i
) ) (AP `  K ) ( d `
 i ) ) 
C_  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
a  +  ( d `
 i ) ) ) ) )  =  1 ) )
205 ovex 6277 . . 3  |-  ( 1 ... ( 2  x.  W ) )  e. 
_V
20651a1i 11 . . 3  |-  ( ph  ->  1  e.  NN )
207 eqid 2428 . . 3  |-  ( 1 ... 1 )  =  ( 1 ... 1
)
208205, 84, 127, 206, 207vdwpc 14873 . 2  |-  ( ph  ->  ( <. 1 ,  K >. PolyAP 
F  <->  E. a  e.  NN  E. d  e.  ( NN 
^m  ( 1 ... 1 ) ) ( A. i  e.  ( 1 ... 1 ) ( ( a  +  ( d `  i
) ) (AP `  K ) ( d `
 i ) ) 
C_  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
a  +  ( d `
 i ) ) ) ) )  =  1 ) ) )
209204, 208mpbird 235 1  |-  ( ph  -> 
<. 1 ,  K >. PolyAP 
F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1872    =/= wne 2599   A.wral 2714   E.wrex 2715   _Vcvv 3022    u. cun 3377    C_ wss 3379   (/)c0 3704   {csn 3941   <.cop 3947   class class class wbr 4366    |-> cmpt 4425    X. cxp 4794   `'ccnv 4795   dom cdm 4796   ran crn 4797   "cima 4799    Fn wfn 5539   -->wf 5540   -1-1-onto->wf1o 5543   ` cfv 5544  (class class class)co 6249    ^m cmap 7427   Fincfn 7524   CCcc 9488   0cc0 9490   1c1 9491    + caddc 9493    x. cmul 9495    - cmin 9811   NNcn 10560   2c2 10610   NN0cn0 10820   ZZcz 10888   ZZ>=cuz 11110   ...cfz 11735   #chash 12465  APcvdwa 14858   PolyAP cvdwp 14860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-reu 2721  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-int 4199  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-riota 6211  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-1st 6751  df-2nd 6752  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-1o 7137  df-er 7318  df-map 7429  df-en 7525  df-dom 7526  df-sdom 7527  df-fin 7528  df-card 8325  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9813  df-neg 9814  df-nn 10561  df-2 10619  df-n0 10821  df-z 10889  df-uz 11111  df-fz 11736  df-hash 12466  df-vdwap 14861  df-vdwpc 14863
This theorem is referenced by:  vdwlem10  14883
  Copyright terms: Public domain W3C validator