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

Theorem vdwlem8 14590
Description: Lemma for vdw 14596. (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 10547 . . . . . . . . 9  |-  ( ph  ->  A  e.  CC )
3 vdwlem8.d . . . . . . . . . 10  |-  ( ph  ->  D  e.  NN )
43nncnd 10547 . . . . . . . . 9  |-  ( ph  ->  D  e.  CC )
52, 4addcomd 9771 . . . . . . . 8  |-  ( ph  ->  ( A  +  D
)  =  ( D  +  A ) )
65oveq2d 6286 . . . . . . 7  |-  ( ph  ->  ( W  -  ( A  +  D )
)  =  ( W  -  ( D  +  A ) ) )
7 vdwlem8.w . . . . . . . . 9  |-  ( ph  ->  W  e.  NN )
87nncnd 10547 . . . . . . . 8  |-  ( ph  ->  W  e.  CC )
98, 4, 2subsub4d 9953 . . . . . . 7  |-  ( ph  ->  ( ( W  -  D )  -  A
)  =  ( W  -  ( D  +  A ) ) )
106, 9eqtr4d 2498 . . . . . 6  |-  ( ph  ->  ( W  -  ( A  +  D )
)  =  ( ( W  -  D )  -  A ) )
1110oveq2d 6286 . . . . 5  |-  ( ph  ->  ( ( A  +  A )  +  ( W  -  ( A  +  D ) ) )  =  ( ( A  +  A )  +  ( ( W  -  D )  -  A ) ) )
128, 4subcld 9922 . . . . . 6  |-  ( ph  ->  ( W  -  D
)  e.  CC )
132, 2, 12ppncand 9962 . . . . 5  |-  ( ph  ->  ( ( A  +  A )  +  ( ( W  -  D
)  -  A ) )  =  ( A  +  ( W  -  D ) ) )
1411, 13eqtrd 2495 . . . 4  |-  ( ph  ->  ( ( A  +  A )  +  ( W  -  ( A  +  D ) ) )  =  ( A  +  ( W  -  D ) ) )
151, 1nnaddcld 10578 . . . . 5  |-  ( ph  ->  ( A  +  A
)  e.  NN )
16 vdwlem8.s . . . . . . . 8  |-  ( ph  ->  ( A (AP `  K ) D ) 
C_  ( `' G " { C } ) )
17 cnvimass 5345 . . . . . . . . 9  |-  ( `' G " { C } )  C_  dom  G
18 fvex 5858 . . . . . . . . . 10  |-  ( F `
 ( x  +  W ) )  e. 
_V
19 vdwlem8.g . . . . . . . . . 10  |-  G  =  ( x  e.  ( 1 ... W ) 
|->  ( F `  (
x  +  W ) ) )
2018, 19dmmpti 5692 . . . . . . . . 9  |-  dom  G  =  ( 1 ... W )
2117, 20sseqtri 3521 . . . . . . . 8  |-  ( `' G " { C } )  C_  (
1 ... W )
2216, 21syl6ss 3501 . . . . . . 7  |-  ( ph  ->  ( A (AP `  K ) D ) 
C_  ( 1 ... W ) )
23 ssun2 3654 . . . . . . . . 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 11157 . . . . . . . . . . 11  |-  ( K  e.  ( ZZ>= `  2
)  ->  ( K  -  1 )  e.  NN )
2624, 25syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( K  -  1 )  e.  NN )
271, 3nnaddcld 10578 . . . . . . . . . 10  |-  ( ph  ->  ( A  +  D
)  e.  NN )
28 vdwapid1 14577 . . . . . . . . . 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 1226 . . . . . . . . 9  |-  ( ph  ->  ( A  +  D
)  e.  ( ( A  +  D ) (AP `  ( K  -  1 ) ) D ) )
3023, 29sseldi 3487 . . . . . . . 8  |-  ( ph  ->  ( A  +  D
)  e.  ( { A }  u.  (
( A  +  D
) (AP `  ( K  -  1 ) ) D ) ) )
31 eluz2nn 11120 . . . . . . . . . . . . . 14  |-  ( K  e.  ( ZZ>= `  2
)  ->  K  e.  NN )
3224, 31syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  K  e.  NN )
3332nncnd 10547 . . . . . . . . . . . 12  |-  ( ph  ->  K  e.  CC )
34 ax-1cn 9539 . . . . . . . . . . . 12  |-  1  e.  CC
35 npcan 9820 . . . . . . . . . . . 12  |-  ( ( K  e.  CC  /\  1  e.  CC )  ->  ( ( K  - 
1 )  +  1 )  =  K )
3633, 34, 35sylancl 660 . . . . . . . . . . 11  |-  ( ph  ->  ( ( K  - 
1 )  +  1 )  =  K )
3736fveq2d 5852 . . . . . . . . . 10  |-  ( ph  ->  (AP `  ( ( K  -  1 )  +  1 ) )  =  (AP `  K
) )
3837oveqd 6287 . . . . . . . . 9  |-  ( ph  ->  ( A (AP `  ( ( K  - 
1 )  +  1 ) ) D )  =  ( A (AP
`  K ) D ) )
3926nnnn0d 10848 . . . . . . . . . 10  |-  ( ph  ->  ( K  -  1 )  e.  NN0 )
40 vdwapun 14576 . . . . . . . . . 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 1226 . . . . . . . . 9  |-  ( ph  ->  ( A (AP `  ( ( K  - 
1 )  +  1 ) ) D )  =  ( { A }  u.  ( ( A  +  D )
(AP `  ( K  -  1 ) ) D ) ) )
4238, 41eqtr3d 2497 . . . . . . . 8  |-  ( ph  ->  ( A (AP `  K ) D )  =  ( { A }  u.  ( ( A  +  D )
(AP `  ( K  -  1 ) ) D ) ) )
4330, 42eleqtrrd 2545 . . . . . . 7  |-  ( ph  ->  ( A  +  D
)  e.  ( A (AP `  K ) D ) )
4422, 43sseldd 3490 . . . . . 6  |-  ( ph  ->  ( A  +  D
)  e.  ( 1 ... W ) )
45 elfzuz3 11688 . . . . . 6  |-  ( ( A  +  D )  e.  ( 1 ... W )  ->  W  e.  ( ZZ>= `  ( A  +  D ) ) )
46 uznn0sub 11113 . . . . . 6  |-  ( W  e.  ( ZZ>= `  ( A  +  D )
)  ->  ( W  -  ( A  +  D ) )  e. 
NN0 )
4744, 45, 463syl 20 . . . . 5  |-  ( ph  ->  ( W  -  ( A  +  D )
)  e.  NN0 )
48 nnnn0addcl 10822 . . . . 5  |-  ( ( ( A  +  A
)  e.  NN  /\  ( W  -  ( A  +  D )
)  e.  NN0 )  ->  ( ( A  +  A )  +  ( W  -  ( A  +  D ) ) )  e.  NN )
4915, 47, 48syl2anc 659 . . . 4  |-  ( ph  ->  ( ( A  +  A )  +  ( W  -  ( A  +  D ) ) )  e.  NN )
5014, 49eqeltrrd 2543 . . 3  |-  ( ph  ->  ( A  +  ( W  -  D ) )  e.  NN )
51 1nn 10542 . . . . . . . 8  |-  1  e.  NN
52 f1osng 5836 . . . . . . . 8  |-  ( ( 1  e.  NN  /\  D  e.  NN )  ->  { <. 1 ,  D >. } : { 1 } -1-1-onto-> { D } )
5351, 3, 52sylancr 661 . . . . . . 7  |-  ( ph  ->  { <. 1 ,  D >. } : { 1 } -1-1-onto-> { D } )
54 f1of 5798 . . . . . . 7  |-  ( {
<. 1 ,  D >. } : { 1 } -1-1-onto-> { D }  ->  {
<. 1 ,  D >. } : { 1 } --> { D }
)
5553, 54syl 16 . . . . . 6  |-  ( ph  ->  { <. 1 ,  D >. } : { 1 } --> { D }
)
563snssd 4161 . . . . . 6  |-  ( ph  ->  { D }  C_  NN )
5755, 56fssd 5722 . . . . 5  |-  ( ph  ->  { <. 1 ,  D >. } : { 1 } --> NN )
58 1z 10890 . . . . . . 7  |-  1  e.  ZZ
59 fzsn 11729 . . . . . . 7  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
6058, 59ax-mp 5 . . . . . 6  |-  ( 1 ... 1 )  =  { 1 }
6160feq2i 5706 . . . . 5  |-  ( {
<. 1 ,  D >. } : ( 1 ... 1 ) --> NN  <->  {
<. 1 ,  D >. } : { 1 } --> NN )
6257, 61sylibr 212 . . . 4  |-  ( ph  ->  { <. 1 ,  D >. } : ( 1 ... 1 ) --> NN )
63 nnex 10537 . . . . 5  |-  NN  e.  _V
64 ovex 6298 . . . . 5  |-  ( 1 ... 1 )  e. 
_V
6563, 64elmap 7440 . . . 4  |-  ( {
<. 1 ,  D >. }  e.  ( NN 
^m  ( 1 ... 1 ) )  <->  { <. 1 ,  D >. } : ( 1 ... 1 ) --> NN )
6662, 65sylibr 212 . . 3  |-  ( ph  ->  { <. 1 ,  D >. }  e.  ( NN 
^m  ( 1 ... 1 ) ) )
671, 7nnaddcld 10578 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  +  W
)  e.  NN )
6867adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  W )  e.  NN )
69 elfznn0 11775 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 0 ... ( K  -  1 ) )  ->  m  e.  NN0 )
703nnnn0d 10848 . . . . . . . . . . . . . 14  |-  ( ph  ->  D  e.  NN0 )
71 nn0mulcl 10828 . . . . . . . . . . . . . 14  |-  ( ( m  e.  NN0  /\  D  e.  NN0 )  -> 
( m  x.  D
)  e.  NN0 )
7269, 70, 71syl2anr 476 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  D )  e.  NN0 )
73 nnnn0addcl 10822 . . . . . . . . . . . . 13  |-  ( ( ( A  +  W
)  e.  NN  /\  ( m  x.  D
)  e.  NN0 )  ->  ( ( A  +  W )  +  ( m  x.  D ) )  e.  NN )
7468, 72, 73syl2anc 659 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  +  W
)  +  ( m  x.  D ) )  e.  NN )
75 nnuz 11117 . . . . . . . . . . . 12  |-  NN  =  ( ZZ>= `  1 )
7674, 75syl6eleq 2552 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  +  W
)  +  ( m  x.  D ) )  e.  ( ZZ>= `  1
) )
7716adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A (AP `  K ) D )  C_  ( `' G " { C } ) )
78 eqid 2454 . . . . . . . . . . . . . . . . . 18  |-  ( A  +  ( m  x.  D ) )  =  ( A  +  ( m  x.  D ) )
79 oveq1 6277 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  m  ->  (
n  x.  D )  =  ( m  x.  D ) )
8079oveq2d 6286 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  m  ->  ( A  +  ( n  x.  D ) )  =  ( A  +  ( m  x.  D ) ) )
8180eqeq2d 2468 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  m  ->  (
( A  +  ( m  x.  D ) )  =  ( A  +  ( n  x.  D ) )  <->  ( A  +  ( m  x.  D ) )  =  ( A  +  ( m  x.  D ) ) ) )
8281rspcev 3207 . . . . . . . . . . . . . . . . . 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 669 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  ( 0 ... ( K  -  1 ) )  ->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( A  +  ( m  x.  D
) )  =  ( A  +  ( n  x.  D ) ) )
8432nnnn0d 10848 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  K  e.  NN0 )
85 vdwapval 14575 . . . . . . . . . . . . . . . . . . 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 1226 . . . . . . . . . . . . . . . . . 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 483 . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( A (AP `  K ) D ) )
8977, 88sseldd 3490 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( `' G " { C } ) )
9018, 19fnmpti 5691 . . . . . . . . . . . . . . . 16  |-  G  Fn  ( 1 ... W
)
91 fniniseg 5984 . . . . . . . . . . . . . . . 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 196 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  +  ( m  x.  D ) )  e.  ( 1 ... W )  /\  ( G `  ( A  +  ( m  x.  D ) ) )  =  C ) )
9493simpld 457 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( A  +  ( m  x.  D ) )  e.  ( 1 ... W
) )
95 elfzuz3 11688 . . . . . . . . . . . . 13  |-  ( ( A  +  ( m  x.  D ) )  e.  ( 1 ... W )  ->  W  e.  ( ZZ>= `  ( A  +  ( m  x.  D ) ) ) )
96 eluzelz 11091 . . . . . . . . . . . . . 14  |-  ( W  e.  ( ZZ>= `  ( A  +  ( m  x.  D ) ) )  ->  W  e.  ZZ )
97 eluzadd 11110 . . . . . . . . . . . . . 14  |-  ( ( W  e.  ( ZZ>= `  ( A  +  (
m  x.  D ) ) )  /\  W  e.  ZZ )  ->  ( W  +  W )  e.  ( ZZ>= `  ( ( A  +  ( m  x.  D ) )  +  W ) ) )
9896, 97mpdan 666 . . . . . . . . . . . . 13  |-  ( W  e.  ( ZZ>= `  ( A  +  ( m  x.  D ) ) )  ->  ( W  +  W )  e.  (
ZZ>= `  ( ( A  +  ( m  x.  D ) )  +  W ) ) )
9994, 95, 983syl 20 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( W  +  W )  e.  ( ZZ>= `  ( ( A  +  ( m  x.  D ) )  +  W ) ) )
10082timesd 10777 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2  x.  W
)  =  ( W  +  W ) )
101100adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
2  x.  W )  =  ( W  +  W ) )
1022adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  A  e.  CC )
1038adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  W  e.  CC )
10472nn0cnd 10850 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  D )  e.  CC )
105102, 103, 104add32d 9793 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  +  W
)  +  ( m  x.  D ) )  =  ( ( A  +  ( m  x.  D ) )  +  W ) )
106105fveq2d 5852 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( ZZ>=
`  ( ( A  +  W )  +  ( m  x.  D
) ) )  =  ( ZZ>= `  ( ( A  +  ( m  x.  D ) )  +  W ) ) )
10799, 101, 1063eltr4d 2557 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
2  x.  W )  e.  ( ZZ>= `  (
( A  +  W
)  +  ( m  x.  D ) ) ) )
108 elfzuzb 11685 . . . . . . . . . . 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 662 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( A  +  W
)  +  ( m  x.  D ) )  e.  ( 1 ... ( 2  x.  W
) ) )
110105fveq2d 5852 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( F `  ( ( A  +  W )  +  ( m  x.  D ) ) )  =  ( F `  ( ( A  +  ( m  x.  D
) )  +  W
) ) )
111 oveq1 6277 . . . . . . . . . . . . . 14  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  (
x  +  W )  =  ( ( A  +  ( m  x.  D ) )  +  W ) )
112111fveq2d 5852 . . . . . . . . . . . . 13  |-  ( x  =  ( A  +  ( m  x.  D
) )  ->  ( F `  ( x  +  W ) )  =  ( F `  (
( A  +  ( m  x.  D ) )  +  W ) ) )
113 fvex 5858 . . . . . . . . . . . . 13  |-  ( F `
 ( ( A  +  ( m  x.  D ) )  +  W ) )  e. 
_V
114112, 19, 113fvmpt 5931 . . . . . . . . . . . 12  |-  ( ( A  +  ( m  x.  D ) )  e.  ( 1 ... W )  ->  ( G `  ( A  +  ( m  x.  D ) ) )  =  ( F `  ( ( A  +  ( m  x.  D
) )  +  W
) ) )
11594, 114syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( G `  ( A  +  ( m  x.  D ) ) )  =  ( F `  ( ( A  +  ( m  x.  D
) )  +  W
) ) )
11693simprd 461 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( G `  ( A  +  ( m  x.  D ) ) )  =  C )
117110, 115, 1163eqtr2d 2501 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( F `  ( ( A  +  W )  +  ( m  x.  D ) ) )  =  C )
118109, 117jca 530 . . . . . . . . 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 2526 . . . . . . . . . 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 5848 . . . . . . . . . . 11  |-  ( x  =  ( ( A  +  W )  +  ( m  x.  D
) )  ->  ( F `  x )  =  ( F `  ( ( A  +  W )  +  ( m  x.  D ) ) ) )
121120eqeq1d 2456 . . . . . . . . . 10  |-  ( x  =  ( ( A  +  W )  +  ( m  x.  D
) )  ->  (
( F `  x
)  =  C  <->  ( F `  ( ( A  +  W )  +  ( m  x.  D ) ) )  =  C ) )
122119, 121anbi12d 708 . . . . . . . . 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 222 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
x  =  ( ( A  +  W )  +  ( m  x.  D ) )  -> 
( x  e.  ( 1 ... ( 2  x.  W ) )  /\  ( F `  x )  =  C ) ) )
124123rexlimdva 2946 . . . . . . 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 14575 . . . . . . . 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 1226 . . . . . . 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 5713 . . . . . . . 8  |-  ( F : ( 1 ... ( 2  x.  W
) ) --> R  ->  F  Fn  ( 1 ... ( 2  x.  W ) ) )
129 fniniseg 5984 . . . . . . . 8  |-  ( F  Fn  ( 1 ... ( 2  x.  W
) )  ->  (
x  e.  ( `' F " { C } )  <->  ( x  e.  ( 1 ... (
2  x.  W ) )  /\  ( F `
 x )  =  C ) ) )
130127, 128, 1293syl 20 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( `' F " { C } )  <->  ( x  e.  ( 1 ... (
2  x.  W ) )  /\  ( F `
 x )  =  C ) ) )
131124, 126, 1303imtr4d 268 . . . . . 6  |-  ( ph  ->  ( x  e.  ( ( A  +  W
) (AP `  K
) D )  ->  x  e.  ( `' F " { C }
) ) )
132131ssrdv 3495 . . . . 5  |-  ( ph  ->  ( ( A  +  W ) (AP `  K ) D ) 
C_  ( `' F " { C } ) )
133 fvsng 6081 . . . . . . . . 9  |-  ( ( 1  e.  NN  /\  D  e.  NN )  ->  ( { <. 1 ,  D >. } `  1
)  =  D )
13451, 3, 133sylancr 661 . . . . . . . 8  |-  ( ph  ->  ( { <. 1 ,  D >. } `  1
)  =  D )
135134oveq2d 6286 . . . . . . 7  |-  ( ph  ->  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) )  =  ( ( A  +  ( W  -  D ) )  +  D ) )
1362, 12, 4addassd 9607 . . . . . . 7  |-  ( ph  ->  ( ( A  +  ( W  -  D
) )  +  D
)  =  ( A  +  ( ( W  -  D )  +  D ) ) )
1378, 4npcand 9926 . . . . . . . 8  |-  ( ph  ->  ( ( W  -  D )  +  D
)  =  W )
138137oveq2d 6286 . . . . . . 7  |-  ( ph  ->  ( A  +  ( ( W  -  D
)  +  D ) )  =  ( A  +  W ) )
139135, 136, 1383eqtrd 2499 . . . . . 6  |-  ( ph  ->  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) )  =  ( A  +  W ) )
140139, 134oveq12d 6288 . . . . 5  |-  ( ph  ->  ( ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `  1
) ) (AP `  K ) ( {
<. 1 ,  D >. } `  1 ) )  =  ( ( A  +  W ) (AP `  K ) D ) )
141139fveq2d 5852 . . . . . . . 8  |-  ( ph  ->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) )  =  ( F `  ( A  +  W ) ) )
142 vdwapid1 14577 . . . . . . . . . . . . 13  |-  ( ( K  e.  NN  /\  A  e.  NN  /\  D  e.  NN )  ->  A  e.  ( A (AP `  K ) D ) )
14332, 1, 3, 142syl3anc 1226 . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  ( A (AP `  K ) D ) )
14416, 143sseldd 3490 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  ( `' G " { C } ) )
145 fniniseg 5984 . . . . . . . . . . . 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 196 . . . . . . . . . 10  |-  ( ph  ->  ( A  e.  ( 1 ... W )  /\  ( G `  A )  =  C ) )
148147simpld 457 . . . . . . . . 9  |-  ( ph  ->  A  e.  ( 1 ... W ) )
149 oveq1 6277 . . . . . . . . . . 11  |-  ( x  =  A  ->  (
x  +  W )  =  ( A  +  W ) )
150149fveq2d 5852 . . . . . . . . . 10  |-  ( x  =  A  ->  ( F `  ( x  +  W ) )  =  ( F `  ( A  +  W )
) )
151 fvex 5858 . . . . . . . . . 10  |-  ( F `
 ( A  +  W ) )  e. 
_V
152150, 19, 151fvmpt 5931 . . . . . . . . 9  |-  ( A  e.  ( 1 ... W )  ->  ( G `  A )  =  ( F `  ( A  +  W
) ) )
153148, 152syl 16 . . . . . . . 8  |-  ( ph  ->  ( G `  A
)  =  ( F `
 ( A  +  W ) ) )
154147simprd 461 . . . . . . . 8  |-  ( ph  ->  ( G `  A
)  =  C )
155141, 153, 1543eqtr2d 2501 . . . . . . 7  |-  ( ph  ->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) )  =  C )
156155sneqd 4028 . . . . . 6  |-  ( ph  ->  { ( F `  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) ) ) }  =  { C } )
157156imaeq2d 5325 . . . . 5  |-  ( ph  ->  ( `' F " { ( F `  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) ) ) } )  =  ( `' F " { C } ) )
158132, 140, 1573sstr4d 3532 . . . 4  |-  ( ph  ->  ( ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `  1
) ) (AP `  K ) ( {
<. 1 ,  D >. } `  1 ) )  C_  ( `' F " { ( F `
 ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `  1
) ) ) } ) )
159158ralrimivw 2869 . . 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 4526 . . . . . . . 8  |-  ( ph  ->  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) ) )  =  ( i  e.  ( 1 ... 1 ) 
|->  C ) )
161 fconstmpt 5032 . . . . . . . 8  |-  ( ( 1 ... 1 )  X.  { C }
)  =  ( i  e.  ( 1 ... 1 )  |->  C )
162160, 161syl6eqr 2513 . . . . . . 7  |-  ( ph  ->  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) ) )  =  ( ( 1 ... 1 )  X.  { C } ) )
163162rneqd 5219 . . . . . 6  |-  ( ph  ->  ran  ( i  e.  ( 1 ... 1
)  |->  ( F `  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) ) ) )  =  ran  ( ( 1 ... 1 )  X. 
{ C } ) )
164 elfz3 11699 . . . . . . . 8  |-  ( 1  e.  ZZ  ->  1  e.  ( 1 ... 1
) )
165 ne0i 3789 . . . . . . . 8  |-  ( 1  e.  ( 1 ... 1 )  ->  (
1 ... 1 )  =/=  (/) )
16658, 164, 165mp2b 10 . . . . . . 7  |-  ( 1 ... 1 )  =/=  (/)
167 rnxp 5422 . . . . . . 7  |-  ( ( 1 ... 1 )  =/=  (/)  ->  ran  ( ( 1 ... 1 )  X.  { C }
)  =  { C } )
168166, 167ax-mp 5 . . . . . 6  |-  ran  (
( 1 ... 1
)  X.  { C } )  =  { C }
169163, 168syl6eq 2511 . . . . 5  |-  ( ph  ->  ran  ( i  e.  ( 1 ... 1
)  |->  ( F `  ( ( A  +  ( W  -  D
) )  +  ( { <. 1 ,  D >. } `  1 ) ) ) )  =  { C } )
170169fveq2d 5852 . . . 4  |-  ( ph  ->  ( # `  ran  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) ) ) )  =  ( # `  { C } ) )
171 vdwlem8.c . . . . 5  |-  C  e. 
_V
172 hashsng 12421 . . . . 5  |-  ( C  e.  _V  ->  ( # `
 { C }
)  =  1 )
173171, 172ax-mp 5 . . . 4  |-  ( # `  { C } )  =  1
174170, 173syl6eq 2511 . . 3  |-  ( ph  ->  ( # `  ran  ( i  e.  ( 1 ... 1 ) 
|->  ( F `  (
( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) ) ) )  =  1 )
175 oveq1 6277 . . . . . . . 8  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  (
a  +  ( d `
 i ) )  =  ( ( A  +  ( W  -  D ) )  +  ( d `  i
) ) )
176175oveq1d 6285 . . . . . . 7  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  (
( a  +  ( d `  i ) ) (AP `  K
) ( d `  i ) )  =  ( ( ( A  +  ( W  -  D ) )  +  ( d `  i
) ) (AP `  K ) ( d `
 i ) ) )
177175fveq2d 5852 . . . . . . . . 9  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  ( F `  ( a  +  ( d `  i ) ) )  =  ( F `  ( ( A  +  ( W  -  D
) )  +  ( d `  i ) ) ) )
178177sneqd 4028 . . . . . . . 8  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  { ( F `  ( a  +  ( d `  i ) ) ) }  =  { ( F `  ( ( A  +  ( W  -  D ) )  +  ( d `  i ) ) ) } )
179178imaeq2d 5325 . . . . . . 7  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } )  =  ( `' F " { ( F `  ( ( A  +  ( W  -  D ) )  +  ( d `  i ) ) ) } ) )
180176, 179sseq12d 3518 . . . . . 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 2893 . . . . 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 4526 . . . . . . . 8  |-  ( a  =  ( A  +  ( W  -  D
) )  ->  (
i  e.  ( 1 ... 1 )  |->  ( F `  ( a  +  ( d `  i ) ) ) )  =  ( i  e.  ( 1 ... 1 )  |->  ( F `
 ( ( A  +  ( W  -  D ) )  +  ( d `  i
) ) ) ) )
183182rneqd 5219 . . . . . . 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 5852 . . . . . 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 2456 . . . . 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 708 . . . 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 5847 . . . . . . . . . 10  |-  ( d  =  { <. 1 ,  D >. }  ->  (
d `  i )  =  ( { <. 1 ,  D >. } `
 i ) )
188 elfz1eq 11700 . . . . . . . . . . 11  |-  ( i  e.  ( 1 ... 1 )  ->  i  =  1 )
189188fveq2d 5852 . . . . . . . . . 10  |-  ( i  e.  ( 1 ... 1 )  ->  ( { <. 1 ,  D >. } `  i )  =  ( { <. 1 ,  D >. } `
 1 ) )
190187, 189sylan9eq 2515 . . . . . . . . 9  |-  ( ( d  =  { <. 1 ,  D >. }  /\  i  e.  ( 1 ... 1 ) )  ->  ( d `  i )  =  ( { <. 1 ,  D >. } `  1 ) )
191190oveq2d 6286 . . . . . . . 8  |-  ( ( d  =  { <. 1 ,  D >. }  /\  i  e.  ( 1 ... 1 ) )  ->  ( ( A  +  ( W  -  D ) )  +  ( d `  i
) )  =  ( ( A  +  ( W  -  D ) )  +  ( {
<. 1 ,  D >. } `  1 ) ) )
192191, 190oveq12d 6288 . . . . . . 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 5852 . . . . . . . . 9  |-  ( ( d  =  { <. 1 ,  D >. }  /\  i  e.  ( 1 ... 1 ) )  ->  ( F `  ( ( A  +  ( W  -  D
) )  +  ( d `  i ) ) )  =  ( F `  ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `
 1 ) ) ) )
194193sneqd 4028 . . . . . . . 8  |-  ( ( d  =  { <. 1 ,  D >. }  /\  i  e.  ( 1 ... 1 ) )  ->  { ( F `  ( ( A  +  ( W  -  D ) )  +  ( d `  i
) ) ) }  =  { ( F `
 ( ( A  +  ( W  -  D ) )  +  ( { <. 1 ,  D >. } `  1
) ) ) } )
195194imaeq2d 5325 . . . . . . 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 3518 . . . . . 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 2890 . . . . 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 4525 . . . . . . . 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 5219 . . . . . . 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 5852 . . . . . 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 2456 . . . . 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 708 . . . 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 3218 . . 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 1230 . 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 6298 . . 3  |-  ( 1 ... ( 2  x.  W ) )  e. 
_V
20651a1i 11 . . 3  |-  ( ph  ->  1  e.  NN )
207 eqid 2454 . . 3  |-  ( 1 ... 1 )  =  ( 1 ... 1
)
208205, 84, 127, 206, 207vdwpc 14582 . 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 232 1  |-  ( ph  -> 
<. 1 ,  K >. PolyAP 
F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1398    e. wcel 1823    =/= wne 2649   A.wral 2804   E.wrex 2805   _Vcvv 3106    u. cun 3459    C_ wss 3461   (/)c0 3783   {csn 4016   <.cop 4022   class class class wbr 4439    |-> cmpt 4497    X. cxp 4986   `'ccnv 4987   dom cdm 4988   ran crn 4989   "cima 4991    Fn wfn 5565   -->wf 5566   -1-1-onto->wf1o 5569   ` cfv 5570  (class class class)co 6270    ^m cmap 7412   Fincfn 7509   CCcc 9479   0cc0 9481   1c1 9482    + caddc 9484    x. cmul 9486    - cmin 9796   NNcn 10531   2c2 10581   NN0cn0 10791   ZZcz 10860   ZZ>=cuz 11082   ...cfz 11675   #chash 12387  APcvdwa 14567   PolyAP cvdwp 14569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-1st 6773  df-2nd 6774  df-recs 7034  df-rdg 7068  df-1o 7122  df-er 7303  df-map 7414  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513  df-card 8311  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-nn 10532  df-2 10590  df-n0 10792  df-z 10861  df-uz 11083  df-fz 11676  df-hash 12388  df-vdwap 14570  df-vdwpc 14572
This theorem is referenced by:  vdwlem10  14592
  Copyright terms: Public domain W3C validator