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 V
vdwmc.2 φ K 0
vdwmc.3 φ F : X R
vdwpc.4 φ M
vdwpc.5 J = 1 M
Assertion vdwpc φ M K PolyAP F a d J i J a + d i AP K d i F -1 F a + d i ran i J F a + d i = M

Proof

Step Hyp Ref Expression
1 vdwmc.1 X V
2 vdwmc.2 φ K 0
3 vdwmc.3 φ F : X R
4 vdwpc.4 φ M
5 vdwpc.5 J = 1 M
6 fex F : X R X V F V
7 3 1 6 sylancl φ F V
8 df-br M K PolyAP F M K F PolyAP
9 df-vdwpc PolyAP = m k f | a d 1 m i 1 m a + d i AP k d i f -1 f a + d i ran i 1 m f a + d i = m
10 9 eleq2i M K F PolyAP M K F m k f | a d 1 m i 1 m a + d i AP k d i f -1 f a + d i ran i 1 m f a + d i = m
11 8 10 bitri M K PolyAP F M K F m k f | a d 1 m i 1 m a + d i AP k d i f -1 f a + d i ran i 1 m f a + d i = m
12 simp1 m = M k = K f = F m = M
13 12 oveq2d m = M k = K f = F 1 m = 1 M
14 13 5 eqtr4di m = M k = K f = F 1 m = J
15 14 oveq2d m = M k = K f = F 1 m = J
16 simp2 m = M k = K f = F k = K
17 16 fveq2d m = M k = K f = F AP k = AP K
18 17 oveqd m = M k = K f = F a + d i AP k d i = a + d i AP K d i
19 simp3 m = M k = K f = F f = F
20 19 cnveqd m = M k = K f = F f -1 = F -1
21 19 fveq1d m = M k = K f = F f a + d i = F a + d i
22 21 sneqd m = M k = K f = F f a + d i = F a + d i
23 20 22 imaeq12d m = M k = K f = F f -1 f a + d i = F -1 F a + d i
24 18 23 sseq12d m = M k = K f = F a + d i AP k d i f -1 f a + d i a + d i AP K d i F -1 F a + d i
25 14 24 raleqbidv m = M k = K f = F i 1 m a + d i AP k d i f -1 f a + d i i J a + d i AP K d i F -1 F a + d i
26 14 21 mpteq12dv m = M k = K f = F i 1 m f a + d i = i J F a + d i
27 26 rneqd m = M k = K f = F ran i 1 m f a + d i = ran i J F a + d i
28 27 fveq2d m = M k = K f = F ran i 1 m f a + d i = ran i J F a + d i
29 28 12 eqeq12d m = M k = K f = F ran i 1 m f a + d i = m ran i J F a + d i = M
30 25 29 anbi12d m = M k = K f = F i 1 m a + d i AP k d i f -1 f a + d i ran i 1 m f a + d i = m i J a + d i AP K d i F -1 F a + d i ran i J F a + d i = M
31 15 30 rexeqbidv m = M k = K f = F d 1 m i 1 m a + d i AP k d i f -1 f a + d i ran i 1 m f a + d i = m d J i J a + d i AP K d i F -1 F a + d i ran i J F a + d i = M
32 31 rexbidv m = M k = K f = F a d 1 m i 1 m a + d i AP k d i f -1 f a + d i ran i 1 m f a + d i = m a d J i J a + d i AP K d i F -1 F a + d i ran i J F a + d i = M
33 32 eloprabga M K 0 F V M K F m k f | a d 1 m i 1 m a + d i AP k d i f -1 f a + d i ran i 1 m f a + d i = m a d J i J a + d i AP K d i F -1 F a + d i ran i J F a + d i = M
34 11 33 syl5bb M K 0 F V M K PolyAP F a d J i J a + d i AP K d i F -1 F a + d i ran i J F a + d i = M
35 4 2 7 34 syl3anc φ M K PolyAP F a d J i J a + d i AP K d i F -1 F a + d i ran i J F a + d i = M