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 ( 𝑖𝐽 ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑𝑖 ) ) ) ) ) = 𝑀 ) ) )