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

Theorem vdwlem2 13031
Description: Lemma for vdw 13043. (Contributed by Mario Carneiro, 12-Sep-2014.)
Hypotheses
Ref Expression
vdwlem2.r  |-  ( ph  ->  R  e.  Fin )
vdwlem2.k  |-  ( ph  ->  K  e.  NN0 )
vdwlem2.w  |-  ( ph  ->  W  e.  NN )
vdwlem2.n  |-  ( ph  ->  N  e.  NN )
vdwlem2.f  |-  ( ph  ->  F : ( 1 ... M ) --> R )
vdwlem2.m  |-  ( ph  ->  M  e.  ( ZZ>= `  ( W  +  N
) ) )
vdwlem2.g  |-  G  =  ( x  e.  ( 1 ... W ) 
|->  ( F `  (
x  +  N ) ) )
Assertion
Ref Expression
vdwlem2  |-  ( ph  ->  ( K MonoAP  G  ->  K MonoAP  F ) )
Distinct variable groups:    x, F    x, K    x, M    ph, x    x, G    x, N    x, R    x, W

Proof of Theorem vdwlem2
Dummy variables  a 
b  c  d  m  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 19 . . . . . 6  |-  ( a  e.  NN  ->  a  e.  NN )
2 vdwlem2.n . . . . . 6  |-  ( ph  ->  N  e.  NN )
3 nnaddcl 9770 . . . . . 6  |-  ( ( a  e.  NN  /\  N  e.  NN )  ->  ( a  +  N
)  e.  NN )
41, 2, 3syl2anr 464 . . . . 5  |-  ( (
ph  /\  a  e.  NN )  ->  ( a  +  N )  e.  NN )
5 simpllr 735 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  a  e.  NN )
65nncnd 9764 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  a  e.  CC )
72ad3antrrr 710 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  N  e.  NN )
87nncnd 9764 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  N  e.  CC )
9 elfznn0 10824 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  ( 0 ... ( K  -  1 ) )  ->  m  e.  NN0 )
109adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  m  e.  NN0 )
1110nn0cnd 10022 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  m  e.  CC )
12 simplrl 736 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  d  e.  NN )
1312nncnd 9764 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  d  e.  CC )
1411, 13mulcld 8857 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
m  x.  d )  e.  CC )
156, 8, 14add32d 9036 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( a  +  N
)  +  ( m  x.  d ) )  =  ( ( a  +  ( m  x.  d ) )  +  N ) )
16 simplrr 737 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
a (AP `  K
) d )  C_  ( `' G " { c } ) )
17 eqid 2285 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  +  ( m  x.  d ) )  =  ( a  +  ( m  x.  d ) )
18 oveq1 5867 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  m  ->  (
n  x.  d )  =  ( m  x.  d ) )
1918oveq2d 5876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  m  ->  (
a  +  ( n  x.  d ) )  =  ( a  +  ( m  x.  d
) ) )
2019eqeq2d 2296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  m  ->  (
( a  +  ( m  x.  d ) )  =  ( a  +  ( n  x.  d ) )  <->  ( a  +  ( m  x.  d ) )  =  ( a  +  ( m  x.  d ) ) ) )
2120rspcev 2886 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( m  e.  ( 0 ... ( K  - 
1 ) )  /\  ( a  +  ( m  x.  d ) )  =  ( a  +  ( m  x.  d ) ) )  ->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( a  +  ( m  x.  d ) )  =  ( a  +  ( n  x.  d ) ) )
2217, 21mpan2 652 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  ( 0 ... ( K  -  1 ) )  ->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( a  +  ( m  x.  d
) )  =  ( a  +  ( n  x.  d ) ) )
2322adantl 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( a  +  ( m  x.  d
) )  =  ( a  +  ( n  x.  d ) ) )
24 vdwlem2.k . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  K  e.  NN0 )
2524ad2antrr 706 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  a  e.  NN )  /\  (
d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  ->  K  e.  NN0 )
2625adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  K  e.  NN0 )
27 vdwapval 13022 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  NN0  /\  a  e.  NN  /\  d  e.  NN )  ->  (
( a  +  ( m  x.  d ) )  e.  ( a (AP `  K ) d )  <->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( a  +  ( m  x.  d
) )  =  ( a  +  ( n  x.  d ) ) ) )
2826, 5, 12, 27syl3anc 1182 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( a  +  ( m  x.  d ) )  e.  ( a (AP `  K ) d )  <->  E. n  e.  ( 0 ... ( K  -  1 ) ) ( a  +  ( m  x.  d
) )  =  ( a  +  ( n  x.  d ) ) ) )
2923, 28mpbird 223 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
a  +  ( m  x.  d ) )  e.  ( a (AP
`  K ) d ) )
3016, 29sseldd 3183 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
a  +  ( m  x.  d ) )  e.  ( `' G " { c } ) )
31 elfznn 10821 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ( 1 ... W )  ->  x  e.  NN )
32 nnaddcl 9770 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  NN  /\  N  e.  NN )  ->  ( x  +  N
)  e.  NN )
3331, 2, 32syl2anr 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... W
) )  ->  (
x  +  N )  e.  NN )
34 nnuz 10265 . . . . . . . . . . . . . . . . . . . . . . 23  |-  NN  =  ( ZZ>= `  1 )
3533, 34syl6eleq 2375 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... W
) )  ->  (
x  +  N )  e.  ( ZZ>= `  1
) )
36 vdwlem2.m . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  M  e.  ( ZZ>= `  ( W  +  N
) ) )
3736adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... W
) )  ->  M  e.  ( ZZ>= `  ( W  +  N ) ) )
38 elfzuz3 10797 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ( 1 ... W )  ->  W  e.  ( ZZ>= `  x )
)
392nnzd 10118 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  N  e.  ZZ )
40 eluzadd 10258 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( W  e.  ( ZZ>= `  x )  /\  N  e.  ZZ )  ->  ( W  +  N )  e.  ( ZZ>= `  ( x  +  N ) ) )
4138, 39, 40syl2anr 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... W
) )  ->  ( W  +  N )  e.  ( ZZ>= `  ( x  +  N ) ) )
42 uztrn 10246 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( M  e.  ( ZZ>= `  ( W  +  N
) )  /\  ( W  +  N )  e.  ( ZZ>= `  ( x  +  N ) ) )  ->  M  e.  (
ZZ>= `  ( x  +  N ) ) )
4337, 41, 42syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... W
) )  ->  M  e.  ( ZZ>= `  ( x  +  N ) ) )
44 elfzuzb 10794 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  +  N )  e.  ( 1 ... M )  <->  ( (
x  +  N )  e.  ( ZZ>= `  1
)  /\  M  e.  ( ZZ>= `  ( x  +  N ) ) ) )
4535, 43, 44sylanbrc 645 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... W
) )  ->  (
x  +  N )  e.  ( 1 ... M ) )
46 vdwlem2.f . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  F : ( 1 ... M ) --> R )
47 ffvelrn 5665 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F : ( 1 ... M ) --> R  /\  ( x  +  N )  e.  ( 1 ... M ) )  ->  ( F `  ( x  +  N
) )  e.  R
)
4846, 47sylan 457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( x  +  N )  e.  ( 1 ... M ) )  ->  ( F `  ( x  +  N
) )  e.  R
)
4945, 48syldan 456 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... W
) )  ->  ( F `  ( x  +  N ) )  e.  R )
50 vdwlem2.g . . . . . . . . . . . . . . . . . . . 20  |-  G  =  ( x  e.  ( 1 ... W ) 
|->  ( F `  (
x  +  N ) ) )
5149, 50fmptd 5686 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  G : ( 1 ... W ) --> R )
52 ffn 5391 . . . . . . . . . . . . . . . . . . 19  |-  ( G : ( 1 ... W ) --> R  ->  G  Fn  ( 1 ... W ) )
5351, 52syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  G  Fn  ( 1 ... W ) )
5453ad3antrrr 710 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  G  Fn  ( 1 ... W
) )
55 fniniseg 5648 . . . . . . . . . . . . . . . . 17  |-  ( G  Fn  ( 1 ... W )  ->  (
( a  +  ( m  x.  d ) )  e.  ( `' G " { c } )  <->  ( (
a  +  ( m  x.  d ) )  e.  ( 1 ... W )  /\  ( G `  ( a  +  ( m  x.  d ) ) )  =  c ) ) )
5654, 55syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( a  +  ( m  x.  d ) )  e.  ( `' G " { c } )  <->  ( (
a  +  ( m  x.  d ) )  e.  ( 1 ... W )  /\  ( G `  ( a  +  ( m  x.  d ) ) )  =  c ) ) )
5730, 56mpbid 201 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( a  +  ( m  x.  d ) )  e.  ( 1 ... W )  /\  ( G `  ( a  +  ( m  x.  d ) ) )  =  c ) )
5857simpld 445 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
a  +  ( m  x.  d ) )  e.  ( 1 ... W ) )
5945ralrimiva 2628 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. x  e.  ( 1 ... W ) ( x  +  N
)  e.  ( 1 ... M ) )
6059ad3antrrr 710 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  A. x  e.  ( 1 ... W
) ( x  +  N )  e.  ( 1 ... M ) )
61 oveq1 5867 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( a  +  ( m  x.  d
) )  ->  (
x  +  N )  =  ( ( a  +  ( m  x.  d ) )  +  N ) )
6261eleq1d 2351 . . . . . . . . . . . . . . 15  |-  ( x  =  ( a  +  ( m  x.  d
) )  ->  (
( x  +  N
)  e.  ( 1 ... M )  <->  ( (
a  +  ( m  x.  d ) )  +  N )  e.  ( 1 ... M
) ) )
6362rspcv 2882 . . . . . . . . . . . . . 14  |-  ( ( a  +  ( m  x.  d ) )  e.  ( 1 ... W )  ->  ( A. x  e.  (
1 ... W ) ( x  +  N )  e.  ( 1 ... M )  ->  (
( a  +  ( m  x.  d ) )  +  N )  e.  ( 1 ... M ) ) )
6458, 60, 63sylc 56 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( a  +  ( m  x.  d ) )  +  N )  e.  ( 1 ... M ) )
6515, 64eqeltrd 2359 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( a  +  N
)  +  ( m  x.  d ) )  e.  ( 1 ... M ) )
6615fveq2d 5531 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( F `  ( (
a  +  N )  +  ( m  x.  d ) ) )  =  ( F `  ( ( a  +  ( m  x.  d
) )  +  N
) ) )
6761fveq2d 5531 . . . . . . . . . . . . . . 15  |-  ( x  =  ( a  +  ( m  x.  d
) )  ->  ( F `  ( x  +  N ) )  =  ( F `  (
( a  +  ( m  x.  d ) )  +  N ) ) )
68 fvex 5541 . . . . . . . . . . . . . . 15  |-  ( F `
 ( ( a  +  ( m  x.  d ) )  +  N ) )  e. 
_V
6967, 50, 68fvmpt 5604 . . . . . . . . . . . . . 14  |-  ( ( a  +  ( m  x.  d ) )  e.  ( 1 ... W )  ->  ( G `  ( a  +  ( m  x.  d ) ) )  =  ( F `  ( ( a  +  ( m  x.  d
) )  +  N
) ) )
7058, 69syl 15 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( G `  ( a  +  ( m  x.  d ) ) )  =  ( F `  ( ( a  +  ( m  x.  d
) )  +  N
) ) )
7157simprd 449 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( G `  ( a  +  ( m  x.  d ) ) )  =  c )
7266, 70, 713eqtr2d 2323 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  ( F `  ( (
a  +  N )  +  ( m  x.  d ) ) )  =  c )
7365, 72jca 518 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
( ( a  +  N )  +  ( m  x.  d ) )  e.  ( 1 ... M )  /\  ( F `  ( ( a  +  N )  +  ( m  x.  d ) ) )  =  c ) )
74 eleq1 2345 . . . . . . . . . . . 12  |-  ( x  =  ( ( a  +  N )  +  ( m  x.  d
) )  ->  (
x  e.  ( 1 ... M )  <->  ( (
a  +  N )  +  ( m  x.  d ) )  e.  ( 1 ... M
) ) )
75 fveq2 5527 . . . . . . . . . . . . 13  |-  ( x  =  ( ( a  +  N )  +  ( m  x.  d
) )  ->  ( F `  x )  =  ( F `  ( ( a  +  N )  +  ( m  x.  d ) ) ) )
7675eqeq1d 2293 . . . . . . . . . . . 12  |-  ( x  =  ( ( a  +  N )  +  ( m  x.  d
) )  ->  (
( F `  x
)  =  c  <->  ( F `  ( ( a  +  N )  +  ( m  x.  d ) ) )  =  c ) )
7774, 76anbi12d 691 . . . . . . . . . . 11  |-  ( x  =  ( ( a  +  N )  +  ( m  x.  d
) )  ->  (
( x  e.  ( 1 ... M )  /\  ( F `  x )  =  c )  <->  ( ( ( a  +  N )  +  ( m  x.  d ) )  e.  ( 1 ... M
)  /\  ( F `  ( ( a  +  N )  +  ( m  x.  d ) ) )  =  c ) ) )
7873, 77syl5ibrcom 213 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  NN )  /\  ( d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  /\  m  e.  ( 0 ... ( K  -  1 ) ) )  ->  (
x  =  ( ( a  +  N )  +  ( m  x.  d ) )  -> 
( x  e.  ( 1 ... M )  /\  ( F `  x )  =  c ) ) )
7978rexlimdva 2669 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  NN )  /\  (
d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  ->  ( E. m  e.  (
0 ... ( K  - 
1 ) ) x  =  ( ( a  +  N )  +  ( m  x.  d
) )  ->  (
x  e.  ( 1 ... M )  /\  ( F `  x )  =  c ) ) )
804adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  NN )  /\  (
d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  ->  (
a  +  N )  e.  NN )
81 simprl 732 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  NN )  /\  (
d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  ->  d  e.  NN )
82 vdwapval 13022 . . . . . . . . . 10  |-  ( ( K  e.  NN0  /\  ( a  +  N
)  e.  NN  /\  d  e.  NN )  ->  ( x  e.  ( ( a  +  N
) (AP `  K
) d )  <->  E. m  e.  ( 0 ... ( K  -  1 ) ) x  =  ( ( a  +  N
)  +  ( m  x.  d ) ) ) )
8325, 80, 81, 82syl3anc 1182 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  NN )  /\  (
d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  ->  (
x  e.  ( ( a  +  N ) (AP `  K ) d )  <->  E. m  e.  ( 0 ... ( K  -  1 ) ) x  =  ( ( a  +  N
)  +  ( m  x.  d ) ) ) )
84 ffn 5391 . . . . . . . . . . . 12  |-  ( F : ( 1 ... M ) --> R  ->  F  Fn  ( 1 ... M ) )
8546, 84syl 15 . . . . . . . . . . 11  |-  ( ph  ->  F  Fn  ( 1 ... M ) )
8685ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  a  e.  NN )  /\  (
d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  ->  F  Fn  ( 1 ... M
) )
87 fniniseg 5648 . . . . . . . . . 10  |-  ( F  Fn  ( 1 ... M )  ->  (
x  e.  ( `' F " { c } )  <->  ( x  e.  ( 1 ... M
)  /\  ( F `  x )  =  c ) ) )
8886, 87syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  a  e.  NN )  /\  (
d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  ->  (
x  e.  ( `' F " { c } )  <->  ( x  e.  ( 1 ... M
)  /\  ( F `  x )  =  c ) ) )
8979, 83, 883imtr4d 259 . . . . . . . 8  |-  ( ( ( ph  /\  a  e.  NN )  /\  (
d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  ->  (
x  e.  ( ( a  +  N ) (AP `  K ) d )  ->  x  e.  ( `' F " { c } ) ) )
9089ssrdv 3187 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  NN )  /\  (
d  e.  NN  /\  ( a (AP `  K ) d ) 
C_  ( `' G " { c } ) ) )  ->  (
( a  +  N
) (AP `  K
) d )  C_  ( `' F " { c } ) )
9190expr 598 . . . . . 6  |-  ( ( ( ph  /\  a  e.  NN )  /\  d  e.  NN )  ->  (
( a (AP `  K ) d ) 
C_  ( `' G " { c } )  ->  ( ( a  +  N ) (AP
`  K ) d )  C_  ( `' F " { c } ) ) )
9291reximdva 2657 . . . . 5  |-  ( (
ph  /\  a  e.  NN )  ->  ( E. d  e.  NN  (
a (AP `  K
) d )  C_  ( `' G " { c } )  ->  E. d  e.  NN  ( ( a  +  N ) (AP
`  K ) d )  C_  ( `' F " { c } ) ) )
93 oveq1 5867 . . . . . . . 8  |-  ( b  =  ( a  +  N )  ->  (
b (AP `  K
) d )  =  ( ( a  +  N ) (AP `  K ) d ) )
9493sseq1d 3207 . . . . . . 7  |-  ( b  =  ( a  +  N )  ->  (
( b (AP `  K ) d ) 
C_  ( `' F " { c } )  <-> 
( ( a  +  N ) (AP `  K ) d ) 
C_  ( `' F " { c } ) ) )
9594rexbidv 2566 . . . . . 6  |-  ( b  =  ( a  +  N )  ->  ( E. d  e.  NN  ( b (AP `  K ) d ) 
C_  ( `' F " { c } )  <->  E. d  e.  NN  ( ( a  +  N ) (AP `  K ) d ) 
C_  ( `' F " { c } ) ) )
9695rspcev 2886 . . . . 5  |-  ( ( ( a  +  N
)  e.  NN  /\  E. d  e.  NN  (
( a  +  N
) (AP `  K
) d )  C_  ( `' F " { c } ) )  ->  E. b  e.  NN  E. d  e.  NN  (
b (AP `  K
) d )  C_  ( `' F " { c } ) )
974, 92, 96ee12an 1353 . . . 4  |-  ( (
ph  /\  a  e.  NN )  ->  ( E. d  e.  NN  (
a (AP `  K
) d )  C_  ( `' G " { c } )  ->  E. b  e.  NN  E. d  e.  NN  ( b (AP
`  K ) d )  C_  ( `' F " { c } ) ) )
9897rexlimdva 2669 . . 3  |-  ( ph  ->  ( E. a  e.  NN  E. d  e.  NN  ( a (AP
`  K ) d )  C_  ( `' G " { c } )  ->  E. b  e.  NN  E. d  e.  NN  ( b (AP
`  K ) d )  C_  ( `' F " { c } ) ) )
9998eximdv 1610 . 2  |-  ( ph  ->  ( E. c E. a  e.  NN  E. d  e.  NN  (
a (AP `  K
) d )  C_  ( `' G " { c } )  ->  E. c E. b  e.  NN  E. d  e.  NN  (
b (AP `  K
) d )  C_  ( `' F " { c } ) ) )
100 ovex 5885 . . 3  |-  ( 1 ... W )  e. 
_V
101100, 24, 51vdwmc 13027 . 2  |-  ( ph  ->  ( K MonoAP  G  <->  E. c E. a  e.  NN  E. d  e.  NN  (
a (AP `  K
) d )  C_  ( `' G " { c } ) ) )
102 ovex 5885 . . 3  |-  ( 1 ... M )  e. 
_V
103102, 24, 46vdwmc 13027 . 2  |-  ( ph  ->  ( K MonoAP  F  <->  E. c E. b  e.  NN  E. d  e.  NN  (
b (AP `  K
) d )  C_  ( `' F " { c } ) ) )
10499, 101, 1033imtr4d 259 1  |-  ( ph  ->  ( K MonoAP  G  ->  K MonoAP  F ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   E.wex 1530    = wceq 1625    e. wcel 1686   A.wral 2545   E.wrex 2546    C_ wss 3154   {csn 3642   class class class wbr 4025    e. cmpt 4079   `'ccnv 4690   "cima 4694    Fn wfn 5252   -->wf 5253   ` cfv 5257  (class class class)co 5860   Fincfn 6865   0cc0 8739   1c1 8740    + caddc 8742    x. cmul 8744    - cmin 9039   NNcn 9748   NN0cn0 9967   ZZcz 10026   ZZ>=cuz 10232   ...cfz 10784  APcvdwa 13014   MonoAP cvdwm 13015
This theorem is referenced by:  vdwlem9  13038
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-cnex 8795  ax-resscn 8796  ax-1cn 8797  ax-icn 8798  ax-addcl 8799  ax-addrcl 8800  ax-mulcl 8801  ax-mulrcl 8802  ax-mulcom 8803  ax-addass 8804  ax-mulass 8805  ax-distr 8806  ax-i2m1 8807  ax-1ne0 8808  ax-1rid 8809  ax-rnegex 8810  ax-rrecex 8811  ax-cnre 8812  ax-pre-lttri 8813  ax-pre-lttrn 8814  ax-pre-ltadd 8815  ax-pre-mulgt0 8816
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-1st 6124  df-2nd 6125  df-riota 6306  df-recs 6390  df-rdg 6425  df-er 6662  df-en 6866  df-dom 6867  df-sdom 6868  df-pnf 8871  df-mnf 8872  df-xr 8873  df-ltxr 8874  df-le 8875  df-sub 9041  df-neg 9042  df-nn 9749  df-n0 9968  df-z 10027  df-uz 10233  df-fz 10785  df-vdwap 13017  df-vdwmc 13018
  Copyright terms: Public domain W3C validator