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 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 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 ) ) )

Proof

Step Hyp Ref Expression
1 vdwmc.1 
 |-  X e. _V
2 vdwmc.2 
 |-  ( ph -> K e. NN0 )
3 vdwmc.3 
 |-  ( ph -> F : X --> R )
4 vdwpc.4 
 |-  ( ph -> M e. NN )
5 vdwpc.5 
 |-  J = ( 1 ... M )
6 fex 
 |-  ( ( F : X --> R /\ X e. _V ) -> F e. _V )
7 3 1 6 sylancl 
 |-  ( ph -> F e. _V )
8 df-br 
 |-  ( <. M , K >. PolyAP F <-> <. <. M , K >. , F >. e. PolyAP )
9 df-vdwpc 
 |-  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 ) }
10 9 eleq2i 
 |-  ( <. <. 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 ) } )
11 8 10 bitri 
 |-  ( <. 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 ) } )
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 ) -> ( NN ^m ( 1 ... m ) ) = ( NN ^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 = `' F )
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 " { ( f ` ( a + ( d ` i ) ) ) } ) = ( `' F " { ( F ` ( a + ( d ` i ) ) ) } ) )
24 18 23 sseq12d 
 |-  ( ( 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 ) ) ) } ) ) )
25 14 24 raleqbidv 
 |-  ( ( 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 ) ) ) } ) ) )
26 14 21 mpteq12dv 
 |-  ( ( m = M /\ k = K /\ f = F ) -> ( i e. ( 1 ... m ) |-> ( f ` ( a + ( d ` i ) ) ) ) = ( i e. J |-> ( F ` ( a + ( d ` i ) ) ) ) )
27 26 rneqd 
 |-  ( ( m = M /\ k = K /\ f = F ) -> ran ( i e. ( 1 ... m ) |-> ( f ` ( a + ( d ` i ) ) ) ) = ran ( i e. J |-> ( F ` ( a + ( d ` i ) ) ) ) )
28 27 fveq2d 
 |-  ( ( m = M /\ k = K /\ f = F ) -> ( # ` ran ( i e. ( 1 ... m ) |-> ( f ` ( a + ( d ` i ) ) ) ) ) = ( # ` ran ( i e. J |-> ( F ` ( a + ( d ` i ) ) ) ) ) )
29 28 12 eqeq12d 
 |-  ( ( 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 ) )
30 25 29 anbi12d 
 |-  ( ( 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 ) ) )
31 15 30 rexeqbidv 
 |-  ( ( 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 ) ) )
32 31 rexbidv 
 |-  ( ( 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 ) ) )
33 32 eloprabga 
 |-  ( ( 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 ) ) )
34 11 33 syl5bb 
 |-  ( ( 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 ) ) )
35 4 2 7 34 syl3anc 
 |-  ( 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 ) ) )