Metamath Proof Explorer

Theorem vdwlem6

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

Ref Expression
Hypotheses vdwlem3.v 
|- ( ph -> V e. NN )
vdwlem3.w 
|- ( ph -> W e. NN )
vdwlem4.r 
|- ( ph -> R e. Fin )
vdwlem4.h 
|- ( ph -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )
vdwlem4.f 
|- F = ( x e. ( 1 ... V ) |-> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) )
vdwlem7.m 
|- ( ph -> M e. NN )
vdwlem7.g 
|- ( ph -> G : ( 1 ... W ) --> R )
vdwlem7.k 
|- ( ph -> K e. ( ZZ>= ` 2 ) )
vdwlem7.a 
|- ( ph -> A e. NN )
vdwlem7.d 
|- ( ph -> D e. NN )
vdwlem7.s 
|- ( ph -> ( A ( AP ` K ) D ) C_ ( `' F " { G } ) )
vdwlem6.b 
|- ( ph -> B e. NN )
vdwlem6.e 
|- ( ph -> E : ( 1 ... M ) --> NN )
vdwlem6.s 
|- ( ph -> A. i e. ( 1 ... M ) ( ( B + ( E ` i ) ) ( AP ` K ) ( E ` i ) ) C_ ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )
vdwlem6.j 
|- J = ( i e. ( 1 ... M ) |-> ( G ` ( B + ( E ` i ) ) ) )
vdwlem6.r 
|- ( ph -> ( # ` ran J ) = M )
vdwlem6.t 
|- T = ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) )
vdwlem6.p 
|- P = ( j e. ( 1 ... ( M + 1 ) ) |-> ( if ( j = ( M + 1 ) , 0 , ( E ` j ) ) + ( W x. D ) ) )
Assertion vdwlem6 
|- ( ph -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP G ) )

Proof

Step Hyp Ref Expression
1 vdwlem3.v 
 |-  ( ph -> V e. NN )
2 vdwlem3.w 
 |-  ( ph -> W e. NN )
3 vdwlem4.r 
 |-  ( ph -> R e. Fin )
4 vdwlem4.h 
 |-  ( ph -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )
5 vdwlem4.f 
 |-  F = ( x e. ( 1 ... V ) |-> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) )
6 vdwlem7.m 
 |-  ( ph -> M e. NN )
7 vdwlem7.g 
 |-  ( ph -> G : ( 1 ... W ) --> R )
8 vdwlem7.k 
 |-  ( ph -> K e. ( ZZ>= ` 2 ) )
9 vdwlem7.a 
 |-  ( ph -> A e. NN )
10 vdwlem7.d 
 |-  ( ph -> D e. NN )
11 vdwlem7.s 
 |-  ( ph -> ( A ( AP ` K ) D ) C_ ( `' F " { G } ) )
12 vdwlem6.b 
 |-  ( ph -> B e. NN )
13 vdwlem6.e 
 |-  ( ph -> E : ( 1 ... M ) --> NN )
14 vdwlem6.s 
 |-  ( ph -> A. i e. ( 1 ... M ) ( ( B + ( E ` i ) ) ( AP ` K ) ( E ` i ) ) C_ ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )
15 vdwlem6.j 
 |-  J = ( i e. ( 1 ... M ) |-> ( G ` ( B + ( E ` i ) ) ) )
16 vdwlem6.r 
 |-  ( ph -> ( # ` ran J ) = M )
17 vdwlem6.t 
 |-  T = ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) )
18 vdwlem6.p 
 |-  P = ( j e. ( 1 ... ( M + 1 ) ) |-> ( if ( j = ( M + 1 ) , 0 , ( E ` j ) ) + ( W x. D ) ) )
19 fvex 
 |-  ( G ` ( B + ( E ` i ) ) ) e. _V
20 19 15 fnmpti 
 |-  J Fn ( 1 ... M )
21 fvelrnb 
 |-  ( J Fn ( 1 ... M ) -> ( ( G ` B ) e. ran J <-> E. m e. ( 1 ... M ) ( J ` m ) = ( G ` B ) ) )
22 20 21 ax-mp 
 |-  ( ( G ` B ) e. ran J <-> E. m e. ( 1 ... M ) ( J ` m ) = ( G ` B ) )
23 3 adantr 
 |-  ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> R e. Fin )
24 eluz2nn 
 |-  ( K e. ( ZZ>= ` 2 ) -> K e. NN )
25 8 24 syl 
 |-  ( ph -> K e. NN )
26 25 adantr 
 |-  ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> K e. NN )
27 2 adantr 
 |-  ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> W e. NN )
28 7 adantr 
 |-  ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> G : ( 1 ... W ) --> R )
29 12 adantr 
 |-  ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> B e. NN )
30 6 adantr 
 |-  ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> M e. NN )
31 13 adantr 
 |-  ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> E : ( 1 ... M ) --> NN )
32 14 adantr 
 |-  ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> A. i e. ( 1 ... M ) ( ( B + ( E ` i ) ) ( AP ` K ) ( E ` i ) ) C_ ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )
33 simprl 
 |-  ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> m e. ( 1 ... M ) )
34 simprr 
 |-  ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> ( J ` m ) = ( G ` B ) )
35 fveq2 
 |-  ( i = m -> ( E ` i ) = ( E ` m ) )
36 35 oveq2d 
 |-  ( i = m -> ( B + ( E ` i ) ) = ( B + ( E ` m ) ) )
37 36 fveq2d 
 |-  ( i = m -> ( G ` ( B + ( E ` i ) ) ) = ( G ` ( B + ( E ` m ) ) ) )
38 fvex 
 |-  ( G ` ( B + ( E ` m ) ) ) e. _V
39 37 15 38 fvmpt 
 |-  ( m e. ( 1 ... M ) -> ( J ` m ) = ( G ` ( B + ( E ` m ) ) ) )
40 33 39 syl 
 |-  ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> ( J ` m ) = ( G ` ( B + ( E ` m ) ) ) )
41 34 40 eqtr3d 
 |-  ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> ( G ` B ) = ( G ` ( B + ( E ` m ) ) ) )
42 23 26 27 28 29 30 31 32 33 41 vdwlem1 
 |-  ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> ( K + 1 ) MonoAP G )
43 42 rexlimdvaa 
 |-  ( ph -> ( E. m e. ( 1 ... M ) ( J ` m ) = ( G ` B ) -> ( K + 1 ) MonoAP G ) )
44 22 43 biimtrid 
 |-  ( ph -> ( ( G ` B ) e. ran J -> ( K + 1 ) MonoAP G ) )
45 44 imp 
 |-  ( ( ph /\ ( G ` B ) e. ran J ) -> ( K + 1 ) MonoAP G )
46 45 olcd 
 |-  ( ( ph /\ ( G ` B ) e. ran J ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP G ) )
47 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 vdwlem5 
 |-  ( ph -> T e. NN )
48 47 adantr 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> T e. NN )
49 0nn0 
 |-  0 e. NN0
50 49 a1i 
 |-  ( ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) /\ j = ( M + 1 ) ) -> 0 e. NN0 )
51 nnuz 
 |-  NN = ( ZZ>= ` 1 )
52 6 51 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
53 52 adantr 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> M e. ( ZZ>= ` 1 ) )
54 elfzp1 
 |-  ( M e. ( ZZ>= ` 1 ) -> ( j e. ( 1 ... ( M + 1 ) ) <-> ( j e. ( 1 ... M ) \/ j = ( M + 1 ) ) ) )
55 53 54 syl 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( j e. ( 1 ... ( M + 1 ) ) <-> ( j e. ( 1 ... M ) \/ j = ( M + 1 ) ) ) )
56 55 biimpa 
 |-  ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) -> ( j e. ( 1 ... M ) \/ j = ( M + 1 ) ) )
57 56 ord 
 |-  ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) -> ( -. j e. ( 1 ... M ) -> j = ( M + 1 ) ) )
58 57 con1d 
 |-  ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) -> ( -. j = ( M + 1 ) -> j e. ( 1 ... M ) ) )
59 58 imp 
 |-  ( ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) /\ -. j = ( M + 1 ) ) -> j e. ( 1 ... M ) )
60 13 ad2antrr 
 |-  ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) -> E : ( 1 ... M ) --> NN )
61 60 ffvelcdmda 
 |-  ( ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) /\ j e. ( 1 ... M ) ) -> ( E ` j ) e. NN )
62 61 nnnn0d 
 |-  ( ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) /\ j e. ( 1 ... M ) ) -> ( E ` j ) e. NN0 )
63 59 62 syldan 
 |-  ( ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) /\ -. j = ( M + 1 ) ) -> ( E ` j ) e. NN0 )
64 50 63 ifclda 
 |-  ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) -> if ( j = ( M + 1 ) , 0 , ( E ` j ) ) e. NN0 )
65 2 10 nnmulcld 
 |-  ( ph -> ( W x. D ) e. NN )
66 65 ad2antrr 
 |-  ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) -> ( W x. D ) e. NN )
67 nn0nnaddcl 
 |-  ( ( if ( j = ( M + 1 ) , 0 , ( E ` j ) ) e. NN0 /\ ( W x. D ) e. NN ) -> ( if ( j = ( M + 1 ) , 0 , ( E ` j ) ) + ( W x. D ) ) e. NN )
68 64 66 67 syl2anc 
 |-  ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) -> ( if ( j = ( M + 1 ) , 0 , ( E ` j ) ) + ( W x. D ) ) e. NN )
69 68 18 fmptd 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> P : ( 1 ... ( M + 1 ) ) --> NN )
70 nnex 
 |-  NN e. _V
71 ovex 
 |-  ( 1 ... ( M + 1 ) ) e. _V
72 70 71 elmap 
 |-  ( P e. ( NN ^m ( 1 ... ( M + 1 ) ) ) <-> P : ( 1 ... ( M + 1 ) ) --> NN )
73 69 72 sylibr 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> P e. ( NN ^m ( 1 ... ( M + 1 ) ) ) )
74 elfzp1 
 |-  ( M e. ( ZZ>= ` 1 ) -> ( i e. ( 1 ... ( M + 1 ) ) <-> ( i e. ( 1 ... M ) \/ i = ( M + 1 ) ) ) )
75 52 74 syl 
 |-  ( ph -> ( i e. ( 1 ... ( M + 1 ) ) <-> ( i e. ( 1 ... M ) \/ i = ( M + 1 ) ) ) )
76 12 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> B e. NN )
77 76 nncnd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> B e. CC )
78 77 adantr 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> B e. CC )
79 13 ffvelcdmda 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( E ` i ) e. NN )
80 79 nncnd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( E ` i ) e. CC )
81 80 adantr 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( E ` i ) e. CC )
82 78 81 addcld 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( B + ( E ` i ) ) e. CC )
83 nnm1nn0 
 |-  ( A e. NN -> ( A - 1 ) e. NN0 )
84 9 83 syl 
 |-  ( ph -> ( A - 1 ) e. NN0 )
85 nn0nnaddcl 
 |-  ( ( ( A - 1 ) e. NN0 /\ V e. NN ) -> ( ( A - 1 ) + V ) e. NN )
86 84 1 85 syl2anc 
 |-  ( ph -> ( ( A - 1 ) + V ) e. NN )
87 2 86 nnmulcld 
 |-  ( ph -> ( W x. ( ( A - 1 ) + V ) ) e. NN )
88 87 nncnd 
 |-  ( ph -> ( W x. ( ( A - 1 ) + V ) ) e. CC )
89 88 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( W x. ( ( A - 1 ) + V ) ) e. CC )
90 elfznn0 
 |-  ( m e. ( 0 ... ( K - 1 ) ) -> m e. NN0 )
91 90 adantl 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> m e. NN0 )
92 91 nn0cnd 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> m e. CC )
93 92 adantlr 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> m e. CC )
94 93 81 mulcld 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. ( E ` i ) ) e. CC )
95 65 nnnn0d 
 |-  ( ph -> ( W x. D ) e. NN0 )
96 95 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( W x. D ) e. NN0 )
97 91 96 nn0mulcld 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. ( W x. D ) ) e. NN0 )
98 97 nn0cnd 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. ( W x. D ) ) e. CC )
99 98 adantlr 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. ( W x. D ) ) e. CC )
100 82 89 94 99 add4d 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( ( m x. ( E ` i ) ) + ( m x. ( W x. D ) ) ) ) = ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) + ( ( W x. ( ( A - 1 ) + V ) ) + ( m x. ( W x. D ) ) ) ) )
101 65 nncnd 
 |-  ( ph -> ( W x. D ) e. CC )
102 101 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( W x. D ) e. CC )
103 93 81 102 adddid 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. ( ( E ` i ) + ( W x. D ) ) ) = ( ( m x. ( E ` i ) ) + ( m x. ( W x. D ) ) ) )
104 103 oveq2d 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) = ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( ( m x. ( E ` i ) ) + ( m x. ( W x. D ) ) ) ) )
105 2 nncnd 
 |-  ( ph -> W e. CC )
106 105 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> W e. CC )
107 86 nncnd 
 |-  ( ph -> ( ( A - 1 ) + V ) e. CC )
108 107 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A - 1 ) + V ) e. CC )
109 10 nncnd 
 |-  ( ph -> D e. CC )
110 109 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> D e. CC )
111 92 110 mulcld 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. D ) e. CC )
112 106 108 111 adddid 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( W x. ( ( ( A - 1 ) + V ) + ( m x. D ) ) ) = ( ( W x. ( ( A - 1 ) + V ) ) + ( W x. ( m x. D ) ) ) )
113 9 nncnd 
 |-  ( ph -> A e. CC )
114 113 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> A e. CC )
115 1cnd 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> 1 e. CC )
116 114 111 115 addsubd 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A + ( m x. D ) ) - 1 ) = ( ( A - 1 ) + ( m x. D ) ) )
117 116 oveq1d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( A + ( m x. D ) ) - 1 ) + V ) = ( ( ( A - 1 ) + ( m x. D ) ) + V ) )
118 84 nn0cnd 
 |-  ( ph -> ( A - 1 ) e. CC )
119 118 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A - 1 ) e. CC )
120 1 nncnd 
 |-  ( ph -> V e. CC )
121 120 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> V e. CC )
122 119 111 121 add32d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( A - 1 ) + ( m x. D ) ) + V ) = ( ( ( A - 1 ) + V ) + ( m x. D ) ) )
123 117 122 eqtrd 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( A + ( m x. D ) ) - 1 ) + V ) = ( ( ( A - 1 ) + V ) + ( m x. D ) ) )
124 123 oveq2d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) = ( W x. ( ( ( A - 1 ) + V ) + ( m x. D ) ) ) )
125 92 106 110 mul12d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. ( W x. D ) ) = ( W x. ( m x. D ) ) )
126 125 oveq2d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( W x. ( ( A - 1 ) + V ) ) + ( m x. ( W x. D ) ) ) = ( ( W x. ( ( A - 1 ) + V ) ) + ( W x. ( m x. D ) ) ) )
127 112 124 126 3eqtr4d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) = ( ( W x. ( ( A - 1 ) + V ) ) + ( m x. ( W x. D ) ) ) )
128 127 adantlr 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) = ( ( W x. ( ( A - 1 ) + V ) ) + ( m x. ( W x. D ) ) ) )
129 128 oveq2d 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) = ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) + ( ( W x. ( ( A - 1 ) + V ) ) + ( m x. ( W x. D ) ) ) ) )
130 100 104 129 3eqtr4d 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) = ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) )
131 1 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> V e. NN )
132 2 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> W e. NN )
133 11 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A ( AP ` K ) D ) C_ ( `' F " { G } ) )
134 eqid 
 |-  ( A + ( m x. D ) ) = ( A + ( m x. D ) )
135 oveq1 
 |-  ( n = m -> ( n x. D ) = ( m x. D ) )
136 135 oveq2d 
 |-  ( n = m -> ( A + ( n x. D ) ) = ( A + ( m x. D ) ) )
137 136 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 ) ) )
138 134 137 mpan2 
 |-  ( m e. ( 0 ... ( K - 1 ) ) -> E. n e. ( 0 ... ( K - 1 ) ) ( A + ( m x. D ) ) = ( A + ( n x. D ) ) )
139 25 nnnn0d 
 |-  ( ph -> K e. NN0 )
140 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 ) ) ) )
141 139 9 10 140 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 ) ) ) )
142 141 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 ) )
143 138 142 sylan2 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + ( m x. D ) ) e. ( A ( AP ` K ) D ) )
144 133 143 sseldd 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + ( m x. D ) ) e. ( `' F " { G } ) )
145 1 2 3 4 5 vdwlem4 
 |-  ( ph -> F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) )
146 145 ffnd 
 |-  ( ph -> F Fn ( 1 ... V ) )
147 fniniseg 
 |-  ( F Fn ( 1 ... V ) -> ( ( A + ( m x. D ) ) e. ( `' F " { G } ) <-> ( ( A + ( m x. D ) ) e. ( 1 ... V ) /\ ( F ` ( A + ( m x. D ) ) ) = G ) ) )
148 146 147 syl 
 |-  ( ph -> ( ( A + ( m x. D ) ) e. ( `' F " { G } ) <-> ( ( A + ( m x. D ) ) e. ( 1 ... V ) /\ ( F ` ( A + ( m x. D ) ) ) = G ) ) )
149 148 biimpa 
 |-  ( ( ph /\ ( A + ( m x. D ) ) e. ( `' F " { G } ) ) -> ( ( A + ( m x. D ) ) e. ( 1 ... V ) /\ ( F ` ( A + ( m x. D ) ) ) = G ) )
150 144 149 syldan 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A + ( m x. D ) ) e. ( 1 ... V ) /\ ( F ` ( A + ( m x. D ) ) ) = G ) )
151 150 simpld 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + ( m x. D ) ) e. ( 1 ... V ) )
152 151 adantlr 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + ( m x. D ) ) e. ( 1 ... V ) )
153 14 r19.21bi 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( B + ( E ` i ) ) ( AP ` K ) ( E ` i ) ) C_ ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )
154 153 adantr 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( B + ( E ` i ) ) ( AP ` K ) ( E ` i ) ) C_ ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )
155 eqid 
 |-  ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) = ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) )
156 oveq1 
 |-  ( n = m -> ( n x. ( E ` i ) ) = ( m x. ( E ` i ) ) )
157 156 oveq2d 
 |-  ( n = m -> ( ( B + ( E ` i ) ) + ( n x. ( E ` i ) ) ) = ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) )
158 157 rspceeqv 
 |-  ( ( m e. ( 0 ... ( K - 1 ) ) /\ ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) = ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) ) -> E. n e. ( 0 ... ( K - 1 ) ) ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) = ( ( B + ( E ` i ) ) + ( n x. ( E ` i ) ) ) )
159 155 158 mpan2 
 |-  ( m e. ( 0 ... ( K - 1 ) ) -> E. n e. ( 0 ... ( K - 1 ) ) ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) = ( ( B + ( E ` i ) ) + ( n x. ( E ` i ) ) ) )
160 25 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> K e. NN )
161 160 nnnn0d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> K e. NN0 )
162 76 79 nnaddcld 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( B + ( E ` i ) ) e. NN )
163 vdwapval 
 |-  ( ( K e. NN0 /\ ( B + ( E ` i ) ) e. NN /\ ( E ` i ) e. NN ) -> ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( ( B + ( E ` i ) ) ( AP ` K ) ( E ` i ) ) <-> E. n e. ( 0 ... ( K - 1 ) ) ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) = ( ( B + ( E ` i ) ) + ( n x. ( E ` i ) ) ) ) )
164 161 162 79 163 syl3anc 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( ( B + ( E ` i ) ) ( AP ` K ) ( E ` i ) ) <-> E. n e. ( 0 ... ( K - 1 ) ) ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) = ( ( B + ( E ` i ) ) + ( n x. ( E ` i ) ) ) ) )
165 164 biimpar 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ E. n e. ( 0 ... ( K - 1 ) ) ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) = ( ( B + ( E ` i ) ) + ( n x. ( E ` i ) ) ) ) -> ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( ( B + ( E ` i ) ) ( AP ` K ) ( E ` i ) ) )
166 159 165 sylan2 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( ( B + ( E ` i ) ) ( AP ` K ) ( E ` i ) ) )
167 154 166 sseldd 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )
168 7 ffnd 
 |-  ( ph -> G Fn ( 1 ... W ) )
169 168 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> G Fn ( 1 ... W ) )
170 fniniseg 
 |-  ( G Fn ( 1 ... W ) -> ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) <-> ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( 1 ... W ) /\ ( G ` ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) ) = ( G ` ( B + ( E ` i ) ) ) ) ) )
171 169 170 syl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) <-> ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( 1 ... W ) /\ ( G ` ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) ) = ( G ` ( B + ( E ` i ) ) ) ) ) )
172 171 biimpa 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) ) -> ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( 1 ... W ) /\ ( G ` ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) ) = ( G ` ( B + ( E ` i ) ) ) ) )
173 167 172 syldan 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( 1 ... W ) /\ ( G ` ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) ) = ( G ` ( B + ( E ` i ) ) ) ) )
174 173 simpld 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( 1 ... W ) )
175 131 132 152 174 vdwlem3 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) )
176 130 175 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) )
177 fvoveq1 
 |-  ( y = ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) -> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) = ( H ` ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) )
178 eqid 
 |-  ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) )
179 fvex 
 |-  ( H ` ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) e. _V
180 177 178 179 fvmpt 
 |-  ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( 1 ... W ) -> ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) ` ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) ) = ( H ` ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) )
181 174 180 syl 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) ` ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) ) = ( H ` ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) )
182 173 simprd 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( G ` ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) ) = ( G ` ( B + ( E ` i ) ) ) )
183 150 simprd 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( F ` ( A + ( m x. D ) ) ) = G )
184 oveq1 
 |-  ( x = ( A + ( m x. D ) ) -> ( x - 1 ) = ( ( A + ( m x. D ) ) - 1 ) )
185 184 oveq1d 
 |-  ( x = ( A + ( m x. D ) ) -> ( ( x - 1 ) + V ) = ( ( ( A + ( m x. D ) ) - 1 ) + V ) )
186 185 oveq2d 
 |-  ( x = ( A + ( m x. D ) ) -> ( W x. ( ( x - 1 ) + V ) ) = ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) )
187 186 oveq2d 
 |-  ( x = ( A + ( m x. D ) ) -> ( y + ( W x. ( ( x - 1 ) + V ) ) ) = ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) )
188 187 fveq2d 
 |-  ( x = ( A + ( m x. D ) ) -> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) = ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) )
189 188 mpteq2dv 
 |-  ( x = ( A + ( m x. D ) ) -> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) )
190 ovex 
 |-  ( 1 ... W ) e. _V
191 190 mptex 
 |-  ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) e. _V
192 189 5 191 fvmpt 
 |-  ( ( A + ( m x. D ) ) e. ( 1 ... V ) -> ( F ` ( A + ( m x. D ) ) ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) )
193 151 192 syl 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( F ` ( A + ( m x. D ) ) ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) )
194 183 193 eqtr3d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> G = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) )
195 194 adantlr 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> G = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) )
196 195 fveq1d 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( G ` ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) ) = ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) ` ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) ) )
197 182 196 eqtr3d 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( G ` ( B + ( E ` i ) ) ) = ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) ` ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) ) )
198 130 fveq2d 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( H ` ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) ) = ( H ` ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) )
199 181 197 198 3eqtr4rd 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( H ` ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) ) = ( G ` ( B + ( E ` i ) ) ) )
200 176 199 jca 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) ) = ( G ` ( B + ( E ` i ) ) ) ) )
201 eleq1 
 |-  ( x = ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) -> ( x e. ( 1 ... ( W x. ( 2 x. V ) ) ) <-> ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) ) )
202 fveqeq2 
 |-  ( x = ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) -> ( ( H ` x ) = ( G ` ( B + ( E ` i ) ) ) <-> ( H ` ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) ) = ( G ` ( B + ( E ` i ) ) ) ) )
203 201 202 anbi12d 
 |-  ( x = ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) -> ( ( x e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` x ) = ( G ` ( B + ( E ` i ) ) ) ) <-> ( ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) ) = ( G ` ( B + ( E ` i ) ) ) ) ) )
204 200 203 syl5ibrcom 
 |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( x = ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) -> ( x e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` x ) = ( G ` ( B + ( E ` i ) ) ) ) ) )
205 204 rexlimdva 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( E. m e. ( 0 ... ( K - 1 ) ) x = ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) -> ( x e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` x ) = ( G ` ( B + ( E ` i ) ) ) ) ) )
206 87 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( W x. ( ( A - 1 ) + V ) ) e. NN )
207 162 206 nnaddcld 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) e. NN )
208 65 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( W x. D ) e. NN )
209 79 208 nnaddcld 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( E ` i ) + ( W x. D ) ) e. NN )
210 vdwapval 
 |-  ( ( K e. NN0 /\ ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) e. NN /\ ( ( E ` i ) + ( W x. D ) ) e. NN ) -> ( x e. ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) ( AP ` K ) ( ( E ` i ) + ( W x. D ) ) ) <-> E. m e. ( 0 ... ( K - 1 ) ) x = ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) ) )
211 161 207 209 210 syl3anc 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( x e. ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) ( AP ` K ) ( ( E ` i ) + ( W x. D ) ) ) <-> E. m e. ( 0 ... ( K - 1 ) ) x = ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) ) )
212 4 ffnd 
 |-  ( ph -> H Fn ( 1 ... ( W x. ( 2 x. V ) ) ) )
213 212 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> H Fn ( 1 ... ( W x. ( 2 x. V ) ) ) )
214 fniniseg 
 |-  ( H Fn ( 1 ... ( W x. ( 2 x. V ) ) ) -> ( x e. ( `' H " { ( G ` ( B + ( E ` i ) ) ) } ) <-> ( x e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` x ) = ( G ` ( B + ( E ` i ) ) ) ) ) )
215 213 214 syl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( x e. ( `' H " { ( G ` ( B + ( E ` i ) ) ) } ) <-> ( x e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` x ) = ( G ` ( B + ( E ` i ) ) ) ) ) )
216 205 211 215 3imtr4d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( x e. ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) ( AP ` K ) ( ( E ` i ) + ( W x. D ) ) ) -> x e. ( `' H " { ( G ` ( B + ( E ` i ) ) ) } ) ) )
217 216 ssrdv 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) ( AP ` K ) ( ( E ` i ) + ( W x. D ) ) ) C_ ( `' H " { ( G ` ( B + ( E ` i ) ) ) } ) )
218 ssun1 
 |-  ( 1 ... M ) C_ ( ( 1 ... M ) u. { ( M + 1 ) } )
219 fzsuc 
 |-  ( M e. ( ZZ>= ` 1 ) -> ( 1 ... ( M + 1 ) ) = ( ( 1 ... M ) u. { ( M + 1 ) } ) )
220 52 219 syl 
 |-  ( ph -> ( 1 ... ( M + 1 ) ) = ( ( 1 ... M ) u. { ( M + 1 ) } ) )
221 218 220 sseqtrrid 
 |-  ( ph -> ( 1 ... M ) C_ ( 1 ... ( M + 1 ) ) )
222 221 sselda 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> i e. ( 1 ... ( M + 1 ) ) )
223 eqeq1 
 |-  ( j = i -> ( j = ( M + 1 ) <-> i = ( M + 1 ) ) )
224 fveq2 
 |-  ( j = i -> ( E ` j ) = ( E ` i ) )
225 223 224 ifbieq2d 
 |-  ( j = i -> if ( j = ( M + 1 ) , 0 , ( E ` j ) ) = if ( i = ( M + 1 ) , 0 , ( E ` i ) ) )
226 225 oveq1d 
 |-  ( j = i -> ( if ( j = ( M + 1 ) , 0 , ( E ` j ) ) + ( W x. D ) ) = ( if ( i = ( M + 1 ) , 0 , ( E ` i ) ) + ( W x. D ) ) )
227 ovex 
 |-  ( if ( i = ( M + 1 ) , 0 , ( E ` i ) ) + ( W x. D ) ) e. _V
228 226 18 227 fvmpt 
 |-  ( i e. ( 1 ... ( M + 1 ) ) -> ( P ` i ) = ( if ( i = ( M + 1 ) , 0 , ( E ` i ) ) + ( W x. D ) ) )
229 222 228 syl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( P ` i ) = ( if ( i = ( M + 1 ) , 0 , ( E ` i ) ) + ( W x. D ) ) )
230 6 nnred 
 |-  ( ph -> M e. RR )
231 230 ltp1d 
 |-  ( ph -> M < ( M + 1 ) )
232 peano2re 
 |-  ( M e. RR -> ( M + 1 ) e. RR )
233 230 232 syl 
 |-  ( ph -> ( M + 1 ) e. RR )
234 230 233 ltnled 
 |-  ( ph -> ( M < ( M + 1 ) <-> -. ( M + 1 ) <_ M ) )
235 231 234 mpbid 
 |-  ( ph -> -. ( M + 1 ) <_ M )
236 breq1 
 |-  ( i = ( M + 1 ) -> ( i <_ M <-> ( M + 1 ) <_ M ) )
237 236 notbid 
 |-  ( i = ( M + 1 ) -> ( -. i <_ M <-> -. ( M + 1 ) <_ M ) )
238 235 237 syl5ibrcom 
 |-  ( ph -> ( i = ( M + 1 ) -> -. i <_ M ) )
239 238 con2d 
 |-  ( ph -> ( i <_ M -> -. i = ( M + 1 ) ) )
240 elfzle2 
 |-  ( i e. ( 1 ... M ) -> i <_ M )
241 239 240 impel 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> -. i = ( M + 1 ) )
242 iffalse 
 |-  ( -. i = ( M + 1 ) -> if ( i = ( M + 1 ) , 0 , ( E ` i ) ) = ( E ` i ) )
243 242 oveq1d 
 |-  ( -. i = ( M + 1 ) -> ( if ( i = ( M + 1 ) , 0 , ( E ` i ) ) + ( W x. D ) ) = ( ( E ` i ) + ( W x. D ) ) )
244 241 243 syl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( if ( i = ( M + 1 ) , 0 , ( E ` i ) ) + ( W x. D ) ) = ( ( E ` i ) + ( W x. D ) ) )
245 229 244 eqtrd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( P ` i ) = ( ( E ` i ) + ( W x. D ) ) )
246 245 oveq2d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( T + ( P ` i ) ) = ( T + ( ( E ` i ) + ( W x. D ) ) ) )
247 47 nncnd 
 |-  ( ph -> T e. CC )
248 247 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> T e. CC )
249 101 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( W x. D ) e. CC )
250 248 80 249 add12d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( T + ( ( E ` i ) + ( W x. D ) ) ) = ( ( E ` i ) + ( T + ( W x. D ) ) ) )
251 17 oveq1i 
 |-  ( T + ( W x. D ) ) = ( ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) ) + ( W x. D ) )
252 12 nncnd 
 |-  ( ph -> B e. CC )
253 120 109 subcld 
 |-  ( ph -> ( V - D ) e. CC )
254 113 253 addcld 
 |-  ( ph -> ( A + ( V - D ) ) e. CC )
255 ax-1cn 
 |-  1 e. CC
256 subcl 
 |-  ( ( ( A + ( V - D ) ) e. CC /\ 1 e. CC ) -> ( ( A + ( V - D ) ) - 1 ) e. CC )
257 254 255 256 sylancl 
 |-  ( ph -> ( ( A + ( V - D ) ) - 1 ) e. CC )
258 105 257 mulcld 
 |-  ( ph -> ( W x. ( ( A + ( V - D ) ) - 1 ) ) e. CC )
259 252 258 101 addassd 
 |-  ( ph -> ( ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) ) + ( W x. D ) ) = ( B + ( ( W x. ( ( A + ( V - D ) ) - 1 ) ) + ( W x. D ) ) ) )
260 105 257 109 adddid 
 |-  ( ph -> ( W x. ( ( ( A + ( V - D ) ) - 1 ) + D ) ) = ( ( W x. ( ( A + ( V - D ) ) - 1 ) ) + ( W x. D ) ) )
261 113 253 109 addassd 
 |-  ( ph -> ( ( A + ( V - D ) ) + D ) = ( A + ( ( V - D ) + D ) ) )
262 120 109 npcand 
 |-  ( ph -> ( ( V - D ) + D ) = V )
263 262 oveq2d 
 |-  ( ph -> ( A + ( ( V - D ) + D ) ) = ( A + V ) )
264 261 263 eqtrd 
 |-  ( ph -> ( ( A + ( V - D ) ) + D ) = ( A + V ) )
265 264 oveq1d 
 |-  ( ph -> ( ( ( A + ( V - D ) ) + D ) - 1 ) = ( ( A + V ) - 1 ) )
266 1cnd 
 |-  ( ph -> 1 e. CC )
267 254 109 266 addsubd 
 |-  ( ph -> ( ( ( A + ( V - D ) ) + D ) - 1 ) = ( ( ( A + ( V - D ) ) - 1 ) + D ) )
268 113 120 266 addsubd 
 |-  ( ph -> ( ( A + V ) - 1 ) = ( ( A - 1 ) + V ) )
269 265 267 268 3eqtr3d 
 |-  ( ph -> ( ( ( A + ( V - D ) ) - 1 ) + D ) = ( ( A - 1 ) + V ) )
270 269 oveq2d 
 |-  ( ph -> ( W x. ( ( ( A + ( V - D ) ) - 1 ) + D ) ) = ( W x. ( ( A - 1 ) + V ) ) )
271 260 270 eqtr3d 
 |-  ( ph -> ( ( W x. ( ( A + ( V - D ) ) - 1 ) ) + ( W x. D ) ) = ( W x. ( ( A - 1 ) + V ) ) )
272 271 oveq2d 
 |-  ( ph -> ( B + ( ( W x. ( ( A + ( V - D ) ) - 1 ) ) + ( W x. D ) ) ) = ( B + ( W x. ( ( A - 1 ) + V ) ) ) )
273 259 272 eqtrd 
 |-  ( ph -> ( ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) ) + ( W x. D ) ) = ( B + ( W x. ( ( A - 1 ) + V ) ) ) )
274 251 273 eqtrid 
 |-  ( ph -> ( T + ( W x. D ) ) = ( B + ( W x. ( ( A - 1 ) + V ) ) ) )
275 274 oveq2d 
 |-  ( ph -> ( ( E ` i ) + ( T + ( W x. D ) ) ) = ( ( E ` i ) + ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) )
276 275 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( E ` i ) + ( T + ( W x. D ) ) ) = ( ( E ` i ) + ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) )
277 88 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( W x. ( ( A - 1 ) + V ) ) e. CC )
278 80 77 277 addassd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( ( E ` i ) + B ) + ( W x. ( ( A - 1 ) + V ) ) ) = ( ( E ` i ) + ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) )
279 80 77 addcomd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( E ` i ) + B ) = ( B + ( E ` i ) ) )
280 279 oveq1d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( ( E ` i ) + B ) + ( W x. ( ( A - 1 ) + V ) ) ) = ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) )
281 276 278 280 3eqtr2d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( E ` i ) + ( T + ( W x. D ) ) ) = ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) )
282 246 250 281 3eqtrd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( T + ( P ` i ) ) = ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) )
283 282 245 oveq12d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) = ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) ( AP ` K ) ( ( E ` i ) + ( W x. D ) ) ) )
284 cnvimass 
 |-  ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) C_ dom G
285 284 7 fssdm 
 |-  ( ph -> ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) C_ ( 1 ... W ) )
286 285 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) C_ ( 1 ... W ) )
287 vdwapid1 
 |-  ( ( K e. NN /\ ( B + ( E ` i ) ) e. NN /\ ( E ` i ) e. NN ) -> ( B + ( E ` i ) ) e. ( ( B + ( E ` i ) ) ( AP ` K ) ( E ` i ) ) )
288 160 162 79 287 syl3anc 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( B + ( E ` i ) ) e. ( ( B + ( E ` i ) ) ( AP ` K ) ( E ` i ) ) )
289 153 288 sseldd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( B + ( E ` i ) ) e. ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )
290 286 289 sseldd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( B + ( E ` i ) ) e. ( 1 ... W ) )
291 fvoveq1 
 |-  ( y = ( B + ( E ` i ) ) -> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) = ( H ` ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) ) )
292 eqid 
 |-  ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) )
293 fvex 
 |-  ( H ` ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) ) e. _V
294 291 292 293 fvmpt 
 |-  ( ( B + ( E ` i ) ) e. ( 1 ... W ) -> ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) ` ( B + ( E ` i ) ) ) = ( H ` ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) ) )
295 290 294 syl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) ` ( B + ( E ` i ) ) ) = ( H ` ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) ) )
296 vdwapid1 
 |-  ( ( K e. NN /\ A e. NN /\ D e. NN ) -> A e. ( A ( AP ` K ) D ) )
297 25 9 10 296 syl3anc 
 |-  ( ph -> A e. ( A ( AP ` K ) D ) )
298 11 297 sseldd 
 |-  ( ph -> A e. ( `' F " { G } ) )
299 fniniseg 
 |-  ( F Fn ( 1 ... V ) -> ( A e. ( `' F " { G } ) <-> ( A e. ( 1 ... V ) /\ ( F ` A ) = G ) ) )
300 146 299 syl 
 |-  ( ph -> ( A e. ( `' F " { G } ) <-> ( A e. ( 1 ... V ) /\ ( F ` A ) = G ) ) )
301 298 300 mpbid 
 |-  ( ph -> ( A e. ( 1 ... V ) /\ ( F ` A ) = G ) )
302 301 simprd 
 |-  ( ph -> ( F ` A ) = G )
303 301 simpld 
 |-  ( ph -> A e. ( 1 ... V ) )
304 oveq1 
 |-  ( x = A -> ( x - 1 ) = ( A - 1 ) )
305 304 oveq1d 
 |-  ( x = A -> ( ( x - 1 ) + V ) = ( ( A - 1 ) + V ) )
306 305 oveq2d 
 |-  ( x = A -> ( W x. ( ( x - 1 ) + V ) ) = ( W x. ( ( A - 1 ) + V ) ) )
307 306 oveq2d 
 |-  ( x = A -> ( y + ( W x. ( ( x - 1 ) + V ) ) ) = ( y + ( W x. ( ( A - 1 ) + V ) ) ) )
308 307 fveq2d 
 |-  ( x = A -> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) = ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) )
309 308 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 ) ) ) ) ) )
310 190 mptex 
 |-  ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) e. _V
311 309 5 310 fvmpt 
 |-  ( A e. ( 1 ... V ) -> ( F ` A ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) )
312 303 311 syl 
 |-  ( ph -> ( F ` A ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) )
313 302 312 eqtr3d 
 |-  ( ph -> G = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) )
314 313 fveq1d 
 |-  ( ph -> ( G ` ( B + ( E ` i ) ) ) = ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) ` ( B + ( E ` i ) ) ) )
315 314 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( G ` ( B + ( E ` i ) ) ) = ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) ` ( B + ( E ` i ) ) ) )
316 282 fveq2d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( H ` ( T + ( P ` i ) ) ) = ( H ` ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) ) )
317 295 315 316 3eqtr4rd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( H ` ( T + ( P ` i ) ) ) = ( G ` ( B + ( E ` i ) ) ) )
318 317 sneqd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> { ( H ` ( T + ( P ` i ) ) ) } = { ( G ` ( B + ( E ` i ) ) ) } )
319 318 imaeq2d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) = ( `' H " { ( G ` ( B + ( E ` i ) ) ) } ) )
320 217 283 319 3sstr4d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) )
321 320 ex 
 |-  ( ph -> ( i e. ( 1 ... M ) -> ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) ) )
322 252 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> B e. CC )
323 88 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( W x. ( ( A - 1 ) + V ) ) e. CC )
324 322 323 98 addassd 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) = ( B + ( ( W x. ( ( A - 1 ) + V ) ) + ( m x. ( W x. D ) ) ) ) )
325 127 oveq2d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( B + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) = ( B + ( ( W x. ( ( A - 1 ) + V ) ) + ( m x. ( W x. D ) ) ) ) )
326 324 325 eqtr4d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) = ( B + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) )
327 1 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> V e. NN )
328 2 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> W e. NN )
329 eluzfz1 
 |-  ( M e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... M ) )
330 52 329 syl 
 |-  ( ph -> 1 e. ( 1 ... M ) )
331 330 ne0d 
 |-  ( ph -> ( 1 ... M ) =/= (/) )
332 elfzuz3 
 |-  ( ( B + ( E ` i ) ) e. ( 1 ... W ) -> W e. ( ZZ>= ` ( B + ( E ` i ) ) ) )
333 290 332 syl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> W e. ( ZZ>= ` ( B + ( E ` i ) ) ) )
334 12 nnzd 
 |-  ( ph -> B e. ZZ )
335 uzid 
 |-  ( B e. ZZ -> B e. ( ZZ>= ` B ) )
336 334 335 syl 
 |-  ( ph -> B e. ( ZZ>= ` B ) )
337 336 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> B e. ( ZZ>= ` B ) )
338 79 nnnn0d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( E ` i ) e. NN0 )
339 uzaddcl 
 |-  ( ( B e. ( ZZ>= ` B ) /\ ( E ` i ) e. NN0 ) -> ( B + ( E ` i ) ) e. ( ZZ>= ` B ) )
340 337 338 339 syl2anc 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( B + ( E ` i ) ) e. ( ZZ>= ` B ) )
341 uztrn 
 |-  ( ( W e. ( ZZ>= ` ( B + ( E ` i ) ) ) /\ ( B + ( E ` i ) ) e. ( ZZ>= ` B ) ) -> W e. ( ZZ>= ` B ) )
342 333 340 341 syl2anc 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> W e. ( ZZ>= ` B ) )
343 eluzle 
 |-  ( W e. ( ZZ>= ` B ) -> B <_ W )
344 342 343 syl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> B <_ W )
345 344 ralrimiva 
 |-  ( ph -> A. i e. ( 1 ... M ) B <_ W )
346 r19.2z 
 |-  ( ( ( 1 ... M ) =/= (/) /\ A. i e. ( 1 ... M ) B <_ W ) -> E. i e. ( 1 ... M ) B <_ W )
347 331 345 346 syl2anc 
 |-  ( ph -> E. i e. ( 1 ... M ) B <_ W )
348 idd 
 |-  ( i e. ( 1 ... M ) -> ( B <_ W -> B <_ W ) )
349 348 rexlimiv 
 |-  ( E. i e. ( 1 ... M ) B <_ W -> B <_ W )
350 347 349 syl 
 |-  ( ph -> B <_ W )
351 2 nnzd 
 |-  ( ph -> W e. ZZ )
352 fznn 
 |-  ( W e. ZZ -> ( B e. ( 1 ... W ) <-> ( B e. NN /\ B <_ W ) ) )
353 351 352 syl 
 |-  ( ph -> ( B e. ( 1 ... W ) <-> ( B e. NN /\ B <_ W ) ) )
354 12 350 353 mpbir2and 
 |-  ( ph -> B e. ( 1 ... W ) )
355 354 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> B e. ( 1 ... W ) )
356 327 328 151 355 vdwlem3 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( B + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) )
357 326 356 eqeltrd 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) )
358 fvoveq1 
 |-  ( y = B -> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) = ( H ` ( B + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) )
359 fvex 
 |-  ( H ` ( B + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) e. _V
360 358 178 359 fvmpt 
 |-  ( B e. ( 1 ... W ) -> ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) ` B ) = ( H ` ( B + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) )
361 355 360 syl 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) ` B ) = ( H ` ( B + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) )
362 194 fveq1d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( G ` B ) = ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) ` B ) )
363 326 fveq2d 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( H ` ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) ) = ( H ` ( B + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) )
364 361 362 363 3eqtr4rd 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( H ` ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) ) = ( G ` B ) )
365 357 364 jca 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) ) = ( G ` B ) ) )
366 eleq1 
 |-  ( z = ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) -> ( z e. ( 1 ... ( W x. ( 2 x. V ) ) ) <-> ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) ) )
367 fveqeq2 
 |-  ( z = ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) -> ( ( H ` z ) = ( G ` B ) <-> ( H ` ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) ) = ( G ` B ) ) )
368 366 367 anbi12d 
 |-  ( z = ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) -> ( ( z e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` z ) = ( G ` B ) ) <-> ( ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) ) = ( G ` B ) ) ) )
369 365 368 syl5ibrcom 
 |-  ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( z = ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) -> ( z e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` z ) = ( G ` B ) ) ) )
370 369 rexlimdva 
 |-  ( ph -> ( E. m e. ( 0 ... ( K - 1 ) ) z = ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) -> ( z e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` z ) = ( G ` B ) ) ) )
371 12 87 nnaddcld 
 |-  ( ph -> ( B + ( W x. ( ( A - 1 ) + V ) ) ) e. NN )
372 vdwapval 
 |-  ( ( K e. NN0 /\ ( B + ( W x. ( ( A - 1 ) + V ) ) ) e. NN /\ ( W x. D ) e. NN ) -> ( z e. ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) ( AP ` K ) ( W x. D ) ) <-> E. m e. ( 0 ... ( K - 1 ) ) z = ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) ) )
373 139 371 65 372 syl3anc 
 |-  ( ph -> ( z e. ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) ( AP ` K ) ( W x. D ) ) <-> E. m e. ( 0 ... ( K - 1 ) ) z = ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) ) )
374 fniniseg 
 |-  ( H Fn ( 1 ... ( W x. ( 2 x. V ) ) ) -> ( z e. ( `' H " { ( G ` B ) } ) <-> ( z e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` z ) = ( G ` B ) ) ) )
375 212 374 syl 
 |-  ( ph -> ( z e. ( `' H " { ( G ` B ) } ) <-> ( z e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` z ) = ( G ` B ) ) ) )
376 370 373 375 3imtr4d 
 |-  ( ph -> ( z e. ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) ( AP ` K ) ( W x. D ) ) -> z e. ( `' H " { ( G ` B ) } ) ) )
377 376 ssrdv 
 |-  ( ph -> ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) ( AP ` K ) ( W x. D ) ) C_ ( `' H " { ( G ` B ) } ) )
378 6 peano2nnd 
 |-  ( ph -> ( M + 1 ) e. NN )
379 378 51 eleqtrdi 
 |-  ( ph -> ( M + 1 ) e. ( ZZ>= ` 1 ) )
380 eluzfz2 
 |-  ( ( M + 1 ) e. ( ZZ>= ` 1 ) -> ( M + 1 ) e. ( 1 ... ( M + 1 ) ) )
381 iftrue 
 |-  ( j = ( M + 1 ) -> if ( j = ( M + 1 ) , 0 , ( E ` j ) ) = 0 )
382 381 oveq1d 
 |-  ( j = ( M + 1 ) -> ( if ( j = ( M + 1 ) , 0 , ( E ` j ) ) + ( W x. D ) ) = ( 0 + ( W x. D ) ) )
383 ovex 
 |-  ( 0 + ( W x. D ) ) e. _V
384 382 18 383 fvmpt 
 |-  ( ( M + 1 ) e. ( 1 ... ( M + 1 ) ) -> ( P ` ( M + 1 ) ) = ( 0 + ( W x. D ) ) )
385 379 380 384 3syl 
 |-  ( ph -> ( P ` ( M + 1 ) ) = ( 0 + ( W x. D ) ) )
386 101 addlidd 
 |-  ( ph -> ( 0 + ( W x. D ) ) = ( W x. D ) )
387 385 386 eqtrd 
 |-  ( ph -> ( P ` ( M + 1 ) ) = ( W x. D ) )
388 387 oveq2d 
 |-  ( ph -> ( T + ( P ` ( M + 1 ) ) ) = ( T + ( W x. D ) ) )
389 388 274 eqtrd 
 |-  ( ph -> ( T + ( P ` ( M + 1 ) ) ) = ( B + ( W x. ( ( A - 1 ) + V ) ) ) )
390 389 387 oveq12d 
 |-  ( ph -> ( ( T + ( P ` ( M + 1 ) ) ) ( AP ` K ) ( P ` ( M + 1 ) ) ) = ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) ( AP ` K ) ( W x. D ) ) )
391 fvoveq1 
 |-  ( y = B -> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) = ( H ` ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) )
392 fvex 
 |-  ( H ` ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) e. _V
393 391 292 392 fvmpt 
 |-  ( B e. ( 1 ... W ) -> ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) ` B ) = ( H ` ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) )
394 354 393 syl 
 |-  ( ph -> ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) ` B ) = ( H ` ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) )
395 313 fveq1d 
 |-  ( ph -> ( G ` B ) = ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) ` B ) )
396 389 fveq2d 
 |-  ( ph -> ( H ` ( T + ( P ` ( M + 1 ) ) ) ) = ( H ` ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) )
397 394 395 396 3eqtr4rd 
 |-  ( ph -> ( H ` ( T + ( P ` ( M + 1 ) ) ) ) = ( G ` B ) )
398 397 sneqd 
 |-  ( ph -> { ( H ` ( T + ( P ` ( M + 1 ) ) ) ) } = { ( G ` B ) } )
399 398 imaeq2d 
 |-  ( ph -> ( `' H " { ( H ` ( T + ( P ` ( M + 1 ) ) ) ) } ) = ( `' H " { ( G ` B ) } ) )
400 377 390 399 3sstr4d 
 |-  ( ph -> ( ( T + ( P ` ( M + 1 ) ) ) ( AP ` K ) ( P ` ( M + 1 ) ) ) C_ ( `' H " { ( H ` ( T + ( P ` ( M + 1 ) ) ) ) } ) )
401 fveq2 
 |-  ( i = ( M + 1 ) -> ( P ` i ) = ( P ` ( M + 1 ) ) )
402 401 oveq2d 
 |-  ( i = ( M + 1 ) -> ( T + ( P ` i ) ) = ( T + ( P ` ( M + 1 ) ) ) )
403 402 401 oveq12d 
 |-  ( i = ( M + 1 ) -> ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) = ( ( T + ( P ` ( M + 1 ) ) ) ( AP ` K ) ( P ` ( M + 1 ) ) ) )
404 402 fveq2d 
 |-  ( i = ( M + 1 ) -> ( H ` ( T + ( P ` i ) ) ) = ( H ` ( T + ( P ` ( M + 1 ) ) ) ) )
405 404 sneqd 
 |-  ( i = ( M + 1 ) -> { ( H ` ( T + ( P ` i ) ) ) } = { ( H ` ( T + ( P ` ( M + 1 ) ) ) ) } )
406 405 imaeq2d 
 |-  ( i = ( M + 1 ) -> ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) = ( `' H " { ( H ` ( T + ( P ` ( M + 1 ) ) ) ) } ) )
407 403 406 sseq12d 
 |-  ( i = ( M + 1 ) -> ( ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) <-> ( ( T + ( P ` ( M + 1 ) ) ) ( AP ` K ) ( P ` ( M + 1 ) ) ) C_ ( `' H " { ( H ` ( T + ( P ` ( M + 1 ) ) ) ) } ) ) )
408 400 407 syl5ibrcom 
 |-  ( ph -> ( i = ( M + 1 ) -> ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) ) )
409 321 408 jaod 
 |-  ( ph -> ( ( i e. ( 1 ... M ) \/ i = ( M + 1 ) ) -> ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) ) )
410 75 409 sylbid 
 |-  ( ph -> ( i e. ( 1 ... ( M + 1 ) ) -> ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) ) )
411 410 ralrimiv 
 |-  ( ph -> A. i e. ( 1 ... ( M + 1 ) ) ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) )
412 411 adantr 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> A. i e. ( 1 ... ( M + 1 ) ) ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) )
413 220 rexeqdv 
 |-  ( ph -> ( E. i e. ( 1 ... ( M + 1 ) ) x = ( H ` ( T + ( P ` i ) ) ) <-> E. i e. ( ( 1 ... M ) u. { ( M + 1 ) } ) x = ( H ` ( T + ( P ` i ) ) ) ) )
414 rexun 
 |-  ( E. i e. ( ( 1 ... M ) u. { ( M + 1 ) } ) x = ( H ` ( T + ( P ` i ) ) ) <-> ( E. i e. ( 1 ... M ) x = ( H ` ( T + ( P ` i ) ) ) \/ E. i e. { ( M + 1 ) } x = ( H ` ( T + ( P ` i ) ) ) ) )
415 317 eqeq2d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( x = ( H ` ( T + ( P ` i ) ) ) <-> x = ( G ` ( B + ( E ` i ) ) ) ) )
416 415 rexbidva 
 |-  ( ph -> ( E. i e. ( 1 ... M ) x = ( H ` ( T + ( P ` i ) ) ) <-> E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) ) )
417 ovex 
 |-  ( M + 1 ) e. _V
418 404 eqeq2d 
 |-  ( i = ( M + 1 ) -> ( x = ( H ` ( T + ( P ` i ) ) ) <-> x = ( H ` ( T + ( P ` ( M + 1 ) ) ) ) ) )
419 417 418 rexsn 
 |-  ( E. i e. { ( M + 1 ) } x = ( H ` ( T + ( P ` i ) ) ) <-> x = ( H ` ( T + ( P ` ( M + 1 ) ) ) ) )
420 397 eqeq2d 
 |-  ( ph -> ( x = ( H ` ( T + ( P ` ( M + 1 ) ) ) ) <-> x = ( G ` B ) ) )
421 419 420 bitrid 
 |-  ( ph -> ( E. i e. { ( M + 1 ) } x = ( H ` ( T + ( P ` i ) ) ) <-> x = ( G ` B ) ) )
422 416 421 orbi12d 
 |-  ( ph -> ( ( E. i e. ( 1 ... M ) x = ( H ` ( T + ( P ` i ) ) ) \/ E. i e. { ( M + 1 ) } x = ( H ` ( T + ( P ` i ) ) ) ) <-> ( E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) \/ x = ( G ` B ) ) ) )
423 414 422 bitrid 
 |-  ( ph -> ( E. i e. ( ( 1 ... M ) u. { ( M + 1 ) } ) x = ( H ` ( T + ( P ` i ) ) ) <-> ( E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) \/ x = ( G ` B ) ) ) )
424 413 423 bitrd 
 |-  ( ph -> ( E. i e. ( 1 ... ( M + 1 ) ) x = ( H ` ( T + ( P ` i ) ) ) <-> ( E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) \/ x = ( G ` B ) ) ) )
425 424 adantr 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( E. i e. ( 1 ... ( M + 1 ) ) x = ( H ` ( T + ( P ` i ) ) ) <-> ( E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) \/ x = ( G ` B ) ) ) )
426 425 abbidv 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> { x | E. i e. ( 1 ... ( M + 1 ) ) x = ( H ` ( T + ( P ` i ) ) ) } = { x | ( E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) \/ x = ( G ` B ) ) } )
427 eqid 
 |-  ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) = ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) )
428 427 rnmpt 
 |-  ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) = { x | E. i e. ( 1 ... ( M + 1 ) ) x = ( H ` ( T + ( P ` i ) ) ) }
429 15 rnmpt 
 |-  ran J = { x | E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) }
430 df-sn 
 |-  { ( G ` B ) } = { x | x = ( G ` B ) }
431 429 430 uneq12i 
 |-  ( ran J u. { ( G ` B ) } ) = ( { x | E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) } u. { x | x = ( G ` B ) } )
432 unab 
 |-  ( { x | E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) } u. { x | x = ( G ` B ) } ) = { x | ( E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) \/ x = ( G ` B ) ) }
433 431 432 eqtri 
 |-  ( ran J u. { ( G ` B ) } ) = { x | ( E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) \/ x = ( G ` B ) ) }
434 426 428 433 3eqtr4g 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) = ( ran J u. { ( G ` B ) } ) )
435 434 fveq2d 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) ) = ( # ` ( ran J u. { ( G ` B ) } ) ) )
436 fzfi 
 |-  ( 1 ... M ) e. Fin
437 dffn4 
 |-  ( J Fn ( 1 ... M ) <-> J : ( 1 ... M ) -onto-> ran J )
438 20 437 mpbi 
 |-  J : ( 1 ... M ) -onto-> ran J
439 fofi 
 |-  ( ( ( 1 ... M ) e. Fin /\ J : ( 1 ... M ) -onto-> ran J ) -> ran J e. Fin )
440 436 438 439 mp2an 
 |-  ran J e. Fin
441 440 a1i 
 |-  ( ph -> ran J e. Fin )
442 fvex 
 |-  ( G ` B ) e. _V
443 hashunsng 
 |-  ( ( G ` B ) e. _V -> ( ( ran J e. Fin /\ -. ( G ` B ) e. ran J ) -> ( # ` ( ran J u. { ( G ` B ) } ) ) = ( ( # ` ran J ) + 1 ) ) )
444 442 443 ax-mp 
 |-  ( ( ran J e. Fin /\ -. ( G ` B ) e. ran J ) -> ( # ` ( ran J u. { ( G ` B ) } ) ) = ( ( # ` ran J ) + 1 ) )
445 441 444 sylan 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( # ` ( ran J u. { ( G ` B ) } ) ) = ( ( # ` ran J ) + 1 ) )
446 16 adantr 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( # ` ran J ) = M )
447 446 oveq1d 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( ( # ` ran J ) + 1 ) = ( M + 1 ) )
448 435 445 447 3eqtrd 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) ) = ( M + 1 ) )
449 412 448 jca 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( A. i e. ( 1 ... ( M + 1 ) ) ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) ) = ( M + 1 ) ) )
450 oveq1 
 |-  ( a = T -> ( a + ( d ` i ) ) = ( T + ( d ` i ) ) )
451 450 oveq1d 
 |-  ( a = T -> ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) = ( ( T + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) )
452 fvoveq1 
 |-  ( a = T -> ( H ` ( a + ( d ` i ) ) ) = ( H ` ( T + ( d ` i ) ) ) )
453 452 sneqd 
 |-  ( a = T -> { ( H ` ( a + ( d ` i ) ) ) } = { ( H ` ( T + ( d ` i ) ) ) } )
454 453 imaeq2d 
 |-  ( a = T -> ( `' H " { ( H ` ( a + ( d ` i ) ) ) } ) = ( `' H " { ( H ` ( T + ( d ` i ) ) ) } ) )
455 451 454 sseq12d 
 |-  ( a = T -> ( ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' H " { ( H ` ( a + ( d ` i ) ) ) } ) <-> ( ( T + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' H " { ( H ` ( T + ( d ` i ) ) ) } ) ) )
456 455 ralbidv 
 |-  ( a = T -> ( A. i e. ( 1 ... ( M + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' H " { ( H ` ( a + ( d ` i ) ) ) } ) <-> A. i e. ( 1 ... ( M + 1 ) ) ( ( T + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' H " { ( H ` ( T + ( d ` i ) ) ) } ) ) )
457 452 mpteq2dv 
 |-  ( a = T -> ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( a + ( d ` i ) ) ) ) = ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( d ` i ) ) ) ) )
458 457 rneqd 
 |-  ( a = T -> ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( a + ( d ` i ) ) ) ) = ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( d ` i ) ) ) ) )
459 458 fveqeq2d 
 |-  ( a = T -> ( ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( a + ( d ` i ) ) ) ) ) = ( M + 1 ) <-> ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( d ` i ) ) ) ) ) = ( M + 1 ) ) )
460 456 459 anbi12d 
 |-  ( a = T -> ( ( A. i e. ( 1 ... ( M + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' H " { ( H ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( a + ( d ` i ) ) ) ) ) = ( M + 1 ) ) <-> ( A. i e. ( 1 ... ( M + 1 ) ) ( ( T + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' H " { ( H ` ( T + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( d ` i ) ) ) ) ) = ( M + 1 ) ) ) )
461 fveq1 
 |-  ( d = P -> ( d ` i ) = ( P ` i ) )
462 461 oveq2d 
 |-  ( d = P -> ( T + ( d ` i ) ) = ( T + ( P ` i ) ) )
463 462 461 oveq12d 
 |-  ( d = P -> ( ( T + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) = ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) )
464 462 fveq2d 
 |-  ( d = P -> ( H ` ( T + ( d ` i ) ) ) = ( H ` ( T + ( P ` i ) ) ) )
465 464 sneqd 
 |-  ( d = P -> { ( H ` ( T + ( d ` i ) ) ) } = { ( H ` ( T + ( P ` i ) ) ) } )
466 465 imaeq2d 
 |-  ( d = P -> ( `' H " { ( H ` ( T + ( d ` i ) ) ) } ) = ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) )
467 463 466 sseq12d 
 |-  ( d = P -> ( ( ( T + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' H " { ( H ` ( T + ( d ` i ) ) ) } ) <-> ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) ) )
468 467 ralbidv 
 |-  ( d = P -> ( A. i e. ( 1 ... ( M + 1 ) ) ( ( T + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' H " { ( H ` ( T + ( d ` i ) ) ) } ) <-> A. i e. ( 1 ... ( M + 1 ) ) ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) ) )
469 464 mpteq2dv 
 |-  ( d = P -> ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( d ` i ) ) ) ) = ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) )
470 469 rneqd 
 |-  ( d = P -> ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( d ` i ) ) ) ) = ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) )
471 470 fveqeq2d 
 |-  ( d = P -> ( ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( d ` i ) ) ) ) ) = ( M + 1 ) <-> ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) ) = ( M + 1 ) ) )
472 468 471 anbi12d 
 |-  ( d = P -> ( ( A. i e. ( 1 ... ( M + 1 ) ) ( ( T + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' H " { ( H ` ( T + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( d ` i ) ) ) ) ) = ( M + 1 ) ) <-> ( A. i e. ( 1 ... ( M + 1 ) ) ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) ) = ( M + 1 ) ) ) )
473 460 472 rspc2ev 
 |-  ( ( T e. NN /\ P e. ( NN ^m ( 1 ... ( M + 1 ) ) ) /\ ( A. i e. ( 1 ... ( M + 1 ) ) ( ( T + ( P ` i ) ) ( AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) ) = ( M + 1 ) ) ) -> E. a e. NN E. d e. ( NN ^m ( 1 ... ( M + 1 ) ) ) ( A. i e. ( 1 ... ( M + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' H " { ( H ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( a + ( d ` i ) ) ) ) ) = ( M + 1 ) ) )
474 48 73 449 473 syl3anc 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> E. a e. NN E. d e. ( NN ^m ( 1 ... ( M + 1 ) ) ) ( A. i e. ( 1 ... ( M + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' H " { ( H ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( a + ( d ` i ) ) ) ) ) = ( M + 1 ) ) )
475 ovex 
 |-  ( 1 ... ( W x. ( 2 x. V ) ) ) e. _V
476 25 adantr 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> K e. NN )
477 476 nnnn0d 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> K e. NN0 )
478 4 adantr 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )
479 6 adantr 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> M e. NN )
480 479 peano2nnd 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( M + 1 ) e. NN )
481 eqid 
 |-  ( 1 ... ( M + 1 ) ) = ( 1 ... ( M + 1 ) )
482 475 477 478 480 481 vdwpc 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( <. ( M + 1 ) , K >. PolyAP H <-> E. a e. NN E. d e. ( NN ^m ( 1 ... ( M + 1 ) ) ) ( A. i e. ( 1 ... ( M + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' H " { ( H ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( a + ( d ` i ) ) ) ) ) = ( M + 1 ) ) ) )
483 474 482 mpbird 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> <. ( M + 1 ) , K >. PolyAP H )
484 483 orcd 
 |-  ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP G ) )
485 46 484 pm2.61dan 
 |-  ( ph -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP G ) )