Theorem vdwlem6 15690

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

Hypotheses

Ref	Expression
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

Ref	Expression
vdwlem6	|- ( ph -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP G ) )

Distinct variable groups:   x, y, A   i, j, x, y, G   i, K, j, x, y   i, J, j, x   P, i, x   ph, i, j, x, y   R, i, x, y   B, i, j, x, y   i, H, x, y   i, M, j, x, y   D, j, x, y   i, E, j, x, y   i, W, j, x, y   T, i, x   x, V, y

Allowed substitution hints:   A( i, j)   D( i)   P( y, j)   R( j)   T( y, j)   F( x, y, i, j)   H( j)   J( y)   V( i, j)

Proof of Theorem vdwlem6

Dummy variables m n z a d are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvex 6201	. . . . . . 7 |- ( G ` ( B + ( E ` i ) ) ) e. _V
2		vdwlem6.j	. . . . . . 7 |- J = ( i e. ( 1 ... M ) |-> ( G ` ( B + ( E ` i ) ) ) )
3	1, 2	fnmpti 6022	. . . . . 6 |- J Fn ( 1 ... M )
4		fvelrnb 6243	. . . . . 6 |- ( J Fn ( 1 ... M ) -> ( ( G ` B ) e. ran J <-> E. m e. ( 1 ... M ) ( J ` m ) = ( G ` B ) ) )
5	3, 4	ax-mp 5	. . . . 5 |- ( ( G ` B ) e. ran J <-> E. m e. ( 1 ... M ) ( J ` m ) = ( G ` B ) )
6		vdwlem4.r	. . . . . . . 8 |- ( ph -> R e. Fin )
7	6	adantr 481	. . . . . . 7 |- ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> R e. Fin )
8		vdwlem7.k	. . . . . . . . 9 |- ( ph -> K e. ( ZZ>= ` 2 ) )
9		eluz2nn 11726	. . . . . . . . 9 |- ( K e. ( ZZ>= ` 2 ) -> K e. NN )
10	8, 9	syl 17	. . . . . . . 8 |- ( ph -> K e. NN )
11	10	adantr 481	. . . . . . 7 |- ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> K e. NN )
12		vdwlem3.w	. . . . . . . 8 |- ( ph -> W e. NN )
13	12	adantr 481	. . . . . . 7 |- ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> W e. NN )
14		vdwlem7.g	. . . . . . . 8 |- ( ph -> G : ( 1 ... W ) --> R )
15	14	adantr 481	. . . . . . 7 |- ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> G : ( 1 ... W ) --> R )
16		vdwlem6.b	. . . . . . . 8 |- ( ph -> B e. NN )
17	16	adantr 481	. . . . . . 7 |- ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> B e. NN )
18		vdwlem7.m	. . . . . . . 8 |- ( ph -> M e. NN )
19	18	adantr 481	. . . . . . 7 |- ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> M e. NN )
20		vdwlem6.e	. . . . . . . 8 |- ( ph -> E : ( 1 ... M ) --> NN )
21	20	adantr 481	. . . . . . 7 |- ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> E : ( 1 ... M ) --> NN )
22		vdwlem6.s	. . . . . . . 8 |- ( ph -> A. i e. ( 1 ... M ) ( ( B + ( E ` i ) ) (AP ` K ) ( E ` i ) ) C_ ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )
23	22	adantr 481	. . . . . . 7 |- ( ( 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 ) ) ) } ) )
24		simprl 794	. . . . . . 7 |- ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> m e. ( 1 ... M ) )
25		simprr 796	. . . . . . . 8 |- ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> ( J ` m ) = ( G ` B ) )
26		fveq2 6191	. . . . . . . . . . . 12 |- ( i = m -> ( E ` i ) = ( E ` m ) )
27	26	oveq2d 6666	. . . . . . . . . . 11 |- ( i = m -> ( B + ( E ` i ) ) = ( B + ( E ` m ) ) )
28	27	fveq2d 6195	. . . . . . . . . 10 |- ( i = m -> ( G ` ( B + ( E ` i ) ) ) = ( G ` ( B + ( E ` m ) ) ) )
29		fvex 6201	. . . . . . . . . 10 |- ( G ` ( B + ( E ` m ) ) ) e. _V
30	28, 2, 29	fvmpt 6282	. . . . . . . . 9 |- ( m e. ( 1 ... M ) -> ( J ` m ) = ( G ` ( B + ( E ` m ) ) ) )
31	24, 30	syl 17	. . . . . . . 8 |- ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> ( J ` m ) = ( G ` ( B + ( E ` m ) ) ) )
32	25, 31	eqtr3d 2658	. . . . . . 7 |- ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> ( G ` B ) = ( G ` ( B + ( E ` m ) ) ) )
33	7, 11, 13, 15, 17, 19, 21, 23, 24, 32	vdwlem1 15685	. . . . . 6 |- ( ( ph /\ ( m e. ( 1 ... M ) /\ ( J ` m ) = ( G ` B ) ) ) -> ( K + 1 ) MonoAP G )
34	33	rexlimdvaa 3032	. . . . 5 |- ( ph -> ( E. m e. ( 1 ... M ) ( J ` m ) = ( G ` B ) -> ( K + 1 ) MonoAP G ) )
35	5, 34	syl5bi 232	. . . 4 |- ( ph -> ( ( G ` B ) e. ran J -> ( K + 1 ) MonoAP G ) )
36	35	imp 445	. . 3 |- ( ( ph /\ ( G ` B ) e. ran J ) -> ( K + 1 ) MonoAP G )
37	36	olcd 408	. 2 |- ( ( ph /\ ( G ` B ) e. ran J ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP G ) )
38		vdwlem3.v	. . . . . . 7 |- ( ph -> V e. NN )
39		vdwlem4.h	. . . . . . 7 |- ( ph -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )
40		vdwlem4.f	. . . . . . 7 |- F = ( x e. ( 1 ... V ) |-> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) )
41		vdwlem7.a	. . . . . . 7 |- ( ph -> A e. NN )
42		vdwlem7.d	. . . . . . 7 |- ( ph -> D e. NN )
43		vdwlem7.s	. . . . . . 7 |- ( ph -> ( A (AP ` K ) D ) C_ ( `' F " { G } ) )
44		vdwlem6.r	. . . . . . 7 |- ( ph -> ( # ` ran J ) = M )
45		vdwlem6.t	. . . . . . 7 |- T = ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) )
46		vdwlem6.p	. . . . . . 7 |- P = ( j e. ( 1 ... ( M + 1 ) ) |-> ( if ( j = ( M + 1 ) , 0 , ( E ` j ) ) + ( W x. D ) ) )
47	38, 12, 6, 39, 40, 18, 14, 8, 41, 42, 43, 16, 20, 22, 2, 44, 45, 46	vdwlem5 15689	. . . . . 6 |- ( ph -> T e. NN )
48	47	adantr 481	. . . . 5 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> T e. NN )
49		0nn0 11307	. . . . . . . . . 10 |- 0 e. NN0
50	49	a1i 11	. . . . . . . . 9 |- ( ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) /\ j = ( M + 1 ) ) -> 0 e. NN0 )
51		nnuz 11723	. . . . . . . . . . . . . . . . 17 |- NN = ( ZZ>= ` 1 )
52	18, 51	syl6eleq 2711	. . . . . . . . . . . . . . . 16 |- ( ph -> M e. ( ZZ>= ` 1 ) )
53	52	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> M e. ( ZZ>= ` 1 ) )
54		elfzp1 12391	. . . . . . . . . . . . . . 15 |- ( M e. ( ZZ>= ` 1 ) -> ( j e. ( 1 ... ( M + 1 ) ) <-> ( j e. ( 1 ... M ) \/ j = ( M + 1 ) ) ) )
55	53, 54	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( j e. ( 1 ... ( M + 1 ) ) <-> ( j e. ( 1 ... M ) \/ j = ( M + 1 ) ) ) )
56	55	biimpa 501	. . . . . . . . . . . . 13 |- ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) -> ( j e. ( 1 ... M ) \/ j = ( M + 1 ) ) )
57	56	ord 392	. . . . . . . . . . . 12 |- ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) -> ( -. j e. ( 1 ... M ) -> j = ( M + 1 ) ) )
58	57	con1d 139	. . . . . . . . . . 11 |- ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) -> ( -. j = ( M + 1 ) -> j e. ( 1 ... M ) ) )
59	58	imp 445	. . . . . . . . . 10 |- ( ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) /\ -. j = ( M + 1 ) ) -> j e. ( 1 ... M ) )
60	20	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) -> E : ( 1 ... M ) --> NN )
61	60	ffvelrnda 6359	. . . . . . . . . . 11 |- ( ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) /\ j e. ( 1 ... M ) ) -> ( E ` j ) e. NN )
62	61	nnnn0d 11351	. . . . . . . . . 10 |- ( ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) /\ j e. ( 1 ... M ) ) -> ( E ` j ) e. NN0 )
63	59, 62	syldan 487	. . . . . . . . 9 |- ( ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) /\ -. j = ( M + 1 ) ) -> ( E ` j ) e. NN0 )
64	50, 63	ifclda 4120	. . . . . . . 8 |- ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) -> if ( j = ( M + 1 ) , 0 , ( E ` j ) ) e. NN0 )
65	12, 42	nnmulcld 11068	. . . . . . . . 9 |- ( ph -> ( W x. D ) e. NN )
66	65	ad2antrr 762	. . . . . . . 8 |- ( ( ( ph /\ -. ( G ` B ) e. ran J ) /\ j e. ( 1 ... ( M + 1 ) ) ) -> ( W x. D ) e. NN )
67		nn0nnaddcl 11324	. . . . . . . 8 |- ( ( 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 693	. . . . . . 7 |- ( ( ( 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, 46	fmptd 6385	. . . . . 6 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> P : ( 1 ... ( M + 1 ) ) --> NN )
70		nnex 11026	. . . . . . 7 |- NN e. _V
71		ovex 6678	. . . . . . 7 |- ( 1 ... ( M + 1 ) ) e. _V
72	70, 71	elmap 7886	. . . . . 6 |- ( P e. ( NN ^m ( 1 ... ( M + 1 ) ) ) <-> P : ( 1 ... ( M + 1 ) ) --> NN )
73	69, 72	sylibr 224	. . . . 5 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> P e. ( NN ^m ( 1 ... ( M + 1 ) ) ) )
74		elfzp1 12391	. . . . . . . . . 10 |- ( M e. ( ZZ>= ` 1 ) -> ( i e. ( 1 ... ( M + 1 ) ) <-> ( i e. ( 1 ... M ) \/ i = ( M + 1 ) ) ) )
75	52, 74	syl 17	. . . . . . . . 9 |- ( ph -> ( i e. ( 1 ... ( M + 1 ) ) <-> ( i e. ( 1 ... M ) \/ i = ( M + 1 ) ) ) )
76	16	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ i e. ( 1 ... M ) ) -> B e. NN )
77	76	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ i e. ( 1 ... M ) ) -> B e. CC )
78	77	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> B e. CC )
79	20	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( E ` i ) e. NN )
80	79	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( E ` i ) e. CC )
81	80	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( E ` i ) e. CC )
82	78, 81	addcld 10059	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( B + ( E ` i ) ) e. CC )
83		nnm1nn0 11334	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A e. NN -> ( A - 1 ) e. NN0 )
84	41, 83	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( A - 1 ) e. NN0 )
85		nn0nnaddcl 11324	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( A - 1 ) e. NN0 /\ V e. NN ) -> ( ( A - 1 ) + V ) e. NN )
86	84, 38, 85	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( ( A - 1 ) + V ) e. NN )
87	12, 86	nnmulcld 11068	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( W x. ( ( A - 1 ) + V ) ) e. NN )
88	87	nncnd 11036	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( W x. ( ( A - 1 ) + V ) ) e. CC )
89	88	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( W x. ( ( A - 1 ) + V ) ) e. CC )
90		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( m e. ( 0 ... ( K - 1 ) ) -> m e. NN0 )
91	90	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> m e. NN0 )
92	91	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> m e. CC )
93	92	adantlr 751	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> m e. CC )
94	93, 81	mulcld 10060	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. ( E ` i ) ) e. CC )
95	65	nnnn0d 11351	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( W x. D ) e. NN0 )
96	95	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( W x. D ) e. NN0 )
97	91, 96	nn0mulcld 11356	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. ( W x. D ) ) e. NN0 )
98	97	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. ( W x. D ) ) e. CC )
99	98	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. ( W x. D ) ) e. CC )
100	82, 89, 94, 99	add4d 10264	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 11036	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( W x. D ) e. CC )
102	101	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( W x. D ) e. CC )
103	93, 81, 102	adddid 10064	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 6666	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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	12	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> W e. CC )
106	105	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> W e. CC )
107	86	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( ( A - 1 ) + V ) e. CC )
108	107	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A - 1 ) + V ) e. CC )
109	42	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> D e. CC )
110	109	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> D e. CC )
111	92, 110	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. D ) e. CC )
112	106, 108, 111	adddid 10064	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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	41	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> A e. CC )
114	113	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> A e. CC )
115		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> 1 e. CC )
116	114, 111, 115	addsubd 10413	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A + ( m x. D ) ) - 1 ) = ( ( A - 1 ) + ( m x. D ) ) )
117	116	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( A + ( m x. D ) ) - 1 ) + V ) = ( ( ( A - 1 ) + ( m x. D ) ) + V ) )
118	84	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( A - 1 ) e. CC )
119	118	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A - 1 ) e. CC )
120	38	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> V e. CC )
121	120	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> V e. CC )
122	119, 111, 121	add32d 10263	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( A - 1 ) + ( m x. D ) ) + V ) = ( ( ( A - 1 ) + V ) + ( m x. D ) ) )
123	117, 122	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( A + ( m x. D ) ) - 1 ) + V ) = ( ( ( A - 1 ) + V ) + ( m x. D ) ) )
124	123	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 10245	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. ( W x. D ) ) = ( W x. ( m x. D ) ) )
126	125	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 2666	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 751	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 6666	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 2666	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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	38	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> V e. NN )
132	12	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> W e. NN )
133	43	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A (AP ` K ) D ) C_ ( `' F " { G } ) )
134		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A + ( m x. D ) ) = ( A + ( m x. D ) )
135		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( n = m -> ( n x. D ) = ( m x. D ) )
136	135	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( n = m -> ( A + ( n x. D ) ) = ( A + ( m x. D ) ) )
137	136	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( n = m -> ( ( A + ( m x. D ) ) = ( A + ( n x. D ) ) <-> ( A + ( m x. D ) ) = ( A + ( m x. D ) ) ) )
138	137	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 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 ) ) )
139	134, 138	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( m e. ( 0 ... ( K - 1 ) ) -> E. n e. ( 0 ... ( K - 1 ) ) ( A + ( m x. D ) ) = ( A + ( n x. D ) ) )
140	10	nnnn0d 11351	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> K e. NN0 )
141		vdwapval 15677	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 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 ) ) ) )
142	140, 41, 42, 141	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( A + ( m x. D ) ) e. ( A (AP ` K ) D ) <-> E. n e. ( 0 ... ( K - 1 ) ) ( A + ( m x. D ) ) = ( A + ( n x. D ) ) ) )
143	142	biimpar 502	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ E. n e. ( 0 ... ( K - 1 ) ) ( A + ( m x. D ) ) = ( A + ( n x. D ) ) ) -> ( A + ( m x. D ) ) e. ( A (AP ` K ) D ) )
144	139, 143	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + ( m x. D ) ) e. ( A (AP ` K ) D ) )
145	133, 144	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + ( m x. D ) ) e. ( `' F " { G } ) )
146	38, 12, 6, 39, 40	vdwlem4 15688	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) )
147		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) -> F Fn ( 1 ... V ) )
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> F Fn ( 1 ... V ) )
149		fniniseg 6338	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( F Fn ( 1 ... V ) -> ( ( A + ( m x. D ) ) e. ( `' F " { G } ) <-> ( ( A + ( m x. D ) ) e. ( 1 ... V ) /\ ( F ` ( A + ( m x. D ) ) ) = G ) ) )
150	148, 149	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( ( A + ( m x. D ) ) e. ( `' F " { G } ) <-> ( ( A + ( m x. D ) ) e. ( 1 ... V ) /\ ( F ` ( A + ( m x. D ) ) ) = G ) ) )
151	150	biimpa 501	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( A + ( m x. D ) ) e. ( `' F " { G } ) ) -> ( ( A + ( m x. D ) ) e. ( 1 ... V ) /\ ( F ` ( A + ( m x. D ) ) ) = G ) )
152	145, 151	syldan 487	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A + ( m x. D ) ) e. ( 1 ... V ) /\ ( F ` ( A + ( m x. D ) ) ) = G ) )
153	152	simpld 475	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + ( m x. D ) ) e. ( 1 ... V ) )
154	153	adantlr 751	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + ( m x. D ) ) e. ( 1 ... V ) )
155	22	r19.21bi 2932	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( B + ( E ` i ) ) (AP ` K ) ( E ` i ) ) C_ ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )
156	155	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( B + ( E ` i ) ) (AP ` K ) ( E ` i ) ) C_ ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )
157		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) = ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) )
158		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( n = m -> ( n x. ( E ` i ) ) = ( m x. ( E ` i ) ) )
159	158	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( n = m -> ( ( B + ( E ` i ) ) + ( n x. ( E ` i ) ) ) = ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) )
160	159	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( n = m -> ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) = ( ( B + ( E ` i ) ) + ( n x. ( E ` i ) ) ) <-> ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) = ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) ) )
161	160	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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 ) ) ) )
162	157, 161	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 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 ) ) ) )
163	10	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ i e. ( 1 ... M ) ) -> K e. NN )
164	163	nnnn0d 11351	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ i e. ( 1 ... M ) ) -> K e. NN0 )
165	76, 79	nnaddcld 11067	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( B + ( E ` i ) ) e. NN )
166		vdwapval 15677	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 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 ) ) ) ) )
167	164, 165, 79, 166	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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 ) ) ) ) )
168	167	biimpar 502	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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 ) ) )
169	162, 168	sylan2 491	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 ) ) )
170	156, 169	sseldd 3604	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )
171		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( G : ( 1 ... W ) --> R -> G Fn ( 1 ... W ) )
172	14, 171	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> G Fn ( 1 ... W ) )
173	172	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ i e. ( 1 ... M ) ) -> G Fn ( 1 ... W ) )
174		fniniseg 6338	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 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 ) ) ) ) ) )
175	173, 174	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 ) ) ) ) ) )
176	175	biimpa 501	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 ) ) ) ) )
177	170, 176	syldan 487	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) ) ) ) )
178	177	simpld 475	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) e. ( 1 ... W ) )
179	131, 132, 154, 178	vdwlem3 15687	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) )
180	130, 179	eqeltrd 2701	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) ) )
181		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) -> ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) = ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) )
182	181	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) ) ) )
183		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) ) ) )
184		fvex 6201	. . . . . . . . . . . . . . . . . . . 20 |- ( H ` ( ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) e. _V
185	182, 183, 184	fvmpt 6282	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) ) ) )
186	178, 185	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) ) )
187	177	simprd 479	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( G ` ( ( B + ( E ` i ) ) + ( m x. ( E ` i ) ) ) ) = ( G ` ( B + ( E ` i ) ) ) )
188	152	simprd 479	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( F ` ( A + ( m x. D ) ) ) = G )
189		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x = ( A + ( m x. D ) ) -> ( x - 1 ) = ( ( A + ( m x. D ) ) - 1 ) )
190	189	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x = ( A + ( m x. D ) ) -> ( ( x - 1 ) + V ) = ( ( ( A + ( m x. D ) ) - 1 ) + V ) )
191	190	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x = ( A + ( m x. D ) ) -> ( W x. ( ( x - 1 ) + V ) ) = ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) )
192	191	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x = ( A + ( m x. D ) ) -> ( y + ( W x. ( ( x - 1 ) + V ) ) ) = ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) )
193	192	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = ( A + ( m x. D ) ) -> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) = ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) )
194	193	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 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 ) ) ) ) ) )
195		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 1 ... W ) e. _V
196	195	mptex 6486	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) e. _V
197	194, 40, 196	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 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 ) ) ) ) ) )
198	153, 197	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 ) ) ) ) ) )
199	188, 198	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> G = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) )
200	199	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) ) ) ) ) )
201	200	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) ) ) )
202	187, 201	eqtr3d 2658	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) ) )
203	130	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) ) )
204	186, 202, 203	3eqtr4rd 2667	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) ) )
205	180, 204	jca 554	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) ) ) ) )
206		eleq1 2689	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) ) ) )
207		fveq2 6191	. . . . . . . . . . . . . . . . . 18 |- ( x = ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) -> ( H ` x ) = ( H ` ( ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( ( E ` i ) + ( W x. D ) ) ) ) ) )
208	207	eqeq1d 2624	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) ) ) )
209	206, 208	anbi12d 747	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) ) ) )
210	205, 209	syl5ibrcom 237	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) ) ) ) )
211	210	rexlimdva 3031	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) ) ) )
212	87	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( W x. ( ( A - 1 ) + V ) ) e. NN )
213	165, 212	nnaddcld 11067	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) e. NN )
214	65	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( W x. D ) e. NN )
215	79, 214	nnaddcld 11067	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( E ` i ) + ( W x. D ) ) e. NN )
216		vdwapval 15677	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) ) ) )
217	164, 213, 215, 216	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) ) ) )
218		ffn 6045	. . . . . . . . . . . . . . . . 17 |- ( H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R -> H Fn ( 1 ... ( W x. ( 2 x. V ) ) ) )
219	39, 218	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> H Fn ( 1 ... ( W x. ( 2 x. V ) ) ) )
220	219	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 1 ... M ) ) -> H Fn ( 1 ... ( W x. ( 2 x. V ) ) ) )
221		fniniseg 6338	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) ) )
222	220, 221	syl 17	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) ) ) )
223	211, 217, 222	3imtr4d 283	. . . . . . . . . . . . 13 |- ( ( 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 ) ) ) } ) ) )
224	223	ssrdv 3609	. . . . . . . . . . . 12 |- ( ( 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 ) ) ) } ) )
225		ssun1 3776	. . . . . . . . . . . . . . . . . . 19 |- ( 1 ... M ) C_ ( ( 1 ... M ) u. { ( M + 1 ) } )
226		fzsuc 12388	. . . . . . . . . . . . . . . . . . . 20 |- ( M e. ( ZZ>= ` 1 ) -> ( 1 ... ( M + 1 ) ) = ( ( 1 ... M ) u. { ( M + 1 ) } ) )
227	52, 226	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 1 ... ( M + 1 ) ) = ( ( 1 ... M ) u. { ( M + 1 ) } ) )
228	225, 227	syl5sseqr 3654	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( 1 ... M ) C_ ( 1 ... ( M + 1 ) ) )
229	228	sselda 3603	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 1 ... M ) ) -> i e. ( 1 ... ( M + 1 ) ) )
230		eqeq1 2626	. . . . . . . . . . . . . . . . . . . 20 |- ( j = i -> ( j = ( M + 1 ) <-> i = ( M + 1 ) ) )
231		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 |- ( j = i -> ( E ` j ) = ( E ` i ) )
232	230, 231	ifbieq2d 4111	. . . . . . . . . . . . . . . . . . 19 |- ( j = i -> if ( j = ( M + 1 ) , 0 , ( E ` j ) ) = if ( i = ( M + 1 ) , 0 , ( E ` i ) ) )
233	232	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( j = i -> ( if ( j = ( M + 1 ) , 0 , ( E ` j ) ) + ( W x. D ) ) = ( if ( i = ( M + 1 ) , 0 , ( E ` i ) ) + ( W x. D ) ) )
234		ovex 6678	. . . . . . . . . . . . . . . . . 18 |- ( if ( i = ( M + 1 ) , 0 , ( E ` i ) ) + ( W x. D ) ) e. _V
235	233, 46, 234	fvmpt 6282	. . . . . . . . . . . . . . . . 17 |- ( i e. ( 1 ... ( M + 1 ) ) -> ( P ` i ) = ( if ( i = ( M + 1 ) , 0 , ( E ` i ) ) + ( W x. D ) ) )
236	229, 235	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( P ` i ) = ( if ( i = ( M + 1 ) , 0 , ( E ` i ) ) + ( W x. D ) ) )
237		elfzle2 12345	. . . . . . . . . . . . . . . . . . 19 |- ( i e. ( 1 ... M ) -> i <_ M )
238	18	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> M e. RR )
239	238	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> M < ( M + 1 ) )
240		peano2re 10209	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( M e. RR -> ( M + 1 ) e. RR )
241	238, 240	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( M + 1 ) e. RR )
242	238, 241	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( M < ( M + 1 ) <-> -. ( M + 1 ) <_ M ) )
243	239, 242	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> -. ( M + 1 ) <_ M )
244		breq1 4656	. . . . . . . . . . . . . . . . . . . . . 22 |- ( i = ( M + 1 ) -> ( i <_ M <-> ( M + 1 ) <_ M ) )
245	244	notbid 308	. . . . . . . . . . . . . . . . . . . . 21 |- ( i = ( M + 1 ) -> ( -. i <_ M <-> -. ( M + 1 ) <_ M ) )
246	243, 245	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( i = ( M + 1 ) -> -. i <_ M ) )
247	246	con2d 129	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( i <_ M -> -. i = ( M + 1 ) ) )
248	237, 247	syl5 34	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( i e. ( 1 ... M ) -> -. i = ( M + 1 ) ) )
249	248	imp 445	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 1 ... M ) ) -> -. i = ( M + 1 ) )
250		iffalse 4095	. . . . . . . . . . . . . . . . . 18 |- ( -. i = ( M + 1 ) -> if ( i = ( M + 1 ) , 0 , ( E ` i ) ) = ( E ` i ) )
251	250	oveq1d 6665	. . . . . . . . . . . . . . . . 17 |- ( -. i = ( M + 1 ) -> ( if ( i = ( M + 1 ) , 0 , ( E ` i ) ) + ( W x. D ) ) = ( ( E ` i ) + ( W x. D ) ) )
252	249, 251	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( if ( i = ( M + 1 ) , 0 , ( E ` i ) ) + ( W x. D ) ) = ( ( E ` i ) + ( W x. D ) ) )
253	236, 252	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( P ` i ) = ( ( E ` i ) + ( W x. D ) ) )
254	253	oveq2d 6666	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( T + ( P ` i ) ) = ( T + ( ( E ` i ) + ( W x. D ) ) ) )
255	47	nncnd 11036	. . . . . . . . . . . . . . . 16 |- ( ph -> T e. CC )
256	255	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 1 ... M ) ) -> T e. CC )
257	101	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( W x. D ) e. CC )
258	256, 80, 257	add12d 10262	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( T + ( ( E ` i ) + ( W x. D ) ) ) = ( ( E ` i ) + ( T + ( W x. D ) ) ) )
259	45	oveq1i 6660	. . . . . . . . . . . . . . . . . 18 |- ( T + ( W x. D ) ) = ( ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) ) + ( W x. D ) )
260	16	nncnd 11036	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> B e. CC )
261	120, 109	subcld 10392	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( V - D ) e. CC )
262	113, 261	addcld 10059	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( A + ( V - D ) ) e. CC )
263		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. CC
264		subcl 10280	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( A + ( V - D ) ) e. CC /\ 1 e. CC ) -> ( ( A + ( V - D ) ) - 1 ) e. CC )
265	262, 263, 264	sylancl 694	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( A + ( V - D ) ) - 1 ) e. CC )
266	105, 265	mulcld 10060	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( W x. ( ( A + ( V - D ) ) - 1 ) ) e. CC )
267	260, 266, 101	addassd 10062	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) ) + ( W x. D ) ) = ( B + ( ( W x. ( ( A + ( V - D ) ) - 1 ) ) + ( W x. D ) ) ) )
268	105, 265, 109	adddid 10064	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( W x. ( ( ( A + ( V - D ) ) - 1 ) + D ) ) = ( ( W x. ( ( A + ( V - D ) ) - 1 ) ) + ( W x. D ) ) )
269	113, 261, 109	addassd 10062	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( A + ( V - D ) ) + D ) = ( A + ( ( V - D ) + D ) ) )
270	120, 109	npcand 10396	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( V - D ) + D ) = V )
271	270	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( A + ( ( V - D ) + D ) ) = ( A + V ) )
272	269, 271	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( ( A + ( V - D ) ) + D ) = ( A + V ) )
273	272	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( ( ( A + ( V - D ) ) + D ) - 1 ) = ( ( A + V ) - 1 ) )
274		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> 1 e. CC )
275	262, 109, 274	addsubd 10413	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( ( ( A + ( V - D ) ) + D ) - 1 ) = ( ( ( A + ( V - D ) ) - 1 ) + D ) )
276	113, 120, 274	addsubd 10413	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( ( A + V ) - 1 ) = ( ( A - 1 ) + V ) )
277	273, 275, 276	3eqtr3d 2664	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( ( ( A + ( V - D ) ) - 1 ) + D ) = ( ( A - 1 ) + V ) )
278	277	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( W x. ( ( ( A + ( V - D ) ) - 1 ) + D ) ) = ( W x. ( ( A - 1 ) + V ) ) )
279	268, 278	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( W x. ( ( A + ( V - D ) ) - 1 ) ) + ( W x. D ) ) = ( W x. ( ( A - 1 ) + V ) ) )
280	279	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( B + ( ( W x. ( ( A + ( V - D ) ) - 1 ) ) + ( W x. D ) ) ) = ( B + ( W x. ( ( A - 1 ) + V ) ) ) )
281	267, 280	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) ) + ( W x. D ) ) = ( B + ( W x. ( ( A - 1 ) + V ) ) ) )
282	259, 281	syl5eq 2668	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( T + ( W x. D ) ) = ( B + ( W x. ( ( A - 1 ) + V ) ) ) )
283	282	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( E ` i ) + ( T + ( W x. D ) ) ) = ( ( E ` i ) + ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) )
284	283	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( E ` i ) + ( T + ( W x. D ) ) ) = ( ( E ` i ) + ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) )
285	88	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( W x. ( ( A - 1 ) + V ) ) e. CC )
286	80, 77, 285	addassd 10062	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( ( E ` i ) + B ) + ( W x. ( ( A - 1 ) + V ) ) ) = ( ( E ` i ) + ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) )
287	80, 77	addcomd 10238	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( E ` i ) + B ) = ( B + ( E ` i ) ) )
288	287	oveq1d 6665	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( ( E ` i ) + B ) + ( W x. ( ( A - 1 ) + V ) ) ) = ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) )
289	284, 286, 288	3eqtr2d 2662	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( E ` i ) + ( T + ( W x. D ) ) ) = ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) )
290	254, 258, 289	3eqtrd 2660	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( T + ( P ` i ) ) = ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) )
291	290, 253	oveq12d 6668	. . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
292		cnvimass 5485	. . . . . . . . . . . . . . . . . . 19 |- ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) C_ dom G
293		fdm 6051	. . . . . . . . . . . . . . . . . . . 20 |- ( G : ( 1 ... W ) --> R -> dom G = ( 1 ... W ) )
294	14, 293	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> dom G = ( 1 ... W ) )
295	292, 294	syl5sseq 3653	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) C_ ( 1 ... W ) )
296	295	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) C_ ( 1 ... W ) )
297		vdwapid1 15679	. . . . . . . . . . . . . . . . . . 19 |- ( ( K e. NN /\ ( B + ( E ` i ) ) e. NN /\ ( E ` i ) e. NN ) -> ( B + ( E ` i ) ) e. ( ( B + ( E ` i ) ) (AP ` K ) ( E ` i ) ) )
298	163, 165, 79, 297	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( B + ( E ` i ) ) e. ( ( B + ( E ` i ) ) (AP ` K ) ( E ` i ) ) )
299	155, 298	sseldd 3604	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( B + ( E ` i ) ) e. ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )
300	296, 299	sseldd 3604	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( B + ( E ` i ) ) e. ( 1 ... W ) )
301		oveq1 6657	. . . . . . . . . . . . . . . . . 18 |- ( y = ( B + ( E ` i ) ) -> ( y + ( W x. ( ( A - 1 ) + V ) ) ) = ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) )
302	301	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( y = ( B + ( E ` i ) ) -> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) = ( H ` ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) ) )
303		eqid 2622	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) )
304		fvex 6201	. . . . . . . . . . . . . . . . 17 |- ( H ` ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) ) e. _V
305	302, 303, 304	fvmpt 6282	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) ) )
306	300, 305	syl 17	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) ) )
307		vdwapid1 15679	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( K e. NN /\ A e. NN /\ D e. NN ) -> A e. ( A (AP ` K ) D ) )
308	10, 41, 42, 307	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> A e. ( A (AP ` K ) D ) )
309	43, 308	sseldd 3604	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> A e. ( `' F " { G } ) )
310		fniniseg 6338	. . . . . . . . . . . . . . . . . . . . 21 |- ( F Fn ( 1 ... V ) -> ( A e. ( `' F " { G } ) <-> ( A e. ( 1 ... V ) /\ ( F ` A ) = G ) ) )
311	148, 310	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( A e. ( `' F " { G } ) <-> ( A e. ( 1 ... V ) /\ ( F ` A ) = G ) ) )
312	309, 311	mpbid 222	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( A e. ( 1 ... V ) /\ ( F ` A ) = G ) )
313	312	simprd 479	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( F ` A ) = G )
314	312	simpld 475	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A e. ( 1 ... V ) )
315		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = A -> ( x - 1 ) = ( A - 1 ) )
316	315	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = A -> ( ( x - 1 ) + V ) = ( ( A - 1 ) + V ) )
317	316	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = A -> ( W x. ( ( x - 1 ) + V ) ) = ( W x. ( ( A - 1 ) + V ) ) )
318	317	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = A -> ( y + ( W x. ( ( x - 1 ) + V ) ) ) = ( y + ( W x. ( ( A - 1 ) + V ) ) ) )
319	318	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = A -> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) = ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) )
320	319	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . 20 |- ( x = A -> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) )
321	195	mptex 6486	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) e. _V
322	320, 40, 321	fvmpt 6282	. . . . . . . . . . . . . . . . . . 19 |- ( A e. ( 1 ... V ) -> ( F ` A ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) )
323	314, 322	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( F ` A ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) )
324	313, 323	eqtr3d 2658	. . . . . . . . . . . . . . . . 17 |- ( ph -> G = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) )
325	324	fveq1d 6193	. . . . . . . . . . . . . . . 16 |- ( ph -> ( G ` ( B + ( E ` i ) ) ) = ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) ` ( B + ( E ` i ) ) ) )
326	325	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( G ` ( B + ( E ` i ) ) ) = ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) ` ( B + ( E ` i ) ) ) )
327	290	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( H ` ( T + ( P ` i ) ) ) = ( H ` ( ( B + ( E ` i ) ) + ( W x. ( ( A - 1 ) + V ) ) ) ) )
328	306, 326, 327	3eqtr4rd 2667	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( H ` ( T + ( P ` i ) ) ) = ( G ` ( B + ( E ` i ) ) ) )
329	328	sneqd 4189	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 1 ... M ) ) -> { ( H ` ( T + ( P ` i ) ) ) } = { ( G ` ( B + ( E ` i ) ) ) } )
330	329	imaeq2d 5466	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) = ( `' H " { ( G ` ( B + ( E ` i ) ) ) } ) )
331	224, 291, 330	3sstr4d 3648	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( T + ( P ` i ) ) (AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) )
332	331	ex 450	. . . . . . . . . 10 |- ( ph -> ( i e. ( 1 ... M ) -> ( ( T + ( P ` i ) ) (AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) ) )
333	260	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> B e. CC )
334	88	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( W x. ( ( A - 1 ) + V ) ) e. CC )
335	333, 334, 98	addassd 10062	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) ) ) )
336	127	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) ) ) )
337	335, 336	eqtr4d 2659	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) )
338	38	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> V e. NN )
339	12	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> W e. NN )
340		eluzfz1 12348	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( M e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... M ) )
341	52, 340	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> 1 e. ( 1 ... M ) )
342		ne0i 3921	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1 e. ( 1 ... M ) -> ( 1 ... M ) =/= (/) )
343	341, 342	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( 1 ... M ) =/= (/) )
344		elfzuz3 12339	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( B + ( E ` i ) ) e. ( 1 ... W ) -> W e. ( ZZ>= ` ( B + ( E ` i ) ) ) )
345	300, 344	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ i e. ( 1 ... M ) ) -> W e. ( ZZ>= ` ( B + ( E ` i ) ) ) )
346	16	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> B e. ZZ )
347		uzid 11702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( B e. ZZ -> B e. ( ZZ>= ` B ) )
348	346, 347	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> B e. ( ZZ>= ` B ) )
349	348	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ i e. ( 1 ... M ) ) -> B e. ( ZZ>= ` B ) )
350	79	nnnn0d 11351	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( E ` i ) e. NN0 )
351		uzaddcl 11744	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( B e. ( ZZ>= ` B ) /\ ( E ` i ) e. NN0 ) -> ( B + ( E ` i ) ) e. ( ZZ>= ` B ) )
352	349, 350, 351	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( B + ( E ` i ) ) e. ( ZZ>= ` B ) )
353		uztrn 11704	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( W e. ( ZZ>= ` ( B + ( E ` i ) ) ) /\ ( B + ( E ` i ) ) e. ( ZZ>= ` B ) ) -> W e. ( ZZ>= ` B ) )
354	345, 352, 353	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ i e. ( 1 ... M ) ) -> W e. ( ZZ>= ` B ) )
355		eluzle 11700	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( W e. ( ZZ>= ` B ) -> B <_ W )
356	354, 355	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ i e. ( 1 ... M ) ) -> B <_ W )
357	356	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> A. i e. ( 1 ... M ) B <_ W )
358		r19.2z 4060	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 1 ... M ) =/= (/) /\ A. i e. ( 1 ... M ) B <_ W ) -> E. i e. ( 1 ... M ) B <_ W )
359	343, 357, 358	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> E. i e. ( 1 ... M ) B <_ W )
360		idd 24	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( i e. ( 1 ... M ) -> ( B <_ W -> B <_ W ) )
361	360	rexlimiv 3027	. . . . . . . . . . . . . . . . . . . . . 22 |- ( E. i e. ( 1 ... M ) B <_ W -> B <_ W )
362	359, 361	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> B <_ W )
363	12	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> W e. ZZ )
364		fznn 12408	. . . . . . . . . . . . . . . . . . . . . 22 |- ( W e. ZZ -> ( B e. ( 1 ... W ) <-> ( B e. NN /\ B <_ W ) ) )
365	363, 364	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( B e. ( 1 ... W ) <-> ( B e. NN /\ B <_ W ) ) )
366	16, 362, 365	mpbir2and 957	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> B e. ( 1 ... W ) )
367	366	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> B e. ( 1 ... W ) )
368	338, 339, 153, 367	vdwlem3 15687	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( B + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) )
369	337, 368	eqeltrd 2701	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) )
370		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = B -> ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) = ( B + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) )
371	370	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 |- ( y = B -> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) = ( H ` ( B + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) )
372		fvex 6201	. . . . . . . . . . . . . . . . . . . 20 |- ( H ` ( B + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) e. _V
373	371, 183, 372	fvmpt 6282	. . . . . . . . . . . . . . . . . . 19 |- ( 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 ) ) ) ) )
374	367, 373	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) ) )
375	199	fveq1d 6193	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( G ` B ) = ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( ( A + ( m x. D ) ) - 1 ) + V ) ) ) ) ) ` B ) )
376	337	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) ) )
377	374, 375, 376	3eqtr4rd 2667	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( H ` ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) ) = ( G ` B ) )
378	369, 377	jca 554	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) )
379		eleq1 2689	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) ) ) )
380		fveq2 6191	. . . . . . . . . . . . . . . . . 18 |- ( z = ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) -> ( H ` z ) = ( H ` ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) + ( m x. ( W x. D ) ) ) ) )
381	380	eqeq1d 2624	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) )
382	379, 381	anbi12d 747	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) )
383	378, 382	syl5ibrcom 237	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) )
384	383	rexlimdva 3031	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) )
385	16, 87	nnaddcld 11067	. . . . . . . . . . . . . . 15 |- ( ph -> ( B + ( W x. ( ( A - 1 ) + V ) ) ) e. NN )
386		vdwapval 15677	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) ) )
387	140, 385, 65, 386	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) ) )
388		fniniseg 6338	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) )
389	219, 388	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ( z e. ( `' H " { ( G ` B ) } ) <-> ( z e. ( 1 ... ( W x. ( 2 x. V ) ) ) /\ ( H ` z ) = ( G ` B ) ) ) )
390	384, 387, 389	3imtr4d 283	. . . . . . . . . . . . 13 |- ( ph -> ( z e. ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) (AP ` K ) ( W x. D ) ) -> z e. ( `' H " { ( G ` B ) } ) ) )
391	390	ssrdv 3609	. . . . . . . . . . . 12 |- ( ph -> ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) (AP ` K ) ( W x. D ) ) C_ ( `' H " { ( G ` B ) } ) )
392	18	peano2nnd 11037	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( M + 1 ) e. NN )
393	392, 51	syl6eleq 2711	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( M + 1 ) e. ( ZZ>= ` 1 ) )
394		eluzfz2 12349	. . . . . . . . . . . . . . . . . 18 |- ( ( M + 1 ) e. ( ZZ>= ` 1 ) -> ( M + 1 ) e. ( 1 ... ( M + 1 ) ) )
395	393, 394	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( M + 1 ) e. ( 1 ... ( M + 1 ) ) )
396		iftrue 4092	. . . . . . . . . . . . . . . . . . 19 |- ( j = ( M + 1 ) -> if ( j = ( M + 1 ) , 0 , ( E ` j ) ) = 0 )
397	396	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( j = ( M + 1 ) -> ( if ( j = ( M + 1 ) , 0 , ( E ` j ) ) + ( W x. D ) ) = ( 0 + ( W x. D ) ) )
398		ovex 6678	. . . . . . . . . . . . . . . . . 18 |- ( 0 + ( W x. D ) ) e. _V
399	397, 46, 398	fvmpt 6282	. . . . . . . . . . . . . . . . 17 |- ( ( M + 1 ) e. ( 1 ... ( M + 1 ) ) -> ( P ` ( M + 1 ) ) = ( 0 + ( W x. D ) ) )
400	395, 399	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> ( P ` ( M + 1 ) ) = ( 0 + ( W x. D ) ) )
401	101	addid2d 10237	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 0 + ( W x. D ) ) = ( W x. D ) )
402	400, 401	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ph -> ( P ` ( M + 1 ) ) = ( W x. D ) )
403	402	oveq2d 6666	. . . . . . . . . . . . . 14 |- ( ph -> ( T + ( P ` ( M + 1 ) ) ) = ( T + ( W x. D ) ) )
404	403, 282	eqtrd 2656	. . . . . . . . . . . . 13 |- ( ph -> ( T + ( P ` ( M + 1 ) ) ) = ( B + ( W x. ( ( A - 1 ) + V ) ) ) )
405	404, 402	oveq12d 6668	. . . . . . . . . . . 12 |- ( ph -> ( ( T + ( P ` ( M + 1 ) ) ) (AP ` K ) ( P ` ( M + 1 ) ) ) = ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) (AP ` K ) ( W x. D ) ) )
406		oveq1 6657	. . . . . . . . . . . . . . . . . 18 |- ( y = B -> ( y + ( W x. ( ( A - 1 ) + V ) ) ) = ( B + ( W x. ( ( A - 1 ) + V ) ) ) )
407	406	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( y = B -> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) = ( H ` ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) )
408		fvex 6201	. . . . . . . . . . . . . . . . 17 |- ( H ` ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) e. _V
409	407, 303, 408	fvmpt 6282	. . . . . . . . . . . . . . . 16 |- ( B e. ( 1 ... W ) -> ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) ` B ) = ( H ` ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) )
410	366, 409	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) ` B ) = ( H ` ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) )
411	324	fveq1d 6193	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` B ) = ( ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( A - 1 ) + V ) ) ) ) ) ` B ) )
412	404	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( ph -> ( H ` ( T + ( P ` ( M + 1 ) ) ) ) = ( H ` ( B + ( W x. ( ( A - 1 ) + V ) ) ) ) )
413	410, 411, 412	3eqtr4rd 2667	. . . . . . . . . . . . . 14 |- ( ph -> ( H ` ( T + ( P ` ( M + 1 ) ) ) ) = ( G ` B ) )
414	413	sneqd 4189	. . . . . . . . . . . . 13 |- ( ph -> { ( H ` ( T + ( P ` ( M + 1 ) ) ) ) } = { ( G ` B ) } )
415	414	imaeq2d 5466	. . . . . . . . . . . 12 |- ( ph -> ( `' H " { ( H ` ( T + ( P ` ( M + 1 ) ) ) ) } ) = ( `' H " { ( G ` B ) } ) )
416	391, 405, 415	3sstr4d 3648	. . . . . . . . . . 11 |- ( ph -> ( ( T + ( P ` ( M + 1 ) ) ) (AP ` K ) ( P ` ( M + 1 ) ) ) C_ ( `' H " { ( H ` ( T + ( P ` ( M + 1 ) ) ) ) } ) )
417		fveq2 6191	. . . . . . . . . . . . . 14 |- ( i = ( M + 1 ) -> ( P ` i ) = ( P ` ( M + 1 ) ) )
418	417	oveq2d 6666	. . . . . . . . . . . . 13 |- ( i = ( M + 1 ) -> ( T + ( P ` i ) ) = ( T + ( P ` ( M + 1 ) ) ) )
419	418, 417	oveq12d 6668	. . . . . . . . . . . 12 |- ( i = ( M + 1 ) -> ( ( T + ( P ` i ) ) (AP ` K ) ( P ` i ) ) = ( ( T + ( P ` ( M + 1 ) ) ) (AP ` K ) ( P ` ( M + 1 ) ) ) )
420	418	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( i = ( M + 1 ) -> ( H ` ( T + ( P ` i ) ) ) = ( H ` ( T + ( P ` ( M + 1 ) ) ) ) )
421	420	sneqd 4189	. . . . . . . . . . . . 13 |- ( i = ( M + 1 ) -> { ( H ` ( T + ( P ` i ) ) ) } = { ( H ` ( T + ( P ` ( M + 1 ) ) ) ) } )
422	421	imaeq2d 5466	. . . . . . . . . . . 12 |- ( i = ( M + 1 ) -> ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) = ( `' H " { ( H ` ( T + ( P ` ( M + 1 ) ) ) ) } ) )
423	419, 422	sseq12d 3634	. . . . . . . . . . 11 |- ( 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 ) ) ) ) } ) ) )
424	416, 423	syl5ibrcom 237	. . . . . . . . . 10 |- ( ph -> ( i = ( M + 1 ) -> ( ( T + ( P ` i ) ) (AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) ) )
425	332, 424	jaod 395	. . . . . . . . 9 |- ( ph -> ( ( i e. ( 1 ... M ) \/ i = ( M + 1 ) ) -> ( ( T + ( P ` i ) ) (AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) ) )
426	75, 425	sylbid 230	. . . . . . . 8 |- ( ph -> ( i e. ( 1 ... ( M + 1 ) ) -> ( ( T + ( P ` i ) ) (AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) ) )
427	426	ralrimiv 2965	. . . . . . 7 |- ( ph -> A. i e. ( 1 ... ( M + 1 ) ) ( ( T + ( P ` i ) ) (AP ` K ) ( P ` i ) ) C_ ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) )
428	427	adantr 481	. . . . . 6 |- ( ( 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 ) ) ) } ) )
429	227	rexeqdv 3145	. . . . . . . . . . . 12 |- ( 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 ) ) ) ) )
430		rexun 3793	. . . . . . . . . . . . 13 |- ( 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 ) ) ) ) )
431	328	eqeq2d 2632	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( x = ( H ` ( T + ( P ` i ) ) ) <-> x = ( G ` ( B + ( E ` i ) ) ) ) )
432	431	rexbidva 3049	. . . . . . . . . . . . . 14 |- ( ph -> ( E. i e. ( 1 ... M ) x = ( H ` ( T + ( P ` i ) ) ) <-> E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) ) )
433		ovex 6678	. . . . . . . . . . . . . . . 16 |- ( M + 1 ) e. _V
434	420	eqeq2d 2632	. . . . . . . . . . . . . . . 16 |- ( i = ( M + 1 ) -> ( x = ( H ` ( T + ( P ` i ) ) ) <-> x = ( H ` ( T + ( P ` ( M + 1 ) ) ) ) ) )
435	433, 434	rexsn 4223	. . . . . . . . . . . . . . 15 |- ( E. i e. { ( M + 1 ) } x = ( H ` ( T + ( P ` i ) ) ) <-> x = ( H ` ( T + ( P ` ( M + 1 ) ) ) ) )
436	413	eqeq2d 2632	. . . . . . . . . . . . . . 15 |- ( ph -> ( x = ( H ` ( T + ( P ` ( M + 1 ) ) ) ) <-> x = ( G ` B ) ) )
437	435, 436	syl5bb 272	. . . . . . . . . . . . . 14 |- ( ph -> ( E. i e. { ( M + 1 ) } x = ( H ` ( T + ( P ` i ) ) ) <-> x = ( G ` B ) ) )
438	432, 437	orbi12d 746	. . . . . . . . . . . . 13 |- ( 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 ) ) ) )
439	430, 438	syl5bb 272	. . . . . . . . . . . 12 |- ( 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 ) ) ) )
440	429, 439	bitrd 268	. . . . . . . . . . 11 |- ( 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 ) ) ) )
441	440	adantr 481	. . . . . . . . . 10 |- ( ( 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 ) ) ) )
442	441	abbidv 2741	. . . . . . . . 9 |- ( ( 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 ) ) } )
443		eqid 2622	. . . . . . . . . 10 |- ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) = ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) )
444	443	rnmpt 5371	. . . . . . . . 9 |- ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) = { x | E. i e. ( 1 ... ( M + 1 ) ) x = ( H ` ( T + ( P ` i ) ) ) }
445	2	rnmpt 5371	. . . . . . . . . . 11 |- ran J = { x | E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) }
446		df-sn 4178	. . . . . . . . . . 11 |- { ( G ` B ) } = { x | x = ( G ` B ) }
447	445, 446	uneq12i 3765	. . . . . . . . . 10 |- ( ran J u. { ( G ` B ) } ) = ( { x | E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) } u. { x | x = ( G ` B ) } )
448		unab 3894	. . . . . . . . . 10 |- ( { 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 ) ) }
449	447, 448	eqtri 2644	. . . . . . . . 9 |- ( ran J u. { ( G ` B ) } ) = { x | ( E. i e. ( 1 ... M ) x = ( G ` ( B + ( E ` i ) ) ) \/ x = ( G ` B ) ) }
450	442, 444, 449	3eqtr4g 2681	. . . . . . . 8 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) = ( ran J u. { ( G ` B ) } ) )
451	450	fveq2d 6195	. . . . . . 7 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) ) = ( # ` ( ran J u. { ( G ` B ) } ) ) )
452		fzfi 12771	. . . . . . . . . 10 |- ( 1 ... M ) e. Fin
453		dffn4 6121	. . . . . . . . . . 11 |- ( J Fn ( 1 ... M ) <-> J : ( 1 ... M ) -onto-> ran J )
454	3, 453	mpbi 220	. . . . . . . . . 10 |- J : ( 1 ... M ) -onto-> ran J
455		fofi 8252	. . . . . . . . . 10 |- ( ( ( 1 ... M ) e. Fin /\ J : ( 1 ... M ) -onto-> ran J ) -> ran J e. Fin )
456	452, 454, 455	mp2an 708	. . . . . . . . 9 |- ran J e. Fin
457	456	a1i 11	. . . . . . . 8 |- ( ph -> ran J e. Fin )
458		fvex 6201	. . . . . . . . 9 |- ( G ` B ) e. _V
459		hashunsng 13181	. . . . . . . . 9 |- ( ( G ` B ) e. _V -> ( ( ran J e. Fin /\ -. ( G ` B ) e. ran J ) -> ( # ` ( ran J u. { ( G ` B ) } ) ) = ( ( # ` ran J ) + 1 ) ) )
460	458, 459	ax-mp 5	. . . . . . . 8 |- ( ( ran J e. Fin /\ -. ( G ` B ) e. ran J ) -> ( # ` ( ran J u. { ( G ` B ) } ) ) = ( ( # ` ran J ) + 1 ) )
461	457, 460	sylan 488	. . . . . . 7 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( # ` ( ran J u. { ( G ` B ) } ) ) = ( ( # ` ran J ) + 1 ) )
462	44	adantr 481	. . . . . . . 8 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( # ` ran J ) = M )
463	462	oveq1d 6665	. . . . . . 7 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( ( # ` ran J ) + 1 ) = ( M + 1 ) )
464	451, 461, 463	3eqtrd 2660	. . . . . 6 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) ) = ( M + 1 ) )
465	428, 464	jca 554	. . . . 5 |- ( ( 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 ) ) )
466		oveq1 6657	. . . . . . . . . 10 |- ( a = T -> ( a + ( d ` i ) ) = ( T + ( d ` i ) ) )
467	466	oveq1d 6665	. . . . . . . . 9 |- ( a = T -> ( ( a + ( d ` i ) ) (AP ` K ) ( d ` i ) ) = ( ( T + ( d ` i ) ) (AP ` K ) ( d ` i ) ) )
468	466	fveq2d 6195	. . . . . . . . . . 11 |- ( a = T -> ( H ` ( a + ( d ` i ) ) ) = ( H ` ( T + ( d ` i ) ) ) )
469	468	sneqd 4189	. . . . . . . . . 10 |- ( a = T -> { ( H ` ( a + ( d ` i ) ) ) } = { ( H ` ( T + ( d ` i ) ) ) } )
470	469	imaeq2d 5466	. . . . . . . . 9 |- ( a = T -> ( `' H " { ( H ` ( a + ( d ` i ) ) ) } ) = ( `' H " { ( H ` ( T + ( d ` i ) ) ) } ) )
471	467, 470	sseq12d 3634	. . . . . . . 8 |- ( 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 ) ) ) } ) ) )
472	471	ralbidv 2986	. . . . . . 7 |- ( 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 ) ) ) } ) ) )
473	468	mpteq2dv 4745	. . . . . . . . . 10 |- ( a = T -> ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( a + ( d ` i ) ) ) ) = ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( d ` i ) ) ) ) )
474	473	rneqd 5353	. . . . . . . . 9 |- ( a = T -> ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( a + ( d ` i ) ) ) ) = ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( d ` i ) ) ) ) )
475	474	fveq2d 6195	. . . . . . . 8 |- ( a = T -> ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( a + ( d ` i ) ) ) ) ) = ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( d ` i ) ) ) ) ) )
476	475	eqeq1d 2624	. . . . . . 7 |- ( 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 ) ) )
477	472, 476	anbi12d 747	. . . . . 6 |- ( 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 ) ) ) )
478		fveq1 6190	. . . . . . . . . . 11 |- ( d = P -> ( d ` i ) = ( P ` i ) )
479	478	oveq2d 6666	. . . . . . . . . 10 |- ( d = P -> ( T + ( d ` i ) ) = ( T + ( P ` i ) ) )
480	479, 478	oveq12d 6668	. . . . . . . . 9 |- ( d = P -> ( ( T + ( d ` i ) ) (AP ` K ) ( d ` i ) ) = ( ( T + ( P ` i ) ) (AP ` K ) ( P ` i ) ) )
481	479	fveq2d 6195	. . . . . . . . . . 11 |- ( d = P -> ( H ` ( T + ( d ` i ) ) ) = ( H ` ( T + ( P ` i ) ) ) )
482	481	sneqd 4189	. . . . . . . . . 10 |- ( d = P -> { ( H ` ( T + ( d ` i ) ) ) } = { ( H ` ( T + ( P ` i ) ) ) } )
483	482	imaeq2d 5466	. . . . . . . . 9 |- ( d = P -> ( `' H " { ( H ` ( T + ( d ` i ) ) ) } ) = ( `' H " { ( H ` ( T + ( P ` i ) ) ) } ) )
484	480, 483	sseq12d 3634	. . . . . . . 8 |- ( 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 ) ) ) } ) ) )
485	484	ralbidv 2986	. . . . . . 7 |- ( 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 ) ) ) } ) ) )
486	481	mpteq2dv 4745	. . . . . . . . . 10 |- ( d = P -> ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( d ` i ) ) ) ) = ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) )
487	486	rneqd 5353	. . . . . . . . 9 |- ( d = P -> ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( d ` i ) ) ) ) = ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) )
488	487	fveq2d 6195	. . . . . . . 8 |- ( d = P -> ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( d ` i ) ) ) ) ) = ( # ` ran ( i e. ( 1 ... ( M + 1 ) ) |-> ( H ` ( T + ( P ` i ) ) ) ) ) )
489	488	eqeq1d 2624	. . . . . . 7 |- ( 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 ) ) )
490	485, 489	anbi12d 747	. . . . . 6 |- ( 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 ) ) ) )
491	477, 490	rspc2ev 3324	. . . . 5 |- ( ( 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 ) ) )
492	48, 73, 465, 491	syl3anc 1326	. . . 4 |- ( ( 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 ) ) )
493		ovex 6678	. . . . 5 |- ( 1 ... ( W x. ( 2 x. V ) ) ) e. _V
494	10	adantr 481	. . . . . 6 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> K e. NN )
495	494	nnnn0d 11351	. . . . 5 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> K e. NN0 )
496	39	adantr 481	. . . . 5 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )
497	18	adantr 481	. . . . . 6 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> M e. NN )
498	497	peano2nnd 11037	. . . . 5 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( M + 1 ) e. NN )
499		eqid 2622	. . . . 5 |- ( 1 ... ( M + 1 ) ) = ( 1 ... ( M + 1 ) )
500	493, 495, 496, 498, 499	vdwpc 15684	. . . 4 |- ( ( 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 ) ) ) )
501	492, 500	mpbird 247	. . 3 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> <. ( M + 1 ) , K >. PolyAP H )
502	501	orcd 407	. 2 |- ( ( ph /\ -. ( G ` B ) e. ran J ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP G ) )
503	37, 502	pm2.61dan 832	1 |- ( ph -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP G ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   u. cun 3572   C_ wss 3574   (/)c0 3915   ifcif 4086   {csn 4177   <.cop 4183   class class class wbr 4653   |-> cmpt 4729   `'ccnv 5113   dom cdm 5114   ran crn 5115   "cima 5117   Fn wfn 5883   -->wf 5884   -onto->wfo 5886   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   Fincfn 7955   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   < clt 10074   <_ cle 10075   - cmin 10266   NNcn 11020   2c2 11070   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326   #chash 13117  APcvdwa 15669   MonoAP cvdwm 15670   PolyAP cvdwp 15671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-fz 12327  df-hash 13118  df-vdwap 15672  df-vdwmc 15673  df-vdwpc 15674

This theorem is referenced by:  vdwlem7  15691