Metamath Proof Explorer

Theorem vdwnnlem1

Description: Corollary of vdw , and lemma for vdwnn . If F is a coloring of the integers, then there are arbitrarily long monochromatic APs in F . (Contributed by Mario Carneiro, 13-Sep-2014)

Ref Expression
Assertion vdwnnlem1 
|- ( ( R e. Fin /\ F : NN --> R /\ K e. NN0 ) -> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )

Proof

Step Hyp Ref Expression
1 vdw 
 |-  ( ( R e. Fin /\ K e. NN0 ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) )
2 1 3adant2 
 |-  ( ( R e. Fin /\ F : NN --> R /\ K e. NN0 ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) )
3 simpl2 
 |-  ( ( ( R e. Fin /\ F : NN --> R /\ K e. NN0 ) /\ n e. NN ) -> F : NN --> R )
4 fz1ssnn 
 |-  ( 1 ... n ) C_ NN
5 fssres 
 |-  ( ( F : NN --> R /\ ( 1 ... n ) C_ NN ) -> ( F |` ( 1 ... n ) ) : ( 1 ... n ) --> R )
6 3 4 5 sylancl 
 |-  ( ( ( R e. Fin /\ F : NN --> R /\ K e. NN0 ) /\ n e. NN ) -> ( F |` ( 1 ... n ) ) : ( 1 ... n ) --> R )
7 simpl1 
 |-  ( ( ( R e. Fin /\ F : NN --> R /\ K e. NN0 ) /\ n e. NN ) -> R e. Fin )
8 ovex 
 |-  ( 1 ... n ) e. _V
9 elmapg 
 |-  ( ( R e. Fin /\ ( 1 ... n ) e. _V ) -> ( ( F |` ( 1 ... n ) ) e. ( R ^m ( 1 ... n ) ) <-> ( F |` ( 1 ... n ) ) : ( 1 ... n ) --> R ) )
10 7 8 9 sylancl 
 |-  ( ( ( R e. Fin /\ F : NN --> R /\ K e. NN0 ) /\ n e. NN ) -> ( ( F |` ( 1 ... n ) ) e. ( R ^m ( 1 ... n ) ) <-> ( F |` ( 1 ... n ) ) : ( 1 ... n ) --> R ) )
11 6 10 mpbird 
 |-  ( ( ( R e. Fin /\ F : NN --> R /\ K e. NN0 ) /\ n e. NN ) -> ( F |` ( 1 ... n ) ) e. ( R ^m ( 1 ... n ) ) )
12 cnveq 
 |-  ( f = ( F |` ( 1 ... n ) ) -> `' f = `' ( F |` ( 1 ... n ) ) )
13 12 imaeq1d 
 |-  ( f = ( F |` ( 1 ... n ) ) -> ( `' f " { c } ) = ( `' ( F |` ( 1 ... n ) ) " { c } ) )
14 13 eleq2d 
 |-  ( f = ( F |` ( 1 ... n ) ) -> ( ( a + ( m x. d ) ) e. ( `' f " { c } ) <-> ( a + ( m x. d ) ) e. ( `' ( F |` ( 1 ... n ) ) " { c } ) ) )
15 14 ralbidv 
 |-  ( f = ( F |` ( 1 ... n ) ) -> ( A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) <-> A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' ( F |` ( 1 ... n ) ) " { c } ) ) )
16 15 2rexbidv 
 |-  ( f = ( F |` ( 1 ... n ) ) -> ( E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) <-> E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' ( F |` ( 1 ... n ) ) " { c } ) ) )
17 16 rexbidv 
 |-  ( f = ( F |` ( 1 ... n ) ) -> ( E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) <-> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' ( F |` ( 1 ... n ) ) " { c } ) ) )
18 17 rspcv 
 |-  ( ( F |` ( 1 ... n ) ) e. ( R ^m ( 1 ... n ) ) -> ( A. f e. ( R ^m ( 1 ... n ) ) E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) -> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' ( F |` ( 1 ... n ) ) " { c } ) ) )
19 11 18 syl 
 |-  ( ( ( R e. Fin /\ F : NN --> R /\ K e. NN0 ) /\ n e. NN ) -> ( A. f e. ( R ^m ( 1 ... n ) ) E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) -> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' ( F |` ( 1 ... n ) ) " { c } ) ) )
20 resss 
 |-  ( F |` ( 1 ... n ) ) C_ F
21 cnvss 
 |-  ( ( F |` ( 1 ... n ) ) C_ F -> `' ( F |` ( 1 ... n ) ) C_ `' F )
22 imass1 
 |-  ( `' ( F |` ( 1 ... n ) ) C_ `' F -> ( `' ( F |` ( 1 ... n ) ) " { c } ) C_ ( `' F " { c } ) )
23 20 21 22 mp2b 
 |-  ( `' ( F |` ( 1 ... n ) ) " { c } ) C_ ( `' F " { c } )
24 23 sseli 
 |-  ( ( a + ( m x. d ) ) e. ( `' ( F |` ( 1 ... n ) ) " { c } ) -> ( a + ( m x. d ) ) e. ( `' F " { c } ) )
25 24 ralimi 
 |-  ( A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' ( F |` ( 1 ... n ) ) " { c } ) -> A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )
26 25 reximi 
 |-  ( E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' ( F |` ( 1 ... n ) ) " { c } ) -> E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )
27 26 reximi 
 |-  ( E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' ( F |` ( 1 ... n ) ) " { c } ) -> E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )
28 27 reximi 
 |-  ( E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' ( F |` ( 1 ... n ) ) " { c } ) -> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )
29 19 28 syl6 
 |-  ( ( ( R e. Fin /\ F : NN --> R /\ K e. NN0 ) /\ n e. NN ) -> ( A. f e. ( R ^m ( 1 ... n ) ) E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) -> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
30 29 rexlimdva 
 |-  ( ( R e. Fin /\ F : NN --> R /\ K e. NN0 ) -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) -> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
31 2 30 mpd 
 |-  ( ( R e. Fin /\ F : NN --> R /\ K e. NN0 ) -> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )