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 ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ∧ 𝐾 ∈ ℕ0 ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )

Proof

Step Hyp Ref Expression
1 vdw ⊢ ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) )
2 1 3adant2 ⊢ ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ∧ 𝐾 ∈ ℕ0 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) )
3 simpl2 ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → 𝐹 : ℕ ⟶ 𝑅 )
4 fz1ssnn ⊢ ( 1 ... 𝑛 ) ⊆ ℕ
5 fssres ⊢ ( ( 𝐹 : ℕ ⟶ 𝑅 ∧ ( 1 ... 𝑛 ) ⊆ ℕ ) → ( 𝐹 ↾ ( 1 ... 𝑛 ) ) : ( 1 ... 𝑛 ) ⟶ 𝑅 )
6 3 4 5 sylancl ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ↾ ( 1 ... 𝑛 ) ) : ( 1 ... 𝑛 ) ⟶ 𝑅 )
7 simpl1 ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → 𝑅 ∈ Fin )
8 ovex ⊢ ( 1 ... 𝑛 ) ∈ V
9 elmapg ⊢ ( ( 𝑅 ∈ Fin ∧ ( 1 ... 𝑛 ) ∈ V ) → ( ( 𝐹 ↾ ( 1 ... 𝑛 ) ) ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ↔ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) : ( 1 ... 𝑛 ) ⟶ 𝑅 ) )
10 7 8 9 sylancl ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ↾ ( 1 ... 𝑛 ) ) ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ↔ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) : ( 1 ... 𝑛 ) ⟶ 𝑅 ) )
11 6 10 mpbird ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ↾ ( 1 ... 𝑛 ) ) ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) )
12 cnveq ⊢ ( 𝑓 = ( 𝐹 ↾ ( 1 ... 𝑛 ) ) → ◡ 𝑓 = ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) )
13 12 imaeq1d ⊢ ( 𝑓 = ( 𝐹 ↾ ( 1 ... 𝑛 ) ) → ( ◡ 𝑓 “ { 𝑐 } ) = ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) “ { 𝑐 } ) )
14 13 eleq2d ⊢ ( 𝑓 = ( 𝐹 ↾ ( 1 ... 𝑛 ) ) → ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) “ { 𝑐 } ) ) )
15 14 ralbidv ⊢ ( 𝑓 = ( 𝐹 ↾ ( 1 ... 𝑛 ) ) → ( ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) “ { 𝑐 } ) ) )
16 15 2rexbidv ⊢ ( 𝑓 = ( 𝐹 ↾ ( 1 ... 𝑛 ) ) → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) “ { 𝑐 } ) ) )
17 16 rexbidv ⊢ ( 𝑓 = ( 𝐹 ↾ ( 1 ... 𝑛 ) ) → ( ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) “ { 𝑐 } ) ) )
18 17 rspcv ⊢ ( ( 𝐹 ↾ ( 1 ... 𝑛 ) ) ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) “ { 𝑐 } ) ) )
19 11 18 syl ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) “ { 𝑐 } ) ) )
20 resss ⊢ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) ⊆ 𝐹
21 cnvss ⊢ ( ( 𝐹 ↾ ( 1 ... 𝑛 ) ) ⊆ 𝐹 → ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) ⊆ ◡ 𝐹 )
22 imass1 ⊢ ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) ⊆ ◡ 𝐹 → ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) “ { 𝑐 } ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
23 20 21 22 mp2b ⊢ ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) “ { 𝑐 } ) ⊆ ( ◡ 𝐹 “ { 𝑐 } )
24 23 sseli ⊢ ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) “ { 𝑐 } ) → ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )
25 24 ralimi ⊢ ( ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) “ { 𝑐 } ) → ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )
26 25 reximi ⊢ ( ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) “ { 𝑐 } ) → ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )
27 26 reximi ⊢ ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) “ { 𝑐 } ) → ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )
28 27 reximi ⊢ ( ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ ( 𝐹 ↾ ( 1 ... 𝑛 ) ) “ { 𝑐 } ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )
29 19 28 syl6 ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
30 29 rexlimdva ⊢ ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ∧ 𝐾 ∈ ℕ0 ) → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
31 2 30 mpd ⊢ ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ∧ 𝐾 ∈ ℕ0 ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )