Metamath Proof Explorer

Theorem vdwlem7

Description: Lemma for vdw . (Contributed by Mario Carneiro, 12-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 } ) )
Assertion vdwlem7 
|- ( ph -> ( <. M , K >. PolyAP G -> ( <. ( 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 ovex 
 |-  ( 1 ... W ) e. _V
13 2nn0 
 |-  2 e. NN0
14 eluznn0 
 |-  ( ( 2 e. NN0 /\ K e. ( ZZ>= ` 2 ) ) -> K e. NN0 )
15 13 8 14 sylancr 
 |-  ( ph -> K e. NN0 )
16 eqid 
 |-  ( 1 ... M ) = ( 1 ... M )
17 12 15 7 6 16 vdwpc 
 |-  ( ph -> ( <. M , K >. PolyAP G <-> E. a e. NN E. d e. ( NN ^m ( 1 ... M ) ) ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) )
18 1 ad2antrr 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> V e. NN )
19 2 ad2antrr 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> W e. NN )
20 3 ad2antrr 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> R e. Fin )
21 4 ad2antrr 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )
22 6 ad2antrr 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> M e. NN )
23 7 ad2antrr 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> G : ( 1 ... W ) --> R )
24 8 ad2antrr 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> K e. ( ZZ>= ` 2 ) )
25 9 ad2antrr 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> A e. NN )
26 10 ad2antrr 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> D e. NN )
27 11 ad2antrr 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> ( A ( AP ` K ) D ) C_ ( `' F " { G } ) )
28 simplrl 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> a e. NN )
29 simplrr 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> d e. ( NN ^m ( 1 ... M ) ) )
30 nnex 
 |-  NN e. _V
31 ovex 
 |-  ( 1 ... M ) e. _V
32 30 31 elmap 
 |-  ( d e. ( NN ^m ( 1 ... M ) ) <-> d : ( 1 ... M ) --> NN )
33 29 32 sylib 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> d : ( 1 ... M ) --> NN )
34 simprl 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) )
35 fveq2 
 |-  ( i = k -> ( d ` i ) = ( d ` k ) )
36 35 oveq2d 
 |-  ( i = k -> ( a + ( d ` i ) ) = ( a + ( d ` k ) ) )
37 36 35 oveq12d 
 |-  ( i = k -> ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) = ( ( a + ( d ` k ) ) ( AP ` K ) ( d ` k ) ) )
38 36 fveq2d 
 |-  ( i = k -> ( G ` ( a + ( d ` i ) ) ) = ( G ` ( a + ( d ` k ) ) ) )
39 38 sneqd 
 |-  ( i = k -> { ( G ` ( a + ( d ` i ) ) ) } = { ( G ` ( a + ( d ` k ) ) ) } )
40 39 imaeq2d 
 |-  ( i = k -> ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) = ( `' G " { ( G ` ( a + ( d ` k ) ) ) } ) )
41 37 40 sseq12d 
 |-  ( i = k -> ( ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) <-> ( ( a + ( d ` k ) ) ( AP ` K ) ( d ` k ) ) C_ ( `' G " { ( G ` ( a + ( d ` k ) ) ) } ) ) )
42 41 cbvralvw 
 |-  ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) <-> A. k e. ( 1 ... M ) ( ( a + ( d ` k ) ) ( AP ` K ) ( d ` k ) ) C_ ( `' G " { ( G ` ( a + ( d ` k ) ) ) } ) )
43 34 42 sylib 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> A. k e. ( 1 ... M ) ( ( a + ( d ` k ) ) ( AP ` K ) ( d ` k ) ) C_ ( `' G " { ( G ` ( a + ( d ` k ) ) ) } ) )
44 38 cbvmptv 
 |-  ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) = ( k e. ( 1 ... M ) |-> ( G ` ( a + ( d ` k ) ) ) )
45 simprr 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M )
46 eqid 
 |-  ( a + ( W x. ( ( A + ( V - D ) ) - 1 ) ) ) = ( a + ( W x. ( ( A + ( V - D ) ) - 1 ) ) )
47 eqid 
 |-  ( j e. ( 1 ... ( M + 1 ) ) |-> ( if ( j = ( M + 1 ) , 0 , ( d ` j ) ) + ( W x. D ) ) ) = ( j e. ( 1 ... ( M + 1 ) ) |-> ( if ( j = ( M + 1 ) , 0 , ( d ` j ) ) + ( W x. D ) ) )
48 18 19 20 21 5 22 23 24 25 26 27 28 33 43 44 45 46 47 vdwlem6 
 |-  ( ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) /\ ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP G ) )
49 48 ex 
 |-  ( ( ph /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... M ) ) ) ) -> ( ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP G ) ) )
50 49 rexlimdvva 
 |-  ( ph -> ( E. a e. NN E. d e. ( NN ^m ( 1 ... M ) ) ( A. i e. ( 1 ... M ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' G " { ( G ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... M ) |-> ( G ` ( a + ( d ` i ) ) ) ) ) = M ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP G ) ) )
51 17 50 sylbid 
 |-  ( ph -> ( <. M , K >. PolyAP G -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP G ) ) )