Step |
Hyp |
Ref |
Expression |
1 |
|
rabdiophlem2.1 |
|- M = ( N + 1 ) |
2 |
|
nfcv |
|- F/_ a A |
3 |
|
nfcsb1v |
|- F/_ u [_ a / u ]_ A |
4 |
|
csbeq1a |
|- ( u = a -> A = [_ a / u ]_ A ) |
5 |
2 3 4
|
cbvmpt |
|- ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) = ( a e. ( ZZ ^m ( 1 ... N ) ) |-> [_ a / u ]_ A ) |
6 |
5
|
fveq1i |
|- ( ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` ( t |` ( 1 ... N ) ) ) = ( ( a e. ( ZZ ^m ( 1 ... N ) ) |-> [_ a / u ]_ A ) ` ( t |` ( 1 ... N ) ) ) |
7 |
|
eqid |
|- ( a e. ( ZZ ^m ( 1 ... N ) ) |-> [_ a / u ]_ A ) = ( a e. ( ZZ ^m ( 1 ... N ) ) |-> [_ a / u ]_ A ) |
8 |
|
csbeq1 |
|- ( a = ( t |` ( 1 ... N ) ) -> [_ a / u ]_ A = [_ ( t |` ( 1 ... N ) ) / u ]_ A ) |
9 |
1
|
mapfzcons1cl |
|- ( t e. ( ZZ ^m ( 1 ... M ) ) -> ( t |` ( 1 ... N ) ) e. ( ZZ ^m ( 1 ... N ) ) ) |
10 |
9
|
adantl |
|- ( ( ( N e. NN0 /\ ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( ZZ ^m ( 1 ... M ) ) ) -> ( t |` ( 1 ... N ) ) e. ( ZZ ^m ( 1 ... N ) ) ) |
11 |
|
mzpf |
|- ( ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) -> ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) : ( ZZ ^m ( 1 ... N ) ) --> ZZ ) |
12 |
|
eqid |
|- ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) = ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) |
13 |
12
|
fmpt |
|- ( A. u e. ( ZZ ^m ( 1 ... N ) ) A e. ZZ <-> ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) : ( ZZ ^m ( 1 ... N ) ) --> ZZ ) |
14 |
11 13
|
sylibr |
|- ( ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) -> A. u e. ( ZZ ^m ( 1 ... N ) ) A e. ZZ ) |
15 |
14
|
ad2antlr |
|- ( ( ( N e. NN0 /\ ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( ZZ ^m ( 1 ... M ) ) ) -> A. u e. ( ZZ ^m ( 1 ... N ) ) A e. ZZ ) |
16 |
|
nfcsb1v |
|- F/_ u [_ ( t |` ( 1 ... N ) ) / u ]_ A |
17 |
16
|
nfel1 |
|- F/ u [_ ( t |` ( 1 ... N ) ) / u ]_ A e. ZZ |
18 |
|
csbeq1a |
|- ( u = ( t |` ( 1 ... N ) ) -> A = [_ ( t |` ( 1 ... N ) ) / u ]_ A ) |
19 |
18
|
eleq1d |
|- ( u = ( t |` ( 1 ... N ) ) -> ( A e. ZZ <-> [_ ( t |` ( 1 ... N ) ) / u ]_ A e. ZZ ) ) |
20 |
17 19
|
rspc |
|- ( ( t |` ( 1 ... N ) ) e. ( ZZ ^m ( 1 ... N ) ) -> ( A. u e. ( ZZ ^m ( 1 ... N ) ) A e. ZZ -> [_ ( t |` ( 1 ... N ) ) / u ]_ A e. ZZ ) ) |
21 |
10 15 20
|
sylc |
|- ( ( ( N e. NN0 /\ ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( ZZ ^m ( 1 ... M ) ) ) -> [_ ( t |` ( 1 ... N ) ) / u ]_ A e. ZZ ) |
22 |
7 8 10 21
|
fvmptd3 |
|- ( ( ( N e. NN0 /\ ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( ZZ ^m ( 1 ... M ) ) ) -> ( ( a e. ( ZZ ^m ( 1 ... N ) ) |-> [_ a / u ]_ A ) ` ( t |` ( 1 ... N ) ) ) = [_ ( t |` ( 1 ... N ) ) / u ]_ A ) |
23 |
6 22
|
syl5req |
|- ( ( ( N e. NN0 /\ ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( ZZ ^m ( 1 ... M ) ) ) -> [_ ( t |` ( 1 ... N ) ) / u ]_ A = ( ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` ( t |` ( 1 ... N ) ) ) ) |
24 |
23
|
mpteq2dva |
|- ( ( N e. NN0 /\ ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( t e. ( ZZ ^m ( 1 ... M ) ) |-> [_ ( t |` ( 1 ... N ) ) / u ]_ A ) = ( t e. ( ZZ ^m ( 1 ... M ) ) |-> ( ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` ( t |` ( 1 ... N ) ) ) ) ) |
25 |
|
ovexd |
|- ( ( N e. NN0 /\ ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( 1 ... M ) e. _V ) |
26 |
|
fzssp1 |
|- ( 1 ... N ) C_ ( 1 ... ( N + 1 ) ) |
27 |
1
|
oveq2i |
|- ( 1 ... M ) = ( 1 ... ( N + 1 ) ) |
28 |
26 27
|
sseqtrri |
|- ( 1 ... N ) C_ ( 1 ... M ) |
29 |
28
|
a1i |
|- ( ( N e. NN0 /\ ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( 1 ... N ) C_ ( 1 ... M ) ) |
30 |
|
simpr |
|- ( ( N e. NN0 /\ ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) |
31 |
|
mzpresrename |
|- ( ( ( 1 ... M ) e. _V /\ ( 1 ... N ) C_ ( 1 ... M ) /\ ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( t e. ( ZZ ^m ( 1 ... M ) ) |-> ( ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` ( t |` ( 1 ... N ) ) ) ) e. ( mzPoly ` ( 1 ... M ) ) ) |
32 |
25 29 30 31
|
syl3anc |
|- ( ( N e. NN0 /\ ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( t e. ( ZZ ^m ( 1 ... M ) ) |-> ( ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` ( t |` ( 1 ... N ) ) ) ) e. ( mzPoly ` ( 1 ... M ) ) ) |
33 |
24 32
|
eqeltrd |
|- ( ( N e. NN0 /\ ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( t e. ( ZZ ^m ( 1 ... M ) ) |-> [_ ( t |` ( 1 ... N ) ) / u ]_ A ) e. ( mzPoly ` ( 1 ... M ) ) ) |