Metamath Proof Explorer

Theorem vdwlem9

Description: Lemma for vdw . (Contributed by Mario Carneiro, 12-Sep-2014)

Ref Expression
Hypotheses vdw.r 
|- ( ph -> R e. Fin )
vdwlem9.k 
|- ( ph -> K e. ( ZZ>= ` 2 ) )
vdwlem9.s 
|- ( ph -> A. s e. Fin E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f )
vdwlem9.m 
|- ( ph -> M e. NN )
vdwlem9.w 
|- ( ph -> W e. NN )
vdwlem9.g 
|- ( ph -> A. g e. ( R ^m ( 1 ... W ) ) ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) )
vdwlem9.v 
|- ( ph -> V e. NN )
vdwlem9.a 
|- ( ph -> A. f e. ( ( R ^m ( 1 ... W ) ) ^m ( 1 ... V ) ) K MonoAP f )
vdwlem9.h 
|- ( ph -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )
vdwlem9.f 
|- F = ( x e. ( 1 ... V ) |-> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) )
Assertion vdwlem9 
|- ( ph -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) )

Proof

Step Hyp Ref Expression
1 vdw.r 
 |-  ( ph -> R e. Fin )
2 vdwlem9.k 
 |-  ( ph -> K e. ( ZZ>= ` 2 ) )
3 vdwlem9.s 
 |-  ( ph -> A. s e. Fin E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f )
4 vdwlem9.m 
 |-  ( ph -> M e. NN )
5 vdwlem9.w 
 |-  ( ph -> W e. NN )
6 vdwlem9.g 
 |-  ( ph -> A. g e. ( R ^m ( 1 ... W ) ) ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) )
7 vdwlem9.v 
 |-  ( ph -> V e. NN )
8 vdwlem9.a 
 |-  ( ph -> A. f e. ( ( R ^m ( 1 ... W ) ) ^m ( 1 ... V ) ) K MonoAP f )
9 vdwlem9.h 
 |-  ( ph -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )
10 vdwlem9.f 
 |-  F = ( x e. ( 1 ... V ) |-> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) )
11 breq2 
 |-  ( f = F -> ( K MonoAP f <-> K MonoAP F ) )
12 7 5 1 9 10 vdwlem4 
 |-  ( ph -> F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) )
13 ovex 
 |-  ( R ^m ( 1 ... W ) ) e. _V
14 ovex 
 |-  ( 1 ... V ) e. _V
15 13 14 elmap 
 |-  ( F e. ( ( R ^m ( 1 ... W ) ) ^m ( 1 ... V ) ) <-> F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) )
16 12 15 sylibr 
 |-  ( ph -> F e. ( ( R ^m ( 1 ... W ) ) ^m ( 1 ... V ) ) )
17 11 8 16 rspcdva 
 |-  ( ph -> K MonoAP F )
18 eluz2nn 
 |-  ( K e. ( ZZ>= ` 2 ) -> K e. NN )
19 2 18 syl 
 |-  ( ph -> K e. NN )
20 19 nnnn0d 
 |-  ( ph -> K e. NN0 )
21 14 20 12 vdwmc 
 |-  ( ph -> ( K MonoAP F <-> E. g E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) )
22 6 adantr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> A. g e. ( R ^m ( 1 ... W ) ) ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) )
23 simprr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a ( AP ` K ) d ) C_ ( `' F " { g } ) )
24 19 adantr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> K e. NN )
25 simprll 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. NN )
26 simprlr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> d e. NN )
27 vdwapid1 
 |-  ( ( K e. NN /\ a e. NN /\ d e. NN ) -> a e. ( a ( AP ` K ) d ) )
28 24 25 26 27 syl3anc 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. ( a ( AP ` K ) d ) )
29 23 28 sseldd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. ( `' F " { g } ) )
30 12 ffnd 
 |-  ( ph -> F Fn ( 1 ... V ) )
31 30 adantr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> F Fn ( 1 ... V ) )
32 fniniseg 
 |-  ( F Fn ( 1 ... V ) -> ( a e. ( `' F " { g } ) <-> ( a e. ( 1 ... V ) /\ ( F ` a ) = g ) ) )
33 31 32 syl 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a e. ( `' F " { g } ) <-> ( a e. ( 1 ... V ) /\ ( F ` a ) = g ) ) )
34 29 33 mpbid 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a e. ( 1 ... V ) /\ ( F ` a ) = g ) )
35 34 simprd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( F ` a ) = g )
36 12 adantr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) )
37 34 simpld 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. ( 1 ... V ) )
38 36 37 ffvelcdmd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( F ` a ) e. ( R ^m ( 1 ... W ) ) )
39 35 38 eqeltrrd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> g e. ( R ^m ( 1 ... W ) ) )
40 rsp 
 |-  ( A. g e. ( R ^m ( 1 ... W ) ) ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) -> ( g e. ( R ^m ( 1 ... W ) ) -> ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) )
41 22 39 40 sylc 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) )
42 7 adantr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> V e. NN )
43 5 adantr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> W e. NN )
44 1 adantr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> R e. Fin )
45 9 adantr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )
46 4 adantr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> M e. NN )
47 ovex 
 |-  ( 1 ... W ) e. _V
48 elmapg 
 |-  ( ( R e. Fin /\ ( 1 ... W ) e. _V ) -> ( g e. ( R ^m ( 1 ... W ) ) <-> g : ( 1 ... W ) --> R ) )
49 44 47 48 sylancl 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( g e. ( R ^m ( 1 ... W ) ) <-> g : ( 1 ... W ) --> R ) )
50 39 49 mpbid 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> g : ( 1 ... W ) --> R )
51 2 adantr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> K e. ( ZZ>= ` 2 ) )
52 42 43 44 45 10 46 50 51 25 26 23 vdwlem7 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( <. M , K >. PolyAP g -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP g ) ) )
53 olc 
 |-  ( ( K + 1 ) MonoAP g -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP g ) )
54 53 a1i 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( K + 1 ) MonoAP g -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP g ) ) )
55 52 54 jaod 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP g ) ) )
56 oveq1 
 |-  ( x = a -> ( x - 1 ) = ( a - 1 ) )
57 56 oveq1d 
 |-  ( x = a -> ( ( x - 1 ) + V ) = ( ( a - 1 ) + V ) )
58 57 oveq2d 
 |-  ( x = a -> ( W x. ( ( x - 1 ) + V ) ) = ( W x. ( ( a - 1 ) + V ) ) )
59 58 oveq2d 
 |-  ( x = a -> ( y + ( W x. ( ( x - 1 ) + V ) ) ) = ( y + ( W x. ( ( a - 1 ) + V ) ) ) )
60 59 fveq2d 
 |-  ( x = a -> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) = ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) )
61 60 mpteq2dv 
 |-  ( x = a -> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) )
62 47 mptex 
 |-  ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) e. _V
63 61 10 62 fvmpt 
 |-  ( a e. ( 1 ... V ) -> ( F ` a ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) )
64 37 63 syl 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( F ` a ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) )
65 64 35 eqtr3d 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) = g )
66 65 breq2d 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( K + 1 ) MonoAP ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) <-> ( K + 1 ) MonoAP g ) )
67 20 adantr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> K e. NN0 )
68 peano2nn0 
 |-  ( K e. NN0 -> ( K + 1 ) e. NN0 )
69 67 68 syl 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( K + 1 ) e. NN0 )
70 nnm1nn0 
 |-  ( a e. NN -> ( a - 1 ) e. NN0 )
71 25 70 syl 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a - 1 ) e. NN0 )
72 nn0nnaddcl 
 |-  ( ( ( a - 1 ) e. NN0 /\ V e. NN ) -> ( ( a - 1 ) + V ) e. NN )
73 71 42 72 syl2anc 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( a - 1 ) + V ) e. NN )
74 43 73 nnmulcld 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( ( a - 1 ) + V ) ) e. NN )
75 25 42 nnaddcld 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) e. NN )
76 43 75 nnmulcld 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( a + V ) ) e. NN )
77 76 nnzd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( a + V ) ) e. ZZ )
78 2nn 
 |-  2 e. NN
79 nnmulcl 
 |-  ( ( 2 e. NN /\ V e. NN ) -> ( 2 x. V ) e. NN )
80 78 7 79 sylancr 
 |-  ( ph -> ( 2 x. V ) e. NN )
81 5 80 nnmulcld 
 |-  ( ph -> ( W x. ( 2 x. V ) ) e. NN )
82 81 nnzd 
 |-  ( ph -> ( W x. ( 2 x. V ) ) e. ZZ )
83 82 adantr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( 2 x. V ) ) e. ZZ )
84 25 nnred 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. RR )
85 42 nnred 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> V e. RR )
86 elfzle2 
 |-  ( a e. ( 1 ... V ) -> a <_ V )
87 37 86 syl 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a <_ V )
88 84 85 85 87 leadd1dd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) <_ ( V + V ) )
89 42 nncnd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> V e. CC )
90 89 2timesd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 2 x. V ) = ( V + V ) )
91 88 90 breqtrrd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) <_ ( 2 x. V ) )
92 75 nnred 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) e. RR )
93 80 nnred 
 |-  ( ph -> ( 2 x. V ) e. RR )
94 93 adantr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 2 x. V ) e. RR )
95 43 nnred 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> W e. RR )
96 43 nngt0d 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> 0 < W )
97 lemul2 
 |-  ( ( ( a + V ) e. RR /\ ( 2 x. V ) e. RR /\ ( W e. RR /\ 0 < W ) ) -> ( ( a + V ) <_ ( 2 x. V ) <-> ( W x. ( a + V ) ) <_ ( W x. ( 2 x. V ) ) ) )
98 92 94 95 96 97 syl112anc 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( a + V ) <_ ( 2 x. V ) <-> ( W x. ( a + V ) ) <_ ( W x. ( 2 x. V ) ) ) )
99 91 98 mpbid 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( a + V ) ) <_ ( W x. ( 2 x. V ) ) )
100 eluz2 
 |-  ( ( W x. ( 2 x. V ) ) e. ( ZZ>= ` ( W x. ( a + V ) ) ) <-> ( ( W x. ( a + V ) ) e. ZZ /\ ( W x. ( 2 x. V ) ) e. ZZ /\ ( W x. ( a + V ) ) <_ ( W x. ( 2 x. V ) ) ) )
101 77 83 99 100 syl3anbrc 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( 2 x. V ) ) e. ( ZZ>= ` ( W x. ( a + V ) ) ) )
102 43 nncnd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> W e. CC )
103 1cnd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> 1 e. CC )
104 71 nn0cnd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a - 1 ) e. CC )
105 104 89 addcld 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( a - 1 ) + V ) e. CC )
106 102 103 105 adddid 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( 1 + ( ( a - 1 ) + V ) ) ) = ( ( W x. 1 ) + ( W x. ( ( a - 1 ) + V ) ) ) )
107 103 104 89 addassd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( 1 + ( a - 1 ) ) + V ) = ( 1 + ( ( a - 1 ) + V ) ) )
108 ax-1cn 
 |-  1 e. CC
109 25 nncnd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. CC )
110 pncan3 
 |-  ( ( 1 e. CC /\ a e. CC ) -> ( 1 + ( a - 1 ) ) = a )
111 108 109 110 sylancr 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 1 + ( a - 1 ) ) = a )
112 111 oveq1d 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( 1 + ( a - 1 ) ) + V ) = ( a + V ) )
113 107 112 eqtr3d 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 1 + ( ( a - 1 ) + V ) ) = ( a + V ) )
114 113 oveq2d 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( 1 + ( ( a - 1 ) + V ) ) ) = ( W x. ( a + V ) ) )
115 102 mulridd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. 1 ) = W )
116 115 oveq1d 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( W x. 1 ) + ( W x. ( ( a - 1 ) + V ) ) ) = ( W + ( W x. ( ( a - 1 ) + V ) ) ) )
117 106 114 116 3eqtr3d 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( a + V ) ) = ( W + ( W x. ( ( a - 1 ) + V ) ) ) )
118 117 fveq2d 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ZZ>= ` ( W x. ( a + V ) ) ) = ( ZZ>= ` ( W + ( W x. ( ( a - 1 ) + V ) ) ) ) )
119 101 118 eleqtrd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( 2 x. V ) ) e. ( ZZ>= ` ( W + ( W x. ( ( a - 1 ) + V ) ) ) ) )
120 fvoveq1 
 |-  ( y = z -> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) = ( H ` ( z + ( W x. ( ( a - 1 ) + V ) ) ) ) )
121 120 cbvmptv 
 |-  ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) = ( z e. ( 1 ... W ) |-> ( H ` ( z + ( W x. ( ( a - 1 ) + V ) ) ) ) )
122 44 69 43 74 45 119 121 vdwlem2 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( K + 1 ) MonoAP ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) -> ( K + 1 ) MonoAP H ) )
123 66 122 sylbird 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( K + 1 ) MonoAP g -> ( K + 1 ) MonoAP H ) )
124 123 orim2d 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP g ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) ) )
125 55 124 syld 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) ) )
126 41 125 mpd 
 |-  ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) )
127 126 expr 
 |-  ( ( ph /\ ( a e. NN /\ d e. NN ) ) -> ( ( a ( AP ` K ) d ) C_ ( `' F " { g } ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) ) )
128 127 rexlimdvva 
 |-  ( ph -> ( E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { g } ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) ) )
129 128 exlimdv 
 |-  ( ph -> ( E. g E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { g } ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) ) )
130 21 129 sylbid 
 |-  ( ph -> ( K MonoAP F -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) ) )
131 17 130 mpd 
 |-  ( ph -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) )