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 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )