Metamath Proof Explorer

Theorem vdwpc

Description: The predicate " The coloring F contains a polychromatic M -tuple of AP's of length K ". A polychromatic M -tuple of AP's is a set of AP's with the same base point but different step lengths, such that each individual AP is monochromatic, but the AP's all have mutually distinct colors. (The common basepoint is not required to have the same color as any of the AP's.) (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdwmc.1 ⊢ 𝑋 ∈ V
vdwmc.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
vdwmc.3 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑅 )
vdwpc.4 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
vdwpc.5 ⊢ 𝐽 = ( 1 ... 𝑀 )
Assertion vdwpc ( 𝜑 → ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝐹 ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m 𝐽 ) ( ∀ 𝑖 ∈ 𝐽 ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ 𝐽 ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 vdwmc.1 ⊢ 𝑋 ∈ V
2 vdwmc.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 vdwmc.3 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑅 )
4 vdwpc.4 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
5 vdwpc.5 ⊢ 𝐽 = ( 1 ... 𝑀 )
6 fex ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑅 ∧ 𝑋 ∈ V ) → 𝐹 ∈ V )
7 3 1 6 sylancl ⊢ ( 𝜑 → 𝐹 ∈ V )
8 df-br ⊢ ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝐹 ↔ ⟨ ⟨ 𝑀 , 𝐾 ⟩ , 𝐹 ⟩ ∈ PolyAP )
9 df-vdwpc ⊢ PolyAP = { ⟨ ⟨ 𝑚 , 𝑘 ⟩ , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑚 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚 ) }
10 9 eleq2i ⊢ ( ⟨ ⟨ 𝑀 , 𝐾 ⟩ , 𝐹 ⟩ ∈ PolyAP ↔ ⟨ ⟨ 𝑀 , 𝐾 ⟩ , 𝐹 ⟩ ∈ { ⟨ ⟨ 𝑚 , 𝑘 ⟩ , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑚 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚 ) } )
11 8 10 bitri ⊢ ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝐹 ↔ ⟨ ⟨ 𝑀 , 𝐾 ⟩ , 𝐹 ⟩ ∈ { ⟨ ⟨ 𝑚 , 𝑘 ⟩ , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑚 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚 ) } )
12 simp1 ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → 𝑚 = 𝑀 )
13 12 oveq2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( 1 ... 𝑚 ) = ( 1 ... 𝑀 ) )
14 13 5 eqtr4di ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( 1 ... 𝑚 ) = 𝐽 )
15 14 oveq2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( ℕ ↑m ( 1 ... 𝑚 ) ) = ( ℕ ↑m 𝐽 ) )
16 simp2 ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → 𝑘 = 𝐾 )
17 16 fveq2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( AP ‘ 𝑘 ) = ( AP ‘ 𝐾 ) )
18 17 oveqd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) = ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) )
19 simp3 ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
20 19 cnveqd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ◡ 𝑓 = ◡ 𝐹 )
21 19 fveq1d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) )
22 21 sneqd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } = { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } )
23 20 22 imaeq12d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) )
24 18 23 sseq12d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ↔ ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) )
25 14 24 raleqbidv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ↔ ∀ 𝑖 ∈ 𝐽 ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) )
26 14 21 mpteq12dv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ 𝐽 ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) )
27 26 rneqd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) = ran ( 𝑖 ∈ 𝐽 ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) )
28 27 fveq2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = ( ♯ ‘ ran ( 𝑖 ∈ 𝐽 ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) )
29 28 12 eqeq12d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚 ↔ ( ♯ ‘ ran ( 𝑖 ∈ 𝐽 ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) )
30 25 29 anbi12d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚 ) ↔ ( ∀ 𝑖 ∈ 𝐽 ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ 𝐽 ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) )
31 15 30 rexeqbidv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑚 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚 ) ↔ ∃ 𝑑 ∈ ( ℕ ↑m 𝐽 ) ( ∀ 𝑖 ∈ 𝐽 ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ 𝐽 ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) )
32 31 rexbidv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑚 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚 ) ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m 𝐽 ) ( ∀ 𝑖 ∈ 𝐽 ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ 𝐽 ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) )
33 32 eloprabga ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝐹 ∈ V ) → ( ⟨ ⟨ 𝑀 , 𝐾 ⟩ , 𝐹 ⟩ ∈ { ⟨ ⟨ 𝑚 , 𝑘 ⟩ , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑚 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚 ) } ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m 𝐽 ) ( ∀ 𝑖 ∈ 𝐽 ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ 𝐽 ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) )
34 11 33 syl5bb ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝐹 ∈ V ) → ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝐹 ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m 𝐽 ) ( ∀ 𝑖 ∈ 𝐽 ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ 𝐽 ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) )
35 4 2 7 34 syl3anc ⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝐹 ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m 𝐽 ) ( ∀ 𝑖 ∈ 𝐽 ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ 𝐽 ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) )