Metamath Proof Explorer

Theorem rabdiophlem2

Description: Lemma for arithmetic diophantine sets. Reuse a polynomial expression under a new quantifier. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Hypothesis rabdiophlem2.1 
|- M = ( N + 1 )
Assertion rabdiophlem2 
|- ( ( 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 ) ) )

Proof

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