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 XV
vdwmc.2 φK0
vdwmc.3 φF:XR
vdwpc.4 φM
vdwpc.5 J=1M
Assertion vdwpc φMKPolyAPFadJiJa+diAPKdiF-1Fa+diraniJFa+di=M

Proof

Step Hyp Ref Expression
1 vdwmc.1 XV
2 vdwmc.2 φK0
3 vdwmc.3 φF:XR
4 vdwpc.4 φM
5 vdwpc.5 J=1M
6 fex F:XRXVFV
7 3 1 6 sylancl φFV
8 df-br MKPolyAPFMKFPolyAP
9 df-vdwpc PolyAP=mkf|ad1mi1ma+diAPkdif-1fa+dirani1mfa+di=m
10 9 eleq2i MKFPolyAPMKFmkf|ad1mi1ma+diAPkdif-1fa+dirani1mfa+di=m
11 8 10 bitri MKPolyAPFMKFmkf|ad1mi1ma+diAPkdif-1fa+dirani1mfa+di=m
12 simp1 m=Mk=Kf=Fm=M
13 12 oveq2d m=Mk=Kf=F1m=1M
14 13 5 eqtr4di m=Mk=Kf=F1m=J
15 14 oveq2d m=Mk=Kf=F1m=J
16 simp2 m=Mk=Kf=Fk=K
17 16 fveq2d m=Mk=Kf=FAPk=APK
18 17 oveqd m=Mk=Kf=Fa+diAPkdi=a+diAPKdi
19 simp3 m=Mk=Kf=Ff=F
20 19 cnveqd m=Mk=Kf=Ff-1=F-1
21 19 fveq1d m=Mk=Kf=Ffa+di=Fa+di
22 21 sneqd m=Mk=Kf=Ffa+di=Fa+di
23 20 22 imaeq12d m=Mk=Kf=Ff-1fa+di=F-1Fa+di
24 18 23 sseq12d m=Mk=Kf=Fa+diAPkdif-1fa+dia+diAPKdiF-1Fa+di
25 14 24 raleqbidv m=Mk=Kf=Fi1ma+diAPkdif-1fa+diiJa+diAPKdiF-1Fa+di
26 14 21 mpteq12dv m=Mk=Kf=Fi1mfa+di=iJFa+di
27 26 rneqd m=Mk=Kf=Frani1mfa+di=raniJFa+di
28 27 fveq2d m=Mk=Kf=Frani1mfa+di=raniJFa+di
29 28 12 eqeq12d m=Mk=Kf=Frani1mfa+di=mraniJFa+di=M
30 25 29 anbi12d m=Mk=Kf=Fi1ma+diAPkdif-1fa+dirani1mfa+di=miJa+diAPKdiF-1Fa+diraniJFa+di=M
31 15 30 rexeqbidv m=Mk=Kf=Fd1mi1ma+diAPkdif-1fa+dirani1mfa+di=mdJiJa+diAPKdiF-1Fa+diraniJFa+di=M
32 31 rexbidv m=Mk=Kf=Fad1mi1ma+diAPkdif-1fa+dirani1mfa+di=madJiJa+diAPKdiF-1Fa+diraniJFa+di=M
33 32 eloprabga MK0FVMKFmkf|ad1mi1ma+diAPkdif-1fa+dirani1mfa+di=madJiJa+diAPKdiF-1Fa+diraniJFa+di=M
34 11 33 bitrid MK0FVMKPolyAPFadJiJa+diAPKdiF-1Fa+diraniJFa+di=M
35 4 2 7 34 syl3anc φMKPolyAPFadJiJa+diAPKdiF-1Fa+diraniJFa+di=M