# 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 ${⊢}{X}\in \mathrm{V}$
vdwmc.2 ${⊢}{\phi }\to {K}\in {ℕ}_{0}$
vdwmc.3 ${⊢}{\phi }\to {F}:{X}⟶{R}$
vdwpc.4 ${⊢}{\phi }\to {M}\in ℕ$
vdwpc.5 ${⊢}{J}=\left(1\dots {M}\right)$
Assertion vdwpc ${⊢}{\phi }\to \left(⟨{M},{K}⟩\mathrm{PolyAP}{F}↔\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in \left({ℕ}^{{J}}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({K}\right){d}\left({i}\right)\subseteq {{F}}^{-1}\left[\left\{{F}\left({a}+{d}\left({i}\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left({i}\in {J}⟼{F}\left({a}+{d}\left({i}\right)\right)\right)\right|={M}\right)\right)$

### Proof

Step Hyp Ref Expression
1 vdwmc.1 ${⊢}{X}\in \mathrm{V}$
2 vdwmc.2 ${⊢}{\phi }\to {K}\in {ℕ}_{0}$
3 vdwmc.3 ${⊢}{\phi }\to {F}:{X}⟶{R}$
4 vdwpc.4 ${⊢}{\phi }\to {M}\in ℕ$
5 vdwpc.5 ${⊢}{J}=\left(1\dots {M}\right)$
6 fex ${⊢}\left({F}:{X}⟶{R}\wedge {X}\in \mathrm{V}\right)\to {F}\in \mathrm{V}$
7 3 1 6 sylancl ${⊢}{\phi }\to {F}\in \mathrm{V}$
8 df-br ${⊢}⟨{M},{K}⟩\mathrm{PolyAP}{F}↔⟨⟨{M},{K}⟩,{F}⟩\in \mathrm{PolyAP}$
9 df-vdwpc ${⊢}\mathrm{PolyAP}=\left\{⟨⟨{m},{k}⟩,{f}⟩|\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in \left({ℕ}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({k}\right){d}\left({i}\right)\subseteq {{f}}^{-1}\left[\left\{{f}\left({a}+{d}\left({i}\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left({i}\in \left(1\dots {m}\right)⟼{f}\left({a}+{d}\left({i}\right)\right)\right)\right|={m}\right)\right\}$
10 9 eleq2i ${⊢}⟨⟨{M},{K}⟩,{F}⟩\in \mathrm{PolyAP}↔⟨⟨{M},{K}⟩,{F}⟩\in \left\{⟨⟨{m},{k}⟩,{f}⟩|\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in \left({ℕ}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({k}\right){d}\left({i}\right)\subseteq {{f}}^{-1}\left[\left\{{f}\left({a}+{d}\left({i}\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left({i}\in \left(1\dots {m}\right)⟼{f}\left({a}+{d}\left({i}\right)\right)\right)\right|={m}\right)\right\}$
11 8 10 bitri ${⊢}⟨{M},{K}⟩\mathrm{PolyAP}{F}↔⟨⟨{M},{K}⟩,{F}⟩\in \left\{⟨⟨{m},{k}⟩,{f}⟩|\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in \left({ℕ}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({k}\right){d}\left({i}\right)\subseteq {{f}}^{-1}\left[\left\{{f}\left({a}+{d}\left({i}\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left({i}\in \left(1\dots {m}\right)⟼{f}\left({a}+{d}\left({i}\right)\right)\right)\right|={m}\right)\right\}$
12 simp1 ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to {m}={M}$
13 12 oveq2d ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to \left(1\dots {m}\right)=\left(1\dots {M}\right)$
14 13 5 syl6eqr ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to \left(1\dots {m}\right)={J}$
15 14 oveq2d ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to {ℕ}^{\left(1\dots {m}\right)}={ℕ}^{{J}}$
16 simp2 ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to {k}={K}$
17 16 fveq2d ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to \mathrm{AP}\left({k}\right)=\mathrm{AP}\left({K}\right)$
18 17 oveqd ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to \left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({k}\right){d}\left({i}\right)=\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({K}\right){d}\left({i}\right)$
19 simp3 ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to {f}={F}$
20 19 cnveqd ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to {{f}}^{-1}={{F}}^{-1}$
21 19 fveq1d ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to {f}\left({a}+{d}\left({i}\right)\right)={F}\left({a}+{d}\left({i}\right)\right)$
22 21 sneqd ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to \left\{{f}\left({a}+{d}\left({i}\right)\right)\right\}=\left\{{F}\left({a}+{d}\left({i}\right)\right)\right\}$
23 20 22 imaeq12d ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to {{f}}^{-1}\left[\left\{{f}\left({a}+{d}\left({i}\right)\right)\right\}\right]={{F}}^{-1}\left[\left\{{F}\left({a}+{d}\left({i}\right)\right)\right\}\right]$
24 18 23 sseq12d ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to \left(\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({k}\right){d}\left({i}\right)\subseteq {{f}}^{-1}\left[\left\{{f}\left({a}+{d}\left({i}\right)\right)\right\}\right]↔\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({K}\right){d}\left({i}\right)\subseteq {{F}}^{-1}\left[\left\{{F}\left({a}+{d}\left({i}\right)\right)\right\}\right]\right)$
25 14 24 raleqbidv ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to \left(\forall {i}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({k}\right){d}\left({i}\right)\subseteq {{f}}^{-1}\left[\left\{{f}\left({a}+{d}\left({i}\right)\right)\right\}\right]↔\forall {i}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({K}\right){d}\left({i}\right)\subseteq {{F}}^{-1}\left[\left\{{F}\left({a}+{d}\left({i}\right)\right)\right\}\right]\right)$
26 14 21 mpteq12dv ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to \left({i}\in \left(1\dots {m}\right)⟼{f}\left({a}+{d}\left({i}\right)\right)\right)=\left({i}\in {J}⟼{F}\left({a}+{d}\left({i}\right)\right)\right)$
27 26 rneqd ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to \mathrm{ran}\left({i}\in \left(1\dots {m}\right)⟼{f}\left({a}+{d}\left({i}\right)\right)\right)=\mathrm{ran}\left({i}\in {J}⟼{F}\left({a}+{d}\left({i}\right)\right)\right)$
28 27 fveq2d ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to \left|\mathrm{ran}\left({i}\in \left(1\dots {m}\right)⟼{f}\left({a}+{d}\left({i}\right)\right)\right)\right|=\left|\mathrm{ran}\left({i}\in {J}⟼{F}\left({a}+{d}\left({i}\right)\right)\right)\right|$
29 28 12 eqeq12d ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to \left(\left|\mathrm{ran}\left({i}\in \left(1\dots {m}\right)⟼{f}\left({a}+{d}\left({i}\right)\right)\right)\right|={m}↔\left|\mathrm{ran}\left({i}\in {J}⟼{F}\left({a}+{d}\left({i}\right)\right)\right)\right|={M}\right)$
30 25 29 anbi12d ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to \left(\left(\forall {i}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({k}\right){d}\left({i}\right)\subseteq {{f}}^{-1}\left[\left\{{f}\left({a}+{d}\left({i}\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left({i}\in \left(1\dots {m}\right)⟼{f}\left({a}+{d}\left({i}\right)\right)\right)\right|={m}\right)↔\left(\forall {i}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({K}\right){d}\left({i}\right)\subseteq {{F}}^{-1}\left[\left\{{F}\left({a}+{d}\left({i}\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left({i}\in {J}⟼{F}\left({a}+{d}\left({i}\right)\right)\right)\right|={M}\right)\right)$
31 15 30 rexeqbidv ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to \left(\exists {d}\in \left({ℕ}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({k}\right){d}\left({i}\right)\subseteq {{f}}^{-1}\left[\left\{{f}\left({a}+{d}\left({i}\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left({i}\in \left(1\dots {m}\right)⟼{f}\left({a}+{d}\left({i}\right)\right)\right)\right|={m}\right)↔\exists {d}\in \left({ℕ}^{{J}}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({K}\right){d}\left({i}\right)\subseteq {{F}}^{-1}\left[\left\{{F}\left({a}+{d}\left({i}\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left({i}\in {J}⟼{F}\left({a}+{d}\left({i}\right)\right)\right)\right|={M}\right)\right)$
32 31 rexbidv ${⊢}\left({m}={M}\wedge {k}={K}\wedge {f}={F}\right)\to \left(\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in \left({ℕ}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({k}\right){d}\left({i}\right)\subseteq {{f}}^{-1}\left[\left\{{f}\left({a}+{d}\left({i}\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left({i}\in \left(1\dots {m}\right)⟼{f}\left({a}+{d}\left({i}\right)\right)\right)\right|={m}\right)↔\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in \left({ℕ}^{{J}}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({K}\right){d}\left({i}\right)\subseteq {{F}}^{-1}\left[\left\{{F}\left({a}+{d}\left({i}\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left({i}\in {J}⟼{F}\left({a}+{d}\left({i}\right)\right)\right)\right|={M}\right)\right)$
33 32 eloprabga ${⊢}\left({M}\in ℕ\wedge {K}\in {ℕ}_{0}\wedge {F}\in \mathrm{V}\right)\to \left(⟨⟨{M},{K}⟩,{F}⟩\in \left\{⟨⟨{m},{k}⟩,{f}⟩|\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in \left({ℕ}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({k}\right){d}\left({i}\right)\subseteq {{f}}^{-1}\left[\left\{{f}\left({a}+{d}\left({i}\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left({i}\in \left(1\dots {m}\right)⟼{f}\left({a}+{d}\left({i}\right)\right)\right)\right|={m}\right)\right\}↔\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in \left({ℕ}^{{J}}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({K}\right){d}\left({i}\right)\subseteq {{F}}^{-1}\left[\left\{{F}\left({a}+{d}\left({i}\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left({i}\in {J}⟼{F}\left({a}+{d}\left({i}\right)\right)\right)\right|={M}\right)\right)$
34 11 33 syl5bb ${⊢}\left({M}\in ℕ\wedge {K}\in {ℕ}_{0}\wedge {F}\in \mathrm{V}\right)\to \left(⟨{M},{K}⟩\mathrm{PolyAP}{F}↔\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in \left({ℕ}^{{J}}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({K}\right){d}\left({i}\right)\subseteq {{F}}^{-1}\left[\left\{{F}\left({a}+{d}\left({i}\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left({i}\in {J}⟼{F}\left({a}+{d}\left({i}\right)\right)\right)\right|={M}\right)\right)$
35 4 2 7 34 syl3anc ${⊢}{\phi }\to \left(⟨{M},{K}⟩\mathrm{PolyAP}{F}↔\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in \left({ℕ}^{{J}}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}+{d}\left({i}\right)\right)\mathrm{AP}\left({K}\right){d}\left({i}\right)\subseteq {{F}}^{-1}\left[\left\{{F}\left({a}+{d}\left({i}\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left({i}\in {J}⟼{F}\left({a}+{d}\left({i}\right)\right)\right)\right|={M}\right)\right)$