Metamath Proof Explorer

Theorem eqrabdioph

Description: Diophantine set builder for equality of polynomial expressions. Note that the two expressions need not be nonnegative; only variables are so constrained. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion eqrabdioph 
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A = B } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 nfmpt1 
 |-  F/_ t ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A )
2 1 nfel1 
 |-  F/ t ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) )
3 nfmpt1 
 |-  F/_ t ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B )
4 3 nfel1 
 |-  F/ t ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) )
5 2 4 nfan 
 |-  F/ t ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) )
6 mzpf 
 |-  ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) -> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) : ( ZZ ^m ( 1 ... N ) ) --> ZZ )
7 6 ad2antrr 
 |-  ( ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) : ( ZZ ^m ( 1 ... N ) ) --> ZZ )
8 zex 
 |-  ZZ e. _V
9 nn0ssz 
 |-  NN0 C_ ZZ
10 mapss 
 |-  ( ( ZZ e. _V /\ NN0 C_ ZZ ) -> ( NN0 ^m ( 1 ... N ) ) C_ ( ZZ ^m ( 1 ... N ) ) )
11 8 9 10 mp2an 
 |-  ( NN0 ^m ( 1 ... N ) ) C_ ( ZZ ^m ( 1 ... N ) )
12 11 sseli 
 |-  ( t e. ( NN0 ^m ( 1 ... N ) ) -> t e. ( ZZ ^m ( 1 ... N ) ) )
13 12 adantl 
 |-  ( ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> t e. ( ZZ ^m ( 1 ... N ) ) )
14 mptfcl 
 |-  ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) : ( ZZ ^m ( 1 ... N ) ) --> ZZ -> ( t e. ( ZZ ^m ( 1 ... N ) ) -> A e. ZZ ) )
15 7 13 14 sylc 
 |-  ( ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> A e. ZZ )
16 15 zcnd 
 |-  ( ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> A e. CC )
17 mzpf 
 |-  ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) -> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) : ( ZZ ^m ( 1 ... N ) ) --> ZZ )
18 17 ad2antlr 
 |-  ( ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) : ( ZZ ^m ( 1 ... N ) ) --> ZZ )
19 mptfcl 
 |-  ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) : ( ZZ ^m ( 1 ... N ) ) --> ZZ -> ( t e. ( ZZ ^m ( 1 ... N ) ) -> B e. ZZ ) )
20 18 13 19 sylc 
 |-  ( ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> B e. ZZ )
21 20 zcnd 
 |-  ( ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> B e. CC )
22 16 21 subeq0ad 
 |-  ( ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> ( ( A - B ) = 0 <-> A = B ) )
23 22 bicomd 
 |-  ( ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> ( A = B <-> ( A - B ) = 0 ) )
24 23 ex 
 |-  ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( t e. ( NN0 ^m ( 1 ... N ) ) -> ( A = B <-> ( A - B ) = 0 ) ) )
25 5 24 ralrimi 
 |-  ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) ( A = B <-> ( A - B ) = 0 ) )
26 rabbi 
 |-  ( A. t e. ( NN0 ^m ( 1 ... N ) ) ( A = B <-> ( A - B ) = 0 ) <-> { t e. ( NN0 ^m ( 1 ... N ) ) | A = B } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( A - B ) = 0 } )
27 25 26 sylib 
 |-  ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A = B } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( A - B ) = 0 } )
28 27 3adant1 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A = B } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( A - B ) = 0 } )
29 simp1 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> N e. NN0 )
30 mzpsubmpt 
 |-  ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> ( A - B ) ) e. ( mzPoly ` ( 1 ... N ) ) )
31 30 3adant1 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> ( A - B ) ) e. ( mzPoly ` ( 1 ... N ) ) )
32 eq0rabdioph 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> ( A - B ) ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( A - B ) = 0 } e. ( Dioph ` N ) )
33 29 31 32 syl2anc 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( A - B ) = 0 } e. ( Dioph ` N ) )
34 28 33 eqeltrd 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A = B } e. ( Dioph ` N ) )