MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vdwpc Structured version   Unicode version

Theorem vdwpc 14041
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.)
Hypotheses
Ref Expression
vdwmc.1  |-  X  e. 
_V
vdwmc.2  |-  ( ph  ->  K  e.  NN0 )
vdwmc.3  |-  ( ph  ->  F : X --> R )
vdwpc.4  |-  ( ph  ->  M  e.  NN )
vdwpc.5  |-  J  =  ( 1 ... M
)
Assertion
Ref Expression
vdwpc  |-  ( ph  ->  ( <. M ,  K >. PolyAP 
F  <->  E. a  e.  NN  E. d  e.  ( NN 
^m  J ) ( A. i  e.  J  ( ( a  +  ( d `  i
) ) (AP `  K ) ( d `
 i ) ) 
C_  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } )  /\  ( # `  ran  ( i  e.  J  |->  ( F `  (
a  +  ( d `
 i ) ) ) ) )  =  M ) ) )
Distinct variable groups:    a, d,
i, F    K, a,
d, i    J, d,
i    M, a, d, i
Allowed substitution hints:    ph( i, a, d)    R( i, a, d)    J( a)    X( i, a, d)

Proof of Theorem vdwpc
Dummy variables  f 
k  m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vdwpc.4 . 2  |-  ( ph  ->  M  e.  NN )
2 vdwmc.2 . 2  |-  ( ph  ->  K  e.  NN0 )
3 vdwmc.3 . . 3  |-  ( ph  ->  F : X --> R )
4 vdwmc.1 . . 3  |-  X  e. 
_V
5 fex 5950 . . 3  |-  ( ( F : X --> R  /\  X  e.  _V )  ->  F  e.  _V )
63, 4, 5sylancl 662 . 2  |-  ( ph  ->  F  e.  _V )
7 df-br 4293 . . . 4  |-  ( <. M ,  K >. PolyAP  F  <->  <. <. M ,  K >. ,  F >.  e. PolyAP  )
8 df-vdwpc 14031 . . . . 5  |- PolyAP  =  { <. <. m ,  k
>. ,  f >.  |  E. a  e.  NN  E. d  e.  ( NN 
^m  ( 1 ... m ) ) ( A. i  e.  ( 1 ... m ) ( ( a  +  ( d `  i
) ) (AP `  k ) ( d `
 i ) ) 
C_  ( `' f
" { ( f `
 ( a  +  ( d `  i
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m ) }
98eleq2i 2507 . . . 4  |-  ( <. <. M ,  K >. ,  F >.  e. PolyAP  <->  <. <. M ,  K >. ,  F >.  e. 
{ <. <. m ,  k
>. ,  f >.  |  E. a  e.  NN  E. d  e.  ( NN 
^m  ( 1 ... m ) ) ( A. i  e.  ( 1 ... m ) ( ( a  +  ( d `  i
) ) (AP `  k ) ( d `
 i ) ) 
C_  ( `' f
" { ( f `
 ( a  +  ( d `  i
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m ) } )
107, 9bitri 249 . . 3  |-  ( <. M ,  K >. PolyAP  F  <->  <. <. M ,  K >. ,  F >.  e.  { <. <.
m ,  k >. ,  f >.  |  E. a  e.  NN  E. d  e.  ( NN  ^m  (
1 ... m ) ) ( A. i  e.  ( 1 ... m
) ( ( a  +  ( d `  i ) ) (AP
`  k ) ( d `  i ) )  C_  ( `' f " { ( f `
 ( a  +  ( d `  i
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m ) } )
11 simp1 988 . . . . . . . . 9  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  m  =  M )
1211oveq2d 6107 . . . . . . . 8  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ( 1 ... m
)  =  ( 1 ... M ) )
13 vdwpc.5 . . . . . . . 8  |-  J  =  ( 1 ... M
)
1412, 13syl6eqr 2493 . . . . . . 7  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ( 1 ... m
)  =  J )
1514oveq2d 6107 . . . . . 6  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ( NN  ^m  (
1 ... m ) )  =  ( NN  ^m  J ) )
16 simp2 989 . . . . . . . . . . 11  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  k  =  K )
1716fveq2d 5695 . . . . . . . . . 10  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  (AP `  k )  =  (AP `  K
) )
1817oveqd 6108 . . . . . . . . 9  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ( ( a  +  ( d `  i
) ) (AP `  k ) ( d `
 i ) )  =  ( ( a  +  ( d `  i ) ) (AP
`  K ) ( d `  i ) ) )
19 simp3 990 . . . . . . . . . . 11  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  f  =  F )
2019cnveqd 5015 . . . . . . . . . 10  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  `' f  =  `' F )
2119fveq1d 5693 . . . . . . . . . . 11  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ( f `  (
a  +  ( d `
 i ) ) )  =  ( F `
 ( a  +  ( d `  i
) ) ) )
2221sneqd 3889 . . . . . . . . . 10  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  { ( f `  ( a  +  ( d `  i ) ) ) }  =  { ( F `  ( a  +  ( d `  i ) ) ) } )
2320, 22imaeq12d 5170 . . . . . . . . 9  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ( `' f " { ( f `  ( a  +  ( d `  i ) ) ) } )  =  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } ) )
2418, 23sseq12d 3385 . . . . . . . 8  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ( ( ( a  +  ( d `  i ) ) (AP
`  k ) ( d `  i ) )  C_  ( `' f " { ( f `
 ( a  +  ( d `  i
) ) ) } )  <->  ( ( a  +  ( d `  i ) ) (AP
`  K ) ( d `  i ) )  C_  ( `' F " { ( F `
 ( a  +  ( d `  i
) ) ) } ) ) )
2514, 24raleqbidv 2931 . . . . . . 7  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ( A. i  e.  ( 1 ... m
) ( ( a  +  ( d `  i ) ) (AP
`  k ) ( d `  i ) )  C_  ( `' f " { ( f `
 ( a  +  ( d `  i
) ) ) } )  <->  A. i  e.  J  ( ( a  +  ( d `  i
) ) (AP `  K ) ( d `
 i ) ) 
C_  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } ) ) )
2614, 21mpteq12dv 4370 . . . . . . . . . 10  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ( i  e.  ( 1 ... m ) 
|->  ( f `  (
a  +  ( d `
 i ) ) ) )  =  ( i  e.  J  |->  ( F `  ( a  +  ( d `  i ) ) ) ) )
2726rneqd 5067 . . . . . . . . 9  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) )  =  ran  ( i  e.  J  |->  ( F `  ( a  +  ( d `  i ) ) ) ) )
2827fveq2d 5695 . . . . . . . 8  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ( # `  ran  ( i  e.  ( 1 ... m ) 
|->  ( f `  (
a  +  ( d `
 i ) ) ) ) )  =  ( # `  ran  ( i  e.  J  |->  ( F `  (
a  +  ( d `
 i ) ) ) ) ) )
2928, 11eqeq12d 2457 . . . . . . 7  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ( ( # `  ran  ( i  e.  ( 1 ... m ) 
|->  ( f `  (
a  +  ( d `
 i ) ) ) ) )  =  m  <->  ( # `  ran  ( i  e.  J  |->  ( F `  (
a  +  ( d `
 i ) ) ) ) )  =  M ) )
3025, 29anbi12d 710 . . . . . 6  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ( ( A. i  e.  ( 1 ... m
) ( ( a  +  ( d `  i ) ) (AP
`  k ) ( d `  i ) )  C_  ( `' f " { ( f `
 ( a  +  ( d `  i
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m )  <->  ( A. i  e.  J  (
( a  +  ( d `  i ) ) (AP `  K
) ( d `  i ) )  C_  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } )  /\  ( # `
 ran  ( i  e.  J  |->  ( F `
 ( a  +  ( d `  i
) ) ) ) )  =  M ) ) )
3115, 30rexeqbidv 2932 . . . . 5  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ( E. d  e.  ( NN  ^m  (
1 ... m ) ) ( A. i  e.  ( 1 ... m
) ( ( a  +  ( d `  i ) ) (AP
`  k ) ( d `  i ) )  C_  ( `' f " { ( f `
 ( a  +  ( d `  i
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m )  <->  E. d  e.  ( NN  ^m  J
) ( A. i  e.  J  ( (
a  +  ( d `
 i ) ) (AP `  K ) ( d `  i
) )  C_  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } )  /\  ( # `
 ran  ( i  e.  J  |->  ( F `
 ( a  +  ( d `  i
) ) ) ) )  =  M ) ) )
3231rexbidv 2736 . . . 4  |-  ( ( m  =  M  /\  k  =  K  /\  f  =  F )  ->  ( E. a  e.  NN  E. d  e.  ( NN  ^m  (
1 ... m ) ) ( A. i  e.  ( 1 ... m
) ( ( a  +  ( d `  i ) ) (AP
`  k ) ( d `  i ) )  C_  ( `' f " { ( f `
 ( a  +  ( d `  i
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m )  <->  E. a  e.  NN  E. d  e.  ( NN  ^m  J
) ( A. i  e.  J  ( (
a  +  ( d `
 i ) ) (AP `  K ) ( d `  i
) )  C_  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } )  /\  ( # `
 ran  ( i  e.  J  |->  ( F `
 ( a  +  ( d `  i
) ) ) ) )  =  M ) ) )
3332eloprabga 6177 . . 3  |-  ( ( M  e.  NN  /\  K  e.  NN0  /\  F  e.  _V )  ->  ( <. <. M ,  K >. ,  F >.  e.  { <. <. m ,  k
>. ,  f >.  |  E. a  e.  NN  E. d  e.  ( NN 
^m  ( 1 ... m ) ) ( A. i  e.  ( 1 ... m ) ( ( a  +  ( d `  i
) ) (AP `  k ) ( d `
 i ) ) 
C_  ( `' f
" { ( f `
 ( a  +  ( d `  i
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m ) }  <->  E. a  e.  NN  E. d  e.  ( NN 
^m  J ) ( A. i  e.  J  ( ( a  +  ( d `  i
) ) (AP `  K ) ( d `
 i ) ) 
C_  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } )  /\  ( # `  ran  ( i  e.  J  |->  ( F `  (
a  +  ( d `
 i ) ) ) ) )  =  M ) ) )
3410, 33syl5bb 257 . 2  |-  ( ( M  e.  NN  /\  K  e.  NN0  /\  F  e.  _V )  ->  ( <. M ,  K >. PolyAP  F  <->  E. a  e.  NN  E. d  e.  ( NN  ^m  J ) ( A. i  e.  J  (
( a  +  ( d `  i ) ) (AP `  K
) ( d `  i ) )  C_  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } )  /\  ( # `
 ran  ( i  e.  J  |->  ( F `
 ( a  +  ( d `  i
) ) ) ) )  =  M ) ) )
351, 2, 6, 34syl3anc 1218 1  |-  ( ph  ->  ( <. M ,  K >. PolyAP 
F  <->  E. a  e.  NN  E. d  e.  ( NN 
^m  J ) ( A. i  e.  J  ( ( a  +  ( d `  i
) ) (AP `  K ) ( d `
 i ) ) 
C_  ( `' F " { ( F `  ( a  +  ( d `  i ) ) ) } )  /\  ( # `  ran  ( i  e.  J  |->  ( F `  (
a  +  ( d `
 i ) ) ) ) )  =  M ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   A.wral 2715   E.wrex 2716   _Vcvv 2972    C_ wss 3328   {csn 3877   <.cop 3883   class class class wbr 4292    e. cmpt 4350   `'ccnv 4839   ran crn 4841   "cima 4843   -->wf 5414   ` cfv 5418  (class class class)co 6091   {coprab 6092    ^m cmap 7214   1c1 9283    + caddc 9285   NNcn 10322   NN0cn0 10579   ...cfz 11437   #chash 12103  APcvdwa 14026   PolyAP cvdwp 14028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pr 4531
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-ov 6094  df-oprab 6095  df-vdwpc 14031
This theorem is referenced by:  vdwlem6  14047  vdwlem7  14048  vdwlem8  14049  vdwlem11  14052
  Copyright terms: Public domain W3C validator