Metamath Proof Explorer

Theorem vdwlem8

Description: Lemma for vdw . (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses 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 vdwlem8 
|- ( ph -> <. 1 , K >. PolyAP F )

Proof

Step Hyp Ref Expression
1 vdwlem8.r 
 |-  ( ph -> R e. Fin )
2 vdwlem8.k 
 |-  ( ph -> K e. ( ZZ>= ` 2 ) )
3 vdwlem8.w 
 |-  ( ph -> W e. NN )
4 vdwlem8.f 
 |-  ( ph -> F : ( 1 ... ( 2 x. W ) ) --> R )
5 vdwlem8.c 
 |-  C e. _V
6 vdwlem8.a 
 |-  ( ph -> A e. NN )
7 vdwlem8.d 
 |-  ( ph -> D e. NN )
8 vdwlem8.s 
 |-  ( ph -> ( A ( AP ` K ) D ) C_ ( `' G " { C } ) )
9 vdwlem8.g 
 |-  G = ( x e. ( 1 ... W ) |-> ( F ` ( x + W ) ) )
10 6 nncnd 
 |-  ( ph -> A e. CC )
11 7 nncnd 
 |-  ( ph -> D e. CC )
12 10 11 addcomd 
 |-  ( ph -> ( A + D ) = ( D + A ) )
13 12 oveq2d 
 |-  ( ph -> ( W - ( A + D ) ) = ( W - ( D + A ) ) )
14 3 nncnd 
 |-  ( ph -> W e. CC )
15 14 11 10 subsub4d 
 |-  ( ph -> ( ( W - D ) - A ) = ( W - ( D + A ) ) )
16 13 15 eqtr4d 
 |-  ( ph -> ( W - ( A + D ) ) = ( ( W - D ) - A ) )
17 16 oveq2d 
 |-  ( ph -> ( ( A + A ) + ( W - ( A + D ) ) ) = ( ( A + A ) + ( ( W - D ) - A ) ) )
18 14 11 subcld 
 |-  ( ph -> ( W - D ) e. CC )
19 10 10 18 ppncand 
 |-  ( ph -> ( ( A + A ) + ( ( W - D ) - A ) ) = ( A + ( W - D ) ) )
20 17 19 eqtrd 
 |-  ( ph -> ( ( A + A ) + ( W - ( A + D ) ) ) = ( A + ( W - D ) ) )
21 6 6 nnaddcld 
 |-  ( ph -> ( A + A ) e. NN )
22 cnvimass 
 |-  ( `' G " { C } ) C_ dom G
23 fvex 
 |-  ( F ` ( x + W ) ) e. _V
24 23 9 dmmpti 
 |-  dom G = ( 1 ... W )
25 22 24 sseqtri 
 |-  ( `' G " { C } ) C_ ( 1 ... W )
26 8 25 sstrdi 
 |-  ( ph -> ( A ( AP ` K ) D ) C_ ( 1 ... W ) )
27 ssun2 
 |-  ( ( A + D ) ( AP ` ( K - 1 ) ) D ) C_ ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) )
28 uz2m1nn 
 |-  ( K e. ( ZZ>= ` 2 ) -> ( K - 1 ) e. NN )
29 2 28 syl 
 |-  ( ph -> ( K - 1 ) e. NN )
30 6 7 nnaddcld 
 |-  ( ph -> ( A + D ) e. NN )
31 vdwapid1 
 |-  ( ( ( K - 1 ) e. NN /\ ( A + D ) e. NN /\ D e. NN ) -> ( A + D ) e. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) )
32 29 30 7 31 syl3anc 
 |-  ( ph -> ( A + D ) e. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) )
33 27 32 sselid 
 |-  ( ph -> ( A + D ) e. ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) )
34 eluz2nn 
 |-  ( K e. ( ZZ>= ` 2 ) -> K e. NN )
35 2 34 syl 
 |-  ( ph -> K e. NN )
36 35 nncnd 
 |-  ( ph -> K e. CC )
37 ax-1cn 
 |-  1 e. CC
38 npcan 
 |-  ( ( K e. CC /\ 1 e. CC ) -> ( ( K - 1 ) + 1 ) = K )
39 36 37 38 sylancl 
 |-  ( ph -> ( ( K - 1 ) + 1 ) = K )
40 39 fveq2d 
 |-  ( ph -> ( AP ` ( ( K - 1 ) + 1 ) ) = ( AP ` K ) )
41 40 oveqd 
 |-  ( ph -> ( A ( AP ` ( ( K - 1 ) + 1 ) ) D ) = ( A ( AP ` K ) D ) )
42 29 nnnn0d 
 |-  ( ph -> ( K - 1 ) e. NN0 )
43 vdwapun 
 |-  ( ( ( K - 1 ) e. NN0 /\ A e. NN /\ D e. NN ) -> ( A ( AP ` ( ( K - 1 ) + 1 ) ) D ) = ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) )
44 42 6 7 43 syl3anc 
 |-  ( ph -> ( A ( AP ` ( ( K - 1 ) + 1 ) ) D ) = ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) )
45 41 44 eqtr3d 
 |-  ( ph -> ( A ( AP ` K ) D ) = ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) )
46 33 45 eleqtrrd 
 |-  ( ph -> ( A + D ) e. ( A ( AP ` K ) D ) )
47 26 46 sseldd 
 |-  ( ph -> ( A + D ) e. ( 1 ... W ) )
48 elfzuz3 
 |-  ( ( A + D ) e. ( 1 ... W ) -> W e. ( ZZ>= ` ( A + D ) ) )
49 uznn0sub 
 |-  ( W e. ( ZZ>= ` ( A + D ) ) -> ( W - ( A + D ) ) e. NN0 )
50 47 48 49 3syl 
 |-  ( ph -> ( W - ( A + D ) ) e. NN0 )
51 nnnn0addcl 
 |-  ( ( ( A + A ) e. NN /\ ( W - ( A + D ) ) e. NN0 ) -> ( ( A + A ) + ( W - ( A + D ) ) ) e. NN )
52 21 50 51 syl2anc 
 |-  ( ph -> ( ( A + A ) + ( W - ( A + D ) ) ) e. NN )
53 20 52 eqeltrrd 
 |-  ( ph -> ( A + ( W - D ) ) e. NN )
54 1nn 
 |-  1 e. NN
55 f1osng 
 |-  ( ( 1 e. NN /\ D e. NN ) -> { <. 1 , D >. } : { 1 } -1-1-onto-> { D } )
56 54 7 55 sylancr 
 |-  ( ph -> { <. 1 , D >. } : { 1 } -1-1-onto-> { D } )
57 f1of 
 |-  ( { <. 1 , D >. } : { 1 } -1-1-onto-> { D } -> { <. 1 , D >. } : { 1 } --> { D } )
58 56 57 syl 
 |-  ( ph -> { <. 1 , D >. } : { 1 } --> { D } )
59 7 snssd 
 |-  ( ph -> { D } C_ NN )
60 58 59 fssd 
 |-  ( ph -> { <. 1 , D >. } : { 1 } --> NN )
61 1z 
 |-  1 e. ZZ
62 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
63 61 62 ax-mp 
 |-  ( 1 ... 1 ) = { 1 }
64 63 feq2i 
 |-  ( { <. 1 , D >. } : ( 1 ... 1 ) --> NN <-> { <. 1 , D >. } : { 1 } --> NN )
65 60 64 sylibr 
 |-  ( ph -> { <. 1 , D >. } : ( 1 ... 1 ) --> NN )
66 nnex 
 |-  NN e. _V
67 ovex 
 |-  ( 1 ... 1 ) e. _V
68 66 67 elmap 
 |-  ( { <. 1 , D >. } e. ( NN ^m ( 1 ... 1 ) ) <-> { <. 1 , D >. } : ( 1 ... 1 ) --> NN )
69 65 68 sylibr 
 |-  ( ph -> { <. 1 , D >. } e. ( NN ^m ( 1 ... 1 ) ) )
70 6 3 nnaddcld 
 |-  ( ph -> ( A + W ) e. NN )
71 70 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + W ) e. NN )
72 elfznn0 
 |-  ( m e. ( 0 ... ( K - 1 ) ) -> m e. NN0 )
73 7 nnnn0d 
 |-  ( ph -> D e. NN0 )
74 nn0mulcl 
 |-  ( ( m e. NN0 /\ D e. NN0 ) -> ( m x. D ) e. NN0 )
75 72 73 74 syl2anr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. D ) e. NN0 )
76 nnnn0addcl 
 |-  ( ( ( A + W ) e. NN /\ ( m x. D ) e. NN0 ) -> ( ( A + W ) + ( m x. D ) ) e. NN )
77 71 75 76 syl2anc 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A + W ) + ( m x. D ) ) e. NN )
78 nnuz 
 |-  NN = ( ZZ>= ` 1 )
79 77 78 eleqtrdi 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A + W ) + ( m x. D ) ) e. ( ZZ>= ` 1 ) )
80 8 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A ( AP ` K ) D ) C_ ( `' G " { C } ) )
81 eqid 
 |-  ( A + ( m x. D ) ) = ( A + ( m x. D ) )
82 oveq1 
 |-  ( n = m -> ( n x. D ) = ( m x. D ) )
83 82 oveq2d 
 |-  ( n = m -> ( A + ( n x. D ) ) = ( A + ( m x. D ) ) )
84 83 rspceeqv 
 |-  ( ( 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 ) ) )
85 81 84 mpan2 
 |-  ( m e. ( 0 ... ( K - 1 ) ) -> E. n e. ( 0 ... ( K - 1 ) ) ( A + ( m x. D ) ) = ( A + ( n x. D ) ) )
86 35 nnnn0d 
 |-  ( ph -> K e. NN0 )
87 vdwapval 
 |-  ( ( 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 ) ) ) )
88 86 6 7 87 syl3anc 
 |-  ( ph -> ( ( A + ( m x. D ) ) e. ( A ( AP ` K ) D ) <-> E. n e. ( 0 ... ( K - 1 ) ) ( A + ( m x. D ) ) = ( A + ( n x. D ) ) ) )
89 88 biimpar 
 |-  ( ( ph /\ E. n e. ( 0 ... ( K - 1 ) ) ( A + ( m x. D ) ) = ( A + ( n x. D ) ) ) -> ( A + ( m x. D ) ) e. ( A ( AP ` K ) D ) )
90 85 89 sylan2 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + ( m x. D ) ) e. ( A ( AP ` K ) D ) )
91 80 90 sseldd 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + ( m x. D ) ) e. ( `' G " { C } ) )
92 23 9 fnmpti 
 |-  G Fn ( 1 ... W )
93 fniniseg 
 |-  ( G Fn ( 1 ... W ) -> ( ( A + ( m x. D ) ) e. ( `' G " { C } ) <-> ( ( A + ( m x. D ) ) e. ( 1 ... W ) /\ ( G ` ( A + ( m x. D ) ) ) = C ) ) )
94 92 93 ax-mp 
 |-  ( ( A + ( m x. D ) ) e. ( `' G " { C } ) <-> ( ( A + ( m x. D ) ) e. ( 1 ... W ) /\ ( G ` ( A + ( m x. D ) ) ) = C ) )
95 91 94 sylib 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A + ( m x. D ) ) e. ( 1 ... W ) /\ ( G ` ( A + ( m x. D ) ) ) = C ) )
96 95 simpld 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + ( m x. D ) ) e. ( 1 ... W ) )
97 elfzuz3 
 |-  ( ( A + ( m x. D ) ) e. ( 1 ... W ) -> W e. ( ZZ>= ` ( A + ( m x. D ) ) ) )
98 eluzelz 
 |-  ( W e. ( ZZ>= ` ( A + ( m x. D ) ) ) -> W e. ZZ )
99 eluzadd 
 |-  ( ( W e. ( ZZ>= ` ( A + ( m x. D ) ) ) /\ W e. ZZ ) -> ( W + W ) e. ( ZZ>= ` ( ( A + ( m x. D ) ) + W ) ) )
100 98 99 mpdan 
 |-  ( W e. ( ZZ>= ` ( A + ( m x. D ) ) ) -> ( W + W ) e. ( ZZ>= ` ( ( A + ( m x. D ) ) + W ) ) )
101 96 97 100 3syl 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( W + W ) e. ( ZZ>= ` ( ( A + ( m x. D ) ) + W ) ) )
102 14 2timesd 
 |-  ( ph -> ( 2 x. W ) = ( W + W ) )
103 102 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( 2 x. W ) = ( W + W ) )
104 10 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> A e. CC )
105 14 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> W e. CC )
106 75 nn0cnd 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. D ) e. CC )
107 104 105 106 add32d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A + W ) + ( m x. D ) ) = ( ( A + ( m x. D ) ) + W ) )
108 107 fveq2d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ZZ>= ` ( ( A + W ) + ( m x. D ) ) ) = ( ZZ>= ` ( ( A + ( m x. D ) ) + W ) ) )
109 101 103 108 3eltr4d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( 2 x. W ) e. ( ZZ>= ` ( ( A + W ) + ( m x. D ) ) ) )
110 elfzuzb 
 |-  ( ( ( 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 ) ) ) ) )
111 79 109 110 sylanbrc 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A + W ) + ( m x. D ) ) e. ( 1 ... ( 2 x. W ) ) )
112 107 fveq2d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( F ` ( ( A + W ) + ( m x. D ) ) ) = ( F ` ( ( A + ( m x. D ) ) + W ) ) )
113 fvoveq1 
 |-  ( x = ( A + ( m x. D ) ) -> ( F ` ( x + W ) ) = ( F ` ( ( A + ( m x. D ) ) + W ) ) )
114 fvex 
 |-  ( F ` ( ( A + ( m x. D ) ) + W ) ) e. _V
115 113 9 114 fvmpt 
 |-  ( ( A + ( m x. D ) ) e. ( 1 ... W ) -> ( G ` ( A + ( m x. D ) ) ) = ( F ` ( ( A + ( m x. D ) ) + W ) ) )
116 96 115 syl 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( G ` ( A + ( m x. D ) ) ) = ( F ` ( ( A + ( m x. D ) ) + W ) ) )
117 95 simprd 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( G ` ( A + ( m x. D ) ) ) = C )
118 112 116 117 3eqtr2d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( F ` ( ( A + W ) + ( m x. D ) ) ) = C )
119 111 118 jca 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( A + W ) + ( m x. D ) ) e. ( 1 ... ( 2 x. W ) ) /\ ( F ` ( ( A + W ) + ( m x. D ) ) ) = C ) )
120 eleq1 
 |-  ( x = ( ( A + W ) + ( m x. D ) ) -> ( x e. ( 1 ... ( 2 x. W ) ) <-> ( ( A + W ) + ( m x. D ) ) e. ( 1 ... ( 2 x. W ) ) ) )
121 fveqeq2 
 |-  ( x = ( ( A + W ) + ( m x. D ) ) -> ( ( F ` x ) = C <-> ( F ` ( ( A + W ) + ( m x. D ) ) ) = C ) )
122 120 121 anbi12d 
 |-  ( 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 ) ) )
123 119 122 syl5ibrcom 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( x = ( ( A + W ) + ( m x. D ) ) -> ( x e. ( 1 ... ( 2 x. W ) ) /\ ( F ` x ) = C ) ) )
124 123 rexlimdva 
 |-  ( ph -> ( E. m e. ( 0 ... ( K - 1 ) ) x = ( ( A + W ) + ( m x. D ) ) -> ( x e. ( 1 ... ( 2 x. W ) ) /\ ( F ` x ) = C ) ) )
125 vdwapval 
 |-  ( ( 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 ) ) ) )
126 86 70 7 125 syl3anc 
 |-  ( ph -> ( x e. ( ( A + W ) ( AP ` K ) D ) <-> E. m e. ( 0 ... ( K - 1 ) ) x = ( ( A + W ) + ( m x. D ) ) ) )
127 ffn 
 |-  ( F : ( 1 ... ( 2 x. W ) ) --> R -> F Fn ( 1 ... ( 2 x. W ) ) )
128 fniniseg 
 |-  ( F Fn ( 1 ... ( 2 x. W ) ) -> ( x e. ( `' F " { C } ) <-> ( x e. ( 1 ... ( 2 x. W ) ) /\ ( F ` x ) = C ) ) )
129 4 127 128 3syl 
 |-  ( ph -> ( x e. ( `' F " { C } ) <-> ( x e. ( 1 ... ( 2 x. W ) ) /\ ( F ` x ) = C ) ) )
130 124 126 129 3imtr4d 
 |-  ( ph -> ( x e. ( ( A + W ) ( AP ` K ) D ) -> x e. ( `' F " { C } ) ) )
131 130 ssrdv 
 |-  ( ph -> ( ( A + W ) ( AP ` K ) D ) C_ ( `' F " { C } ) )
132 fvsng 
 |-  ( ( 1 e. NN /\ D e. NN ) -> ( { <. 1 , D >. } ` 1 ) = D )
133 54 7 132 sylancr 
 |-  ( ph -> ( { <. 1 , D >. } ` 1 ) = D )
134 133 oveq2d 
 |-  ( ph -> ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) = ( ( A + ( W - D ) ) + D ) )
135 10 18 11 addassd 
 |-  ( ph -> ( ( A + ( W - D ) ) + D ) = ( A + ( ( W - D ) + D ) ) )
136 14 11 npcand 
 |-  ( ph -> ( ( W - D ) + D ) = W )
137 136 oveq2d 
 |-  ( ph -> ( A + ( ( W - D ) + D ) ) = ( A + W ) )
138 134 135 137 3eqtrd 
 |-  ( ph -> ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) = ( A + W ) )
139 138 133 oveq12d 
 |-  ( ph -> ( ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ( AP ` K ) ( { <. 1 , D >. } ` 1 ) ) = ( ( A + W ) ( AP ` K ) D ) )
140 138 fveq2d 
 |-  ( ph -> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) = ( F ` ( A + W ) ) )
141 vdwapid1 
 |-  ( ( K e. NN /\ A e. NN /\ D e. NN ) -> A e. ( A ( AP ` K ) D ) )
142 35 6 7 141 syl3anc 
 |-  ( ph -> A e. ( A ( AP ` K ) D ) )
143 8 142 sseldd 
 |-  ( ph -> A e. ( `' G " { C } ) )
144 fniniseg 
 |-  ( G Fn ( 1 ... W ) -> ( A e. ( `' G " { C } ) <-> ( A e. ( 1 ... W ) /\ ( G ` A ) = C ) ) )
145 92 144 ax-mp 
 |-  ( A e. ( `' G " { C } ) <-> ( A e. ( 1 ... W ) /\ ( G ` A ) = C ) )
146 143 145 sylib 
 |-  ( ph -> ( A e. ( 1 ... W ) /\ ( G ` A ) = C ) )
147 146 simpld 
 |-  ( ph -> A e. ( 1 ... W ) )
148 fvoveq1 
 |-  ( x = A -> ( F ` ( x + W ) ) = ( F ` ( A + W ) ) )
149 fvex 
 |-  ( F ` ( A + W ) ) e. _V
150 148 9 149 fvmpt 
 |-  ( A e. ( 1 ... W ) -> ( G ` A ) = ( F ` ( A + W ) ) )
151 147 150 syl 
 |-  ( ph -> ( G ` A ) = ( F ` ( A + W ) ) )
152 146 simprd 
 |-  ( ph -> ( G ` A ) = C )
153 140 151 152 3eqtr2d 
 |-  ( ph -> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) = C )
154 153 sneqd 
 |-  ( ph -> { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } = { C } )
155 154 imaeq2d 
 |-  ( ph -> ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } ) = ( `' F " { C } ) )
156 131 139 155 3sstr4d 
 |-  ( ph -> ( ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ( AP ` K ) ( { <. 1 , D >. } ` 1 ) ) C_ ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } ) )
157 156 ralrimivw 
 |-  ( 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 ) ) ) } ) )
158 153 mpteq2dv 
 |-  ( ph -> ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) = ( i e. ( 1 ... 1 ) |-> C ) )
159 fconstmpt 
 |-  ( ( 1 ... 1 ) X. { C } ) = ( i e. ( 1 ... 1 ) |-> C )
160 158 159 eqtr4di 
 |-  ( ph -> ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) = ( ( 1 ... 1 ) X. { C } ) )
161 160 rneqd 
 |-  ( ph -> ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) = ran ( ( 1 ... 1 ) X. { C } ) )
162 elfz3 
 |-  ( 1 e. ZZ -> 1 e. ( 1 ... 1 ) )
163 ne0i 
 |-  ( 1 e. ( 1 ... 1 ) -> ( 1 ... 1 ) =/= (/) )
164 61 162 163 mp2b 
 |-  ( 1 ... 1 ) =/= (/)
165 rnxp 
 |-  ( ( 1 ... 1 ) =/= (/) -> ran ( ( 1 ... 1 ) X. { C } ) = { C } )
166 164 165 ax-mp 
 |-  ran ( ( 1 ... 1 ) X. { C } ) = { C }
167 161 166 eqtrdi 
 |-  ( ph -> ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) = { C } )
168 167 fveq2d 
 |-  ( ph -> ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) ) = ( # ` { C } ) )
169 hashsng 
 |-  ( C e. _V -> ( # ` { C } ) = 1 )
170 5 169 ax-mp 
 |-  ( # ` { C } ) = 1
171 168 170 eqtrdi 
 |-  ( ph -> ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) ) = 1 )
172 oveq1 
 |-  ( a = ( A + ( W - D ) ) -> ( a + ( d ` i ) ) = ( ( A + ( W - D ) ) + ( d ` i ) ) )
173 172 oveq1d 
 |-  ( a = ( A + ( W - D ) ) -> ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) = ( ( ( A + ( W - D ) ) + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) )
174 fvoveq1 
 |-  ( a = ( A + ( W - D ) ) -> ( F ` ( a + ( d ` i ) ) ) = ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) )
175 174 sneqd 
 |-  ( a = ( A + ( W - D ) ) -> { ( F ` ( a + ( d ` i ) ) ) } = { ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) } )
176 175 imaeq2d 
 |-  ( a = ( A + ( W - D ) ) -> ( `' F " { ( F ` ( a + ( d ` i ) ) ) } ) = ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) } ) )
177 173 176 sseq12d 
 |-  ( 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 ) ) ) } ) ) )
178 177 ralbidv 
 |-  ( 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 ) ) ) } ) ) )
179 174 mpteq2dv 
 |-  ( a = ( A + ( W - D ) ) -> ( i e. ( 1 ... 1 ) |-> ( F ` ( a + ( d ` i ) ) ) ) = ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) ) )
180 179 rneqd 
 |-  ( a = ( A + ( W - D ) ) -> ran ( i e. ( 1 ... 1 ) |-> ( F ` ( a + ( d ` i ) ) ) ) = ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) ) )
181 180 fveqeq2d 
 |-  ( 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 ) )
182 178 181 anbi12d 
 |-  ( 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 ) ) )
183 fveq1 
 |-  ( d = { <. 1 , D >. } -> ( d ` i ) = ( { <. 1 , D >. } ` i ) )
184 elfz1eq 
 |-  ( i e. ( 1 ... 1 ) -> i = 1 )
185 184 fveq2d 
 |-  ( i e. ( 1 ... 1 ) -> ( { <. 1 , D >. } ` i ) = ( { <. 1 , D >. } ` 1 ) )
186 183 185 sylan9eq 
 |-  ( ( d = { <. 1 , D >. } /\ i e. ( 1 ... 1 ) ) -> ( d ` i ) = ( { <. 1 , D >. } ` 1 ) )
187 186 oveq2d 
 |-  ( ( d = { <. 1 , D >. } /\ i e. ( 1 ... 1 ) ) -> ( ( A + ( W - D ) ) + ( d ` i ) ) = ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) )
188 187 186 oveq12d 
 |-  ( ( 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 ) ) )
189 187 fveq2d 
 |-  ( ( d = { <. 1 , D >. } /\ i e. ( 1 ... 1 ) ) -> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) = ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) )
190 189 sneqd 
 |-  ( ( d = { <. 1 , D >. } /\ i e. ( 1 ... 1 ) ) -> { ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) } = { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } )
191 190 imaeq2d 
 |-  ( ( d = { <. 1 , D >. } /\ i e. ( 1 ... 1 ) ) -> ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) } ) = ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } ) )
192 188 191 sseq12d 
 |-  ( ( 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 ) ) ) } ) ) )
193 192 ralbidva 
 |-  ( 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 ) ) ) } ) ) )
194 189 mpteq2dva 
 |-  ( d = { <. 1 , D >. } -> ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) ) = ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) )
195 194 rneqd 
 |-  ( 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 ) ) ) ) )
196 195 fveqeq2d 
 |-  ( 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 ) )
197 193 196 anbi12d 
 |-  ( 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 ) ) )
198 182 197 rspc2ev 
 |-  ( ( ( 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 ) )
199 53 69 157 171 198 syl112anc 
 |-  ( 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 ) )
200 ovex 
 |-  ( 1 ... ( 2 x. W ) ) e. _V
201 54 a1i 
 |-  ( ph -> 1 e. NN )
202 eqid 
 |-  ( 1 ... 1 ) = ( 1 ... 1 )
203 200 86 4 201 202 vdwpc 
 |-  ( 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 ) ) )
204 199 203 mpbird 
 |-  ( ph -> <. 1 , K >. PolyAP F )