Metamath Proof Explorer

Theorem vdwlem2

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

Ref Expression
Hypotheses vdwlem2.r 
|- ( ph -> R e. Fin )
vdwlem2.k 
|- ( ph -> K e. NN0 )
vdwlem2.w 
|- ( ph -> W e. NN )
vdwlem2.n 
|- ( ph -> N e. NN )
vdwlem2.f 
|- ( ph -> F : ( 1 ... M ) --> R )
vdwlem2.m 
|- ( ph -> M e. ( ZZ>= ` ( W + N ) ) )
vdwlem2.g 
|- G = ( x e. ( 1 ... W ) |-> ( F ` ( x + N ) ) )
Assertion vdwlem2 
|- ( ph -> ( K MonoAP G -> K MonoAP F ) )

Proof

Step Hyp Ref Expression
1 vdwlem2.r 
 |-  ( ph -> R e. Fin )
2 vdwlem2.k 
 |-  ( ph -> K e. NN0 )
3 vdwlem2.w 
 |-  ( ph -> W e. NN )
4 vdwlem2.n 
 |-  ( ph -> N e. NN )
5 vdwlem2.f 
 |-  ( ph -> F : ( 1 ... M ) --> R )
6 vdwlem2.m 
 |-  ( ph -> M e. ( ZZ>= ` ( W + N ) ) )
7 vdwlem2.g 
 |-  G = ( x e. ( 1 ... W ) |-> ( F ` ( x + N ) ) )
8 id 
 |-  ( a e. NN -> a e. NN )
9 nnaddcl 
 |-  ( ( a e. NN /\ N e. NN ) -> ( a + N ) e. NN )
10 8 4 9 syl2anr 
 |-  ( ( ph /\ a e. NN ) -> ( a + N ) e. NN )
11 simpllr 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> a e. NN )
12 11 nncnd 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> a e. CC )
13 4 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> N e. NN )
14 13 nncnd 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> N e. CC )
15 elfznn0 
 |-  ( m e. ( 0 ... ( K - 1 ) ) -> m e. NN0 )
16 15 adantl 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> m e. NN0 )
17 16 nn0cnd 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> m e. CC )
18 simplrl 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> d e. NN )
19 18 nncnd 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> d e. CC )
20 17 19 mulcld 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. d ) e. CC )
21 12 14 20 add32d 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( a + N ) + ( m x. d ) ) = ( ( a + ( m x. d ) ) + N ) )
22 oveq1 
 |-  ( x = ( a + ( m x. d ) ) -> ( x + N ) = ( ( a + ( m x. d ) ) + N ) )
23 22 eleq1d 
 |-  ( x = ( a + ( m x. d ) ) -> ( ( x + N ) e. ( 1 ... M ) <-> ( ( a + ( m x. d ) ) + N ) e. ( 1 ... M ) ) )
24 elfznn 
 |-  ( x e. ( 1 ... W ) -> x e. NN )
25 nnaddcl 
 |-  ( ( x e. NN /\ N e. NN ) -> ( x + N ) e. NN )
26 24 4 25 syl2anr 
 |-  ( ( ph /\ x e. ( 1 ... W ) ) -> ( x + N ) e. NN )
27 nnuz 
 |-  NN = ( ZZ>= ` 1 )
28 26 27 eleqtrdi 
 |-  ( ( ph /\ x e. ( 1 ... W ) ) -> ( x + N ) e. ( ZZ>= ` 1 ) )
29 elfzuz3 
 |-  ( x e. ( 1 ... W ) -> W e. ( ZZ>= ` x ) )
30 4 nnzd 
 |-  ( ph -> N e. ZZ )
31 eluzadd 
 |-  ( ( W e. ( ZZ>= ` x ) /\ N e. ZZ ) -> ( W + N ) e. ( ZZ>= ` ( x + N ) ) )
32 29 30 31 syl2anr 
 |-  ( ( ph /\ x e. ( 1 ... W ) ) -> ( W + N ) e. ( ZZ>= ` ( x + N ) ) )
33 uztrn 
 |-  ( ( M e. ( ZZ>= ` ( W + N ) ) /\ ( W + N ) e. ( ZZ>= ` ( x + N ) ) ) -> M e. ( ZZ>= ` ( x + N ) ) )
34 6 32 33 syl2an2r 
 |-  ( ( ph /\ x e. ( 1 ... W ) ) -> M e. ( ZZ>= ` ( x + N ) ) )
35 elfzuzb 
 |-  ( ( x + N ) e. ( 1 ... M ) <-> ( ( x + N ) e. ( ZZ>= ` 1 ) /\ M e. ( ZZ>= ` ( x + N ) ) ) )
36 28 34 35 sylanbrc 
 |-  ( ( ph /\ x e. ( 1 ... W ) ) -> ( x + N ) e. ( 1 ... M ) )
37 36 ralrimiva 
 |-  ( ph -> A. x e. ( 1 ... W ) ( x + N ) e. ( 1 ... M ) )
38 37 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> A. x e. ( 1 ... W ) ( x + N ) e. ( 1 ... M ) )
39 simplrr 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( a ( AP ` K ) d ) C_ ( `' G " { c } ) )
40 eqid 
 |-  ( a + ( m x. d ) ) = ( a + ( m x. d ) )
41 oveq1 
 |-  ( n = m -> ( n x. d ) = ( m x. d ) )
42 41 oveq2d 
 |-  ( n = m -> ( a + ( n x. d ) ) = ( a + ( m x. d ) ) )
43 42 rspceeqv 
 |-  ( ( m e. ( 0 ... ( K - 1 ) ) /\ ( a + ( m x. d ) ) = ( a + ( m x. d ) ) ) -> E. n e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) = ( a + ( n x. d ) ) )
44 40 43 mpan2 
 |-  ( m e. ( 0 ... ( K - 1 ) ) -> E. n e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) = ( a + ( n x. d ) ) )
45 44 adantl 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> E. n e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) = ( a + ( n x. d ) ) )
46 2 ad2antrr 
 |-  ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) -> K e. NN0 )
47 46 adantr 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> K e. NN0 )
48 vdwapval 
 |-  ( ( K e. NN0 /\ a e. NN /\ d e. NN ) -> ( ( a + ( m x. d ) ) e. ( a ( AP ` K ) d ) <-> E. n e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) = ( a + ( n x. d ) ) ) )
49 47 11 18 48 syl3anc 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( a + ( m x. d ) ) e. ( a ( AP ` K ) d ) <-> E. n e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) = ( a + ( n x. d ) ) ) )
50 45 49 mpbird 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( a + ( m x. d ) ) e. ( a ( AP ` K ) d ) )
51 39 50 sseldd 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( a + ( m x. d ) ) e. ( `' G " { c } ) )
52 5 ffvelrnda 
 |-  ( ( ph /\ ( x + N ) e. ( 1 ... M ) ) -> ( F ` ( x + N ) ) e. R )
53 36 52 syldan 
 |-  ( ( ph /\ x e. ( 1 ... W ) ) -> ( F ` ( x + N ) ) e. R )
54 53 7 fmptd 
 |-  ( ph -> G : ( 1 ... W ) --> R )
55 54 ffnd 
 |-  ( ph -> G Fn ( 1 ... W ) )
56 55 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> G Fn ( 1 ... W ) )
57 fniniseg 
 |-  ( G Fn ( 1 ... W ) -> ( ( a + ( m x. d ) ) e. ( `' G " { c } ) <-> ( ( a + ( m x. d ) ) e. ( 1 ... W ) /\ ( G ` ( a + ( m x. d ) ) ) = c ) ) )
58 56 57 syl 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( a + ( m x. d ) ) e. ( `' G " { c } ) <-> ( ( a + ( m x. d ) ) e. ( 1 ... W ) /\ ( G ` ( a + ( m x. d ) ) ) = c ) ) )
59 51 58 mpbid 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( a + ( m x. d ) ) e. ( 1 ... W ) /\ ( G ` ( a + ( m x. d ) ) ) = c ) )
60 59 simpld 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( a + ( m x. d ) ) e. ( 1 ... W ) )
61 23 38 60 rspcdva 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( a + ( m x. d ) ) + N ) e. ( 1 ... M ) )
62 21 61 eqeltrd 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( a + N ) + ( m x. d ) ) e. ( 1 ... M ) )
63 21 fveq2d 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( F ` ( ( a + N ) + ( m x. d ) ) ) = ( F ` ( ( a + ( m x. d ) ) + N ) ) )
64 22 fveq2d 
 |-  ( x = ( a + ( m x. d ) ) -> ( F ` ( x + N ) ) = ( F ` ( ( a + ( m x. d ) ) + N ) ) )
65 fvex 
 |-  ( F ` ( ( a + ( m x. d ) ) + N ) ) e. _V
66 64 7 65 fvmpt 
 |-  ( ( a + ( m x. d ) ) e. ( 1 ... W ) -> ( G ` ( a + ( m x. d ) ) ) = ( F ` ( ( a + ( m x. d ) ) + N ) ) )
67 60 66 syl 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( G ` ( a + ( m x. d ) ) ) = ( F ` ( ( a + ( m x. d ) ) + N ) ) )
68 59 simprd 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( G ` ( a + ( m x. d ) ) ) = c )
69 63 67 68 3eqtr2d 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( F ` ( ( a + N ) + ( m x. d ) ) ) = c )
70 62 69 jca 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( a + N ) + ( m x. d ) ) e. ( 1 ... M ) /\ ( F ` ( ( a + N ) + ( m x. d ) ) ) = c ) )
71 eleq1 
 |-  ( x = ( ( a + N ) + ( m x. d ) ) -> ( x e. ( 1 ... M ) <-> ( ( a + N ) + ( m x. d ) ) e. ( 1 ... M ) ) )
72 fveqeq2 
 |-  ( x = ( ( a + N ) + ( m x. d ) ) -> ( ( F ` x ) = c <-> ( F ` ( ( a + N ) + ( m x. d ) ) ) = c ) )
73 71 72 anbi12d 
 |-  ( x = ( ( a + N ) + ( m x. d ) ) -> ( ( x e. ( 1 ... M ) /\ ( F ` x ) = c ) <-> ( ( ( a + N ) + ( m x. d ) ) e. ( 1 ... M ) /\ ( F ` ( ( a + N ) + ( m x. d ) ) ) = c ) ) )
74 70 73 syl5ibrcom 
 |-  ( ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( x = ( ( a + N ) + ( m x. d ) ) -> ( x e. ( 1 ... M ) /\ ( F ` x ) = c ) ) )
75 74 rexlimdva 
 |-  ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) -> ( E. m e. ( 0 ... ( K - 1 ) ) x = ( ( a + N ) + ( m x. d ) ) -> ( x e. ( 1 ... M ) /\ ( F ` x ) = c ) ) )
76 10 adantr 
 |-  ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) -> ( a + N ) e. NN )
77 simprl 
 |-  ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) -> d e. NN )
78 vdwapval 
 |-  ( ( K e. NN0 /\ ( a + N ) e. NN /\ d e. NN ) -> ( x e. ( ( a + N ) ( AP ` K ) d ) <-> E. m e. ( 0 ... ( K - 1 ) ) x = ( ( a + N ) + ( m x. d ) ) ) )
79 46 76 77 78 syl3anc 
 |-  ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) -> ( x e. ( ( a + N ) ( AP ` K ) d ) <-> E. m e. ( 0 ... ( K - 1 ) ) x = ( ( a + N ) + ( m x. d ) ) ) )
80 5 ffnd 
 |-  ( ph -> F Fn ( 1 ... M ) )
81 80 ad2antrr 
 |-  ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) -> F Fn ( 1 ... M ) )
82 fniniseg 
 |-  ( F Fn ( 1 ... M ) -> ( x e. ( `' F " { c } ) <-> ( x e. ( 1 ... M ) /\ ( F ` x ) = c ) ) )
83 81 82 syl 
 |-  ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) -> ( x e. ( `' F " { c } ) <-> ( x e. ( 1 ... M ) /\ ( F ` x ) = c ) ) )
84 75 79 83 3imtr4d 
 |-  ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) -> ( x e. ( ( a + N ) ( AP ` K ) d ) -> x e. ( `' F " { c } ) ) )
85 84 ssrdv 
 |-  ( ( ( ph /\ a e. NN ) /\ ( d e. NN /\ ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) ) -> ( ( a + N ) ( AP ` K ) d ) C_ ( `' F " { c } ) )
86 85 expr 
 |-  ( ( ( ph /\ a e. NN ) /\ d e. NN ) -> ( ( a ( AP ` K ) d ) C_ ( `' G " { c } ) -> ( ( a + N ) ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
87 86 reximdva 
 |-  ( ( ph /\ a e. NN ) -> ( E. d e. NN ( a ( AP ` K ) d ) C_ ( `' G " { c } ) -> E. d e. NN ( ( a + N ) ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
88 oveq1 
 |-  ( b = ( a + N ) -> ( b ( AP ` K ) d ) = ( ( a + N ) ( AP ` K ) d ) )
89 88 sseq1d 
 |-  ( b = ( a + N ) -> ( ( b ( AP ` K ) d ) C_ ( `' F " { c } ) <-> ( ( a + N ) ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
90 89 rexbidv 
 |-  ( b = ( a + N ) -> ( E. d e. NN ( b ( AP ` K ) d ) C_ ( `' F " { c } ) <-> E. d e. NN ( ( a + N ) ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
91 90 rspcev 
 |-  ( ( ( a + N ) e. NN /\ E. d e. NN ( ( a + N ) ( AP ` K ) d ) C_ ( `' F " { c } ) ) -> E. b e. NN E. d e. NN ( b ( AP ` K ) d ) C_ ( `' F " { c } ) )
92 10 87 91 syl6an 
 |-  ( ( ph /\ a e. NN ) -> ( E. d e. NN ( a ( AP ` K ) d ) C_ ( `' G " { c } ) -> E. b e. NN E. d e. NN ( b ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
93 92 rexlimdva 
 |-  ( ph -> ( E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' G " { c } ) -> E. b e. NN E. d e. NN ( b ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
94 93 eximdv 
 |-  ( ph -> ( E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' G " { c } ) -> E. c E. b e. NN E. d e. NN ( b ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
95 ovex 
 |-  ( 1 ... W ) e. _V
96 95 2 54 vdwmc 
 |-  ( ph -> ( K MonoAP G <-> E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' G " { c } ) ) )
97 ovex 
 |-  ( 1 ... M ) e. _V
98 97 2 5 vdwmc 
 |-  ( ph -> ( K MonoAP F <-> E. c E. b e. NN E. d e. NN ( b ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
99 94 96 98 3imtr4d 
 |-  ( ph -> ( K MonoAP G -> K MonoAP F ) )