Step |
Hyp |
Ref |
Expression |
1 |
|
vdw.r |
|- ( ph -> R e. Fin ) |
2 |
|
vdwlem9.k |
|- ( ph -> K e. ( ZZ>= ` 2 ) ) |
3 |
|
vdwlem9.s |
|- ( ph -> A. s e. Fin E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f ) |
4 |
|
vdwlem10.m |
|- ( ph -> M e. NN ) |
5 |
|
opeq1 |
|- ( x = 1 -> <. x , K >. = <. 1 , K >. ) |
6 |
5
|
breq1d |
|- ( x = 1 -> ( <. x , K >. PolyAP f <-> <. 1 , K >. PolyAP f ) ) |
7 |
6
|
orbi1d |
|- ( x = 1 -> ( ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
8 |
7
|
rexralbidv |
|- ( x = 1 -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
9 |
8
|
imbi2d |
|- ( x = 1 -> ( ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) <-> ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) ) |
10 |
|
opeq1 |
|- ( x = m -> <. x , K >. = <. m , K >. ) |
11 |
10
|
breq1d |
|- ( x = m -> ( <. x , K >. PolyAP f <-> <. m , K >. PolyAP f ) ) |
12 |
11
|
orbi1d |
|- ( x = m -> ( ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
13 |
12
|
rexralbidv |
|- ( x = m -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
14 |
13
|
imbi2d |
|- ( x = m -> ( ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) <-> ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) ) |
15 |
|
opeq1 |
|- ( x = ( m + 1 ) -> <. x , K >. = <. ( m + 1 ) , K >. ) |
16 |
15
|
breq1d |
|- ( x = ( m + 1 ) -> ( <. x , K >. PolyAP f <-> <. ( m + 1 ) , K >. PolyAP f ) ) |
17 |
16
|
orbi1d |
|- ( x = ( m + 1 ) -> ( ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
18 |
17
|
rexralbidv |
|- ( x = ( m + 1 ) -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
19 |
18
|
imbi2d |
|- ( x = ( m + 1 ) -> ( ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) <-> ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) ) |
20 |
|
opeq1 |
|- ( x = M -> <. x , K >. = <. M , K >. ) |
21 |
20
|
breq1d |
|- ( x = M -> ( <. x , K >. PolyAP f <-> <. M , K >. PolyAP f ) ) |
22 |
21
|
orbi1d |
|- ( x = M -> ( ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> ( <. M , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
23 |
22
|
rexralbidv |
|- ( x = M -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. M , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
24 |
23
|
imbi2d |
|- ( x = M -> ( ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) <-> ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. M , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) ) |
25 |
|
oveq1 |
|- ( s = R -> ( s ^m ( 1 ... n ) ) = ( R ^m ( 1 ... n ) ) ) |
26 |
25
|
raleqdv |
|- ( s = R -> ( A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f <-> A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f ) ) |
27 |
26
|
rexbidv |
|- ( s = R -> ( E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f <-> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f ) ) |
28 |
27 3 1
|
rspcdva |
|- ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f ) |
29 |
|
oveq2 |
|- ( n = w -> ( 1 ... n ) = ( 1 ... w ) ) |
30 |
29
|
oveq2d |
|- ( n = w -> ( R ^m ( 1 ... n ) ) = ( R ^m ( 1 ... w ) ) ) |
31 |
30
|
raleqdv |
|- ( n = w -> ( A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f <-> A. f e. ( R ^m ( 1 ... w ) ) K MonoAP f ) ) |
32 |
31
|
cbvrexvw |
|- ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f <-> E. w e. NN A. f e. ( R ^m ( 1 ... w ) ) K MonoAP f ) |
33 |
28 32
|
sylib |
|- ( ph -> E. w e. NN A. f e. ( R ^m ( 1 ... w ) ) K MonoAP f ) |
34 |
|
breq2 |
|- ( f = g -> ( K MonoAP f <-> K MonoAP g ) ) |
35 |
34
|
cbvralvw |
|- ( A. f e. ( R ^m ( 1 ... w ) ) K MonoAP f <-> A. g e. ( R ^m ( 1 ... w ) ) K MonoAP g ) |
36 |
|
2nn |
|- 2 e. NN |
37 |
|
simpr |
|- ( ( ph /\ w e. NN ) -> w e. NN ) |
38 |
|
nnmulcl |
|- ( ( 2 e. NN /\ w e. NN ) -> ( 2 x. w ) e. NN ) |
39 |
36 37 38
|
sylancr |
|- ( ( ph /\ w e. NN ) -> ( 2 x. w ) e. NN ) |
40 |
1
|
adantr |
|- ( ( ph /\ w e. NN ) -> R e. Fin ) |
41 |
|
ovex |
|- ( 1 ... ( 2 x. w ) ) e. _V |
42 |
|
elmapg |
|- ( ( R e. Fin /\ ( 1 ... ( 2 x. w ) ) e. _V ) -> ( f e. ( R ^m ( 1 ... ( 2 x. w ) ) ) <-> f : ( 1 ... ( 2 x. w ) ) --> R ) ) |
43 |
40 41 42
|
sylancl |
|- ( ( ph /\ w e. NN ) -> ( f e. ( R ^m ( 1 ... ( 2 x. w ) ) ) <-> f : ( 1 ... ( 2 x. w ) ) --> R ) ) |
44 |
43
|
biimpa |
|- ( ( ( ph /\ w e. NN ) /\ f e. ( R ^m ( 1 ... ( 2 x. w ) ) ) ) -> f : ( 1 ... ( 2 x. w ) ) --> R ) |
45 |
|
simplr |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> f : ( 1 ... ( 2 x. w ) ) --> R ) |
46 |
|
elfznn |
|- ( y e. ( 1 ... w ) -> y e. NN ) |
47 |
46
|
adantl |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> y e. NN ) |
48 |
47
|
nnred |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> y e. RR ) |
49 |
|
simpllr |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> w e. NN ) |
50 |
49
|
nnred |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> w e. RR ) |
51 |
|
elfzle2 |
|- ( y e. ( 1 ... w ) -> y <_ w ) |
52 |
51
|
adantl |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> y <_ w ) |
53 |
48 50 50 52
|
leadd1dd |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( y + w ) <_ ( w + w ) ) |
54 |
49
|
nncnd |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> w e. CC ) |
55 |
54
|
2timesd |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( 2 x. w ) = ( w + w ) ) |
56 |
53 55
|
breqtrrd |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( y + w ) <_ ( 2 x. w ) ) |
57 |
47 49
|
nnaddcld |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( y + w ) e. NN ) |
58 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
59 |
57 58
|
eleqtrdi |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( y + w ) e. ( ZZ>= ` 1 ) ) |
60 |
39
|
ad2antrr |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( 2 x. w ) e. NN ) |
61 |
60
|
nnzd |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( 2 x. w ) e. ZZ ) |
62 |
|
elfz5 |
|- ( ( ( y + w ) e. ( ZZ>= ` 1 ) /\ ( 2 x. w ) e. ZZ ) -> ( ( y + w ) e. ( 1 ... ( 2 x. w ) ) <-> ( y + w ) <_ ( 2 x. w ) ) ) |
63 |
59 61 62
|
syl2anc |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( ( y + w ) e. ( 1 ... ( 2 x. w ) ) <-> ( y + w ) <_ ( 2 x. w ) ) ) |
64 |
56 63
|
mpbird |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( y + w ) e. ( 1 ... ( 2 x. w ) ) ) |
65 |
45 64
|
ffvelrnd |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( f ` ( y + w ) ) e. R ) |
66 |
|
fvoveq1 |
|- ( x = y -> ( f ` ( x + w ) ) = ( f ` ( y + w ) ) ) |
67 |
66
|
cbvmptv |
|- ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) = ( y e. ( 1 ... w ) |-> ( f ` ( y + w ) ) ) |
68 |
65 67
|
fmptd |
|- ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) : ( 1 ... w ) --> R ) |
69 |
|
ovex |
|- ( 1 ... w ) e. _V |
70 |
|
elmapg |
|- ( ( R e. Fin /\ ( 1 ... w ) e. _V ) -> ( ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) e. ( R ^m ( 1 ... w ) ) <-> ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) : ( 1 ... w ) --> R ) ) |
71 |
40 69 70
|
sylancl |
|- ( ( ph /\ w e. NN ) -> ( ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) e. ( R ^m ( 1 ... w ) ) <-> ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) : ( 1 ... w ) --> R ) ) |
72 |
71
|
biimpar |
|- ( ( ( ph /\ w e. NN ) /\ ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) : ( 1 ... w ) --> R ) -> ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) e. ( R ^m ( 1 ... w ) ) ) |
73 |
68 72
|
syldan |
|- ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) e. ( R ^m ( 1 ... w ) ) ) |
74 |
|
breq2 |
|- ( g = ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) -> ( K MonoAP g <-> K MonoAP ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) ) ) |
75 |
74
|
rspcv |
|- ( ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) e. ( R ^m ( 1 ... w ) ) -> ( A. g e. ( R ^m ( 1 ... w ) ) K MonoAP g -> K MonoAP ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) ) ) |
76 |
73 75
|
syl |
|- ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( A. g e. ( R ^m ( 1 ... w ) ) K MonoAP g -> K MonoAP ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) ) ) |
77 |
|
2nn0 |
|- 2 e. NN0 |
78 |
2
|
ad2antrr |
|- ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> K e. ( ZZ>= ` 2 ) ) |
79 |
|
eluznn0 |
|- ( ( 2 e. NN0 /\ K e. ( ZZ>= ` 2 ) ) -> K e. NN0 ) |
80 |
77 78 79
|
sylancr |
|- ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> K e. NN0 ) |
81 |
69 80 68
|
vdwmc |
|- ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( K MonoAP ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) <-> E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) |
82 |
40
|
ad2antrr |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> R e. Fin ) |
83 |
78
|
adantr |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> K e. ( ZZ>= ` 2 ) ) |
84 |
|
simpllr |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> w e. NN ) |
85 |
|
simplr |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> f : ( 1 ... ( 2 x. w ) ) --> R ) |
86 |
|
vex |
|- c e. _V |
87 |
|
simprll |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> a e. NN ) |
88 |
|
simprlr |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> d e. NN ) |
89 |
|
simprr |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) |
90 |
82 83 84 85 86 87 88 89 67
|
vdwlem8 |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> <. 1 , K >. PolyAP f ) |
91 |
90
|
orcd |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) |
92 |
91
|
expr |
|- ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( a e. NN /\ d e. NN ) ) -> ( ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) -> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
93 |
92
|
rexlimdvva |
|- ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) -> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
94 |
93
|
exlimdv |
|- ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) -> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
95 |
81 94
|
sylbid |
|- ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( K MonoAP ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) -> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
96 |
76 95
|
syld |
|- ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( A. g e. ( R ^m ( 1 ... w ) ) K MonoAP g -> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
97 |
44 96
|
syldan |
|- ( ( ( ph /\ w e. NN ) /\ f e. ( R ^m ( 1 ... ( 2 x. w ) ) ) ) -> ( A. g e. ( R ^m ( 1 ... w ) ) K MonoAP g -> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
98 |
97
|
ralrimdva |
|- ( ( ph /\ w e. NN ) -> ( A. g e. ( R ^m ( 1 ... w ) ) K MonoAP g -> A. f e. ( R ^m ( 1 ... ( 2 x. w ) ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
99 |
|
oveq2 |
|- ( n = ( 2 x. w ) -> ( 1 ... n ) = ( 1 ... ( 2 x. w ) ) ) |
100 |
99
|
oveq2d |
|- ( n = ( 2 x. w ) -> ( R ^m ( 1 ... n ) ) = ( R ^m ( 1 ... ( 2 x. w ) ) ) ) |
101 |
100
|
raleqdv |
|- ( n = ( 2 x. w ) -> ( A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> A. f e. ( R ^m ( 1 ... ( 2 x. w ) ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
102 |
101
|
rspcev |
|- ( ( ( 2 x. w ) e. NN /\ A. f e. ( R ^m ( 1 ... ( 2 x. w ) ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) |
103 |
39 98 102
|
syl6an |
|- ( ( ph /\ w e. NN ) -> ( A. g e. ( R ^m ( 1 ... w ) ) K MonoAP g -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
104 |
35 103
|
syl5bi |
|- ( ( ph /\ w e. NN ) -> ( A. f e. ( R ^m ( 1 ... w ) ) K MonoAP f -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
105 |
104
|
rexlimdva |
|- ( ph -> ( E. w e. NN A. f e. ( R ^m ( 1 ... w ) ) K MonoAP f -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
106 |
33 105
|
mpd |
|- ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) |
107 |
|
breq2 |
|- ( f = g -> ( <. m , K >. PolyAP f <-> <. m , K >. PolyAP g ) ) |
108 |
|
breq2 |
|- ( f = g -> ( ( K + 1 ) MonoAP f <-> ( K + 1 ) MonoAP g ) ) |
109 |
107 108
|
orbi12d |
|- ( f = g -> ( ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) |
110 |
109
|
cbvralvw |
|- ( A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> A. g e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) |
111 |
30
|
raleqdv |
|- ( n = w -> ( A. g e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) <-> A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) |
112 |
110 111
|
syl5bb |
|- ( n = w -> ( A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) |
113 |
112
|
cbvrexvw |
|- ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> E. w e. NN A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) |
114 |
|
oveq2 |
|- ( n = v -> ( 1 ... n ) = ( 1 ... v ) ) |
115 |
114
|
oveq2d |
|- ( n = v -> ( s ^m ( 1 ... n ) ) = ( s ^m ( 1 ... v ) ) ) |
116 |
115
|
raleqdv |
|- ( n = v -> ( A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f <-> A. f e. ( s ^m ( 1 ... v ) ) K MonoAP f ) ) |
117 |
116
|
cbvrexvw |
|- ( E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f <-> E. v e. NN A. f e. ( s ^m ( 1 ... v ) ) K MonoAP f ) |
118 |
|
oveq1 |
|- ( s = ( R ^m ( 1 ... w ) ) -> ( s ^m ( 1 ... v ) ) = ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) ) |
119 |
118
|
raleqdv |
|- ( s = ( R ^m ( 1 ... w ) ) -> ( A. f e. ( s ^m ( 1 ... v ) ) K MonoAP f <-> A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) |
120 |
119
|
rexbidv |
|- ( s = ( R ^m ( 1 ... w ) ) -> ( E. v e. NN A. f e. ( s ^m ( 1 ... v ) ) K MonoAP f <-> E. v e. NN A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) |
121 |
117 120
|
syl5bb |
|- ( s = ( R ^m ( 1 ... w ) ) -> ( E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f <-> E. v e. NN A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) |
122 |
3
|
ad2antrr |
|- ( ( ( ph /\ m e. NN ) /\ ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) -> A. s e. Fin E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f ) |
123 |
1
|
ad2antrr |
|- ( ( ( ph /\ m e. NN ) /\ ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) -> R e. Fin ) |
124 |
|
fzfi |
|- ( 1 ... w ) e. Fin |
125 |
|
mapfi |
|- ( ( R e. Fin /\ ( 1 ... w ) e. Fin ) -> ( R ^m ( 1 ... w ) ) e. Fin ) |
126 |
123 124 125
|
sylancl |
|- ( ( ( ph /\ m e. NN ) /\ ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) -> ( R ^m ( 1 ... w ) ) e. Fin ) |
127 |
121 122 126
|
rspcdva |
|- ( ( ( ph /\ m e. NN ) /\ ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) -> E. v e. NN A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) |
128 |
|
simprll |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) ) -> w e. NN ) |
129 |
|
simprrl |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) ) -> v e. NN ) |
130 |
|
nnmulcl |
|- ( ( 2 e. NN /\ v e. NN ) -> ( 2 x. v ) e. NN ) |
131 |
36 130
|
mpan |
|- ( v e. NN -> ( 2 x. v ) e. NN ) |
132 |
|
nnmulcl |
|- ( ( w e. NN /\ ( 2 x. v ) e. NN ) -> ( w x. ( 2 x. v ) ) e. NN ) |
133 |
131 132
|
sylan2 |
|- ( ( w e. NN /\ v e. NN ) -> ( w x. ( 2 x. v ) ) e. NN ) |
134 |
128 129 133
|
syl2anc |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) ) -> ( w x. ( 2 x. v ) ) e. NN ) |
135 |
|
simp1l |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> ph ) |
136 |
135 1
|
syl |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> R e. Fin ) |
137 |
135 2
|
syl |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> K e. ( ZZ>= ` 2 ) ) |
138 |
135 3
|
syl |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> A. s e. Fin E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f ) |
139 |
|
simp1r |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> m e. NN ) |
140 |
|
simp2ll |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> w e. NN ) |
141 |
|
simp2lr |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) |
142 |
|
breq2 |
|- ( g = k -> ( <. m , K >. PolyAP g <-> <. m , K >. PolyAP k ) ) |
143 |
|
breq2 |
|- ( g = k -> ( ( K + 1 ) MonoAP g <-> ( K + 1 ) MonoAP k ) ) |
144 |
142 143
|
orbi12d |
|- ( g = k -> ( ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) <-> ( <. m , K >. PolyAP k \/ ( K + 1 ) MonoAP k ) ) ) |
145 |
144
|
cbvralvw |
|- ( A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) <-> A. k e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP k \/ ( K + 1 ) MonoAP k ) ) |
146 |
141 145
|
sylib |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> A. k e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP k \/ ( K + 1 ) MonoAP k ) ) |
147 |
|
simp2rl |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> v e. NN ) |
148 |
|
simp2rr |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) |
149 |
|
simp3 |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) |
150 |
|
ovex |
|- ( 1 ... ( w x. ( 2 x. v ) ) ) e. _V |
151 |
|
elmapg |
|- ( ( R e. Fin /\ ( 1 ... ( w x. ( 2 x. v ) ) ) e. _V ) -> ( h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) <-> h : ( 1 ... ( w x. ( 2 x. v ) ) ) --> R ) ) |
152 |
136 150 151
|
sylancl |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> ( h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) <-> h : ( 1 ... ( w x. ( 2 x. v ) ) ) --> R ) ) |
153 |
149 152
|
mpbid |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> h : ( 1 ... ( w x. ( 2 x. v ) ) ) --> R ) |
154 |
|
fvoveq1 |
|- ( y = u -> ( h ` ( y + ( w x. ( ( x - 1 ) + v ) ) ) ) = ( h ` ( u + ( w x. ( ( x - 1 ) + v ) ) ) ) ) |
155 |
154
|
cbvmptv |
|- ( y e. ( 1 ... w ) |-> ( h ` ( y + ( w x. ( ( x - 1 ) + v ) ) ) ) ) = ( u e. ( 1 ... w ) |-> ( h ` ( u + ( w x. ( ( x - 1 ) + v ) ) ) ) ) |
156 |
|
oveq1 |
|- ( x = z -> ( x - 1 ) = ( z - 1 ) ) |
157 |
156
|
oveq1d |
|- ( x = z -> ( ( x - 1 ) + v ) = ( ( z - 1 ) + v ) ) |
158 |
157
|
oveq2d |
|- ( x = z -> ( w x. ( ( x - 1 ) + v ) ) = ( w x. ( ( z - 1 ) + v ) ) ) |
159 |
158
|
oveq2d |
|- ( x = z -> ( u + ( w x. ( ( x - 1 ) + v ) ) ) = ( u + ( w x. ( ( z - 1 ) + v ) ) ) ) |
160 |
159
|
fveq2d |
|- ( x = z -> ( h ` ( u + ( w x. ( ( x - 1 ) + v ) ) ) ) = ( h ` ( u + ( w x. ( ( z - 1 ) + v ) ) ) ) ) |
161 |
160
|
mpteq2dv |
|- ( x = z -> ( u e. ( 1 ... w ) |-> ( h ` ( u + ( w x. ( ( x - 1 ) + v ) ) ) ) ) = ( u e. ( 1 ... w ) |-> ( h ` ( u + ( w x. ( ( z - 1 ) + v ) ) ) ) ) ) |
162 |
155 161
|
syl5eq |
|- ( x = z -> ( y e. ( 1 ... w ) |-> ( h ` ( y + ( w x. ( ( x - 1 ) + v ) ) ) ) ) = ( u e. ( 1 ... w ) |-> ( h ` ( u + ( w x. ( ( z - 1 ) + v ) ) ) ) ) ) |
163 |
162
|
cbvmptv |
|- ( x e. ( 1 ... v ) |-> ( y e. ( 1 ... w ) |-> ( h ` ( y + ( w x. ( ( x - 1 ) + v ) ) ) ) ) ) = ( z e. ( 1 ... v ) |-> ( u e. ( 1 ... w ) |-> ( h ` ( u + ( w x. ( ( z - 1 ) + v ) ) ) ) ) ) |
164 |
136 137 138 139 140 146 147 148 153 163
|
vdwlem9 |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> ( <. ( m + 1 ) , K >. PolyAP h \/ ( K + 1 ) MonoAP h ) ) |
165 |
164
|
3expia |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) ) -> ( h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) -> ( <. ( m + 1 ) , K >. PolyAP h \/ ( K + 1 ) MonoAP h ) ) ) |
166 |
165
|
ralrimiv |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) ) -> A. h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ( <. ( m + 1 ) , K >. PolyAP h \/ ( K + 1 ) MonoAP h ) ) |
167 |
|
oveq2 |
|- ( n = ( w x. ( 2 x. v ) ) -> ( 1 ... n ) = ( 1 ... ( w x. ( 2 x. v ) ) ) ) |
168 |
167
|
oveq2d |
|- ( n = ( w x. ( 2 x. v ) ) -> ( R ^m ( 1 ... n ) ) = ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) |
169 |
168
|
raleqdv |
|- ( n = ( w x. ( 2 x. v ) ) -> ( A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> A. f e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
170 |
|
breq2 |
|- ( f = h -> ( <. ( m + 1 ) , K >. PolyAP f <-> <. ( m + 1 ) , K >. PolyAP h ) ) |
171 |
|
breq2 |
|- ( f = h -> ( ( K + 1 ) MonoAP f <-> ( K + 1 ) MonoAP h ) ) |
172 |
170 171
|
orbi12d |
|- ( f = h -> ( ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> ( <. ( m + 1 ) , K >. PolyAP h \/ ( K + 1 ) MonoAP h ) ) ) |
173 |
172
|
cbvralvw |
|- ( A. f e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> A. h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ( <. ( m + 1 ) , K >. PolyAP h \/ ( K + 1 ) MonoAP h ) ) |
174 |
169 173
|
bitrdi |
|- ( n = ( w x. ( 2 x. v ) ) -> ( A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> A. h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ( <. ( m + 1 ) , K >. PolyAP h \/ ( K + 1 ) MonoAP h ) ) ) |
175 |
174
|
rspcev |
|- ( ( ( w x. ( 2 x. v ) ) e. NN /\ A. h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ( <. ( m + 1 ) , K >. PolyAP h \/ ( K + 1 ) MonoAP h ) ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) |
176 |
134 166 175
|
syl2anc |
|- ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) |
177 |
176
|
anassrs |
|- ( ( ( ( ph /\ m e. NN ) /\ ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) |
178 |
127 177
|
rexlimddv |
|- ( ( ( ph /\ m e. NN ) /\ ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) |
179 |
178
|
rexlimdvaa |
|- ( ( ph /\ m e. NN ) -> ( E. w e. NN A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
180 |
113 179
|
syl5bi |
|- ( ( ph /\ m e. NN ) -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
181 |
180
|
expcom |
|- ( m e. NN -> ( ph -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) ) |
182 |
181
|
a2d |
|- ( m e. NN -> ( ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) -> ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) ) |
183 |
9 14 19 24 106 182
|
nnind |
|- ( M e. NN -> ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. M , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) |
184 |
4 183
|
mpcom |
|- ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. M , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) |