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 | |
|
vdwmc.2 | |
||
vdwmc.3 | |
||
vdwpc.4 | |
||
vdwpc.5 | |
||
Assertion | vdwpc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vdwmc.1 | |
|
2 | vdwmc.2 | |
|
3 | vdwmc.3 | |
|
4 | vdwpc.4 | |
|
5 | vdwpc.5 | |
|
6 | fex | |
|
7 | 3 1 6 | sylancl | |
8 | df-br | |
|
9 | df-vdwpc | |
|
10 | 9 | eleq2i | |
11 | 8 10 | bitri | |
12 | simp1 | |
|
13 | 12 | oveq2d | |
14 | 13 5 | eqtr4di | |
15 | 14 | oveq2d | |
16 | simp2 | |
|
17 | 16 | fveq2d | |
18 | 17 | oveqd | |
19 | simp3 | |
|
20 | 19 | cnveqd | |
21 | 19 | fveq1d | |
22 | 21 | sneqd | |
23 | 20 22 | imaeq12d | |
24 | 18 23 | sseq12d | |
25 | 14 24 | raleqbidv | |
26 | 14 21 | mpteq12dv | |
27 | 26 | rneqd | |
28 | 27 | fveq2d | |
29 | 28 12 | eqeq12d | |
30 | 25 29 | anbi12d | |
31 | 15 30 | rexeqbidv | |
32 | 31 | rexbidv | |
33 | 32 | eloprabga | |
34 | 11 33 | bitrid | |
35 | 4 2 7 34 | syl3anc | |