Metamath Proof Explorer

Theorem eq0rabdioph

Description: This is the first of a number of theorems which allow sets to be proven Diophantine by syntactic induction, and models the correspondence between Diophantine sets and monotone existential first-order logic. This first theorem shows that the zero set of an implicit polynomial is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ t N e. NN0
2 nfmpt1 
 |-  F/_ t ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A )
3 2 nfel1 
 |-  F/ t ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) )
4 1 3 nfan 
 |-  F/ t ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) )
5 zex 
 |-  ZZ e. _V
6 nn0ssz 
 |-  NN0 C_ ZZ
7 mapss 
 |-  ( ( ZZ e. _V /\ NN0 C_ ZZ ) -> ( NN0 ^m ( 1 ... N ) ) C_ ( ZZ ^m ( 1 ... N ) ) )
8 5 6 7 mp2an 
 |-  ( NN0 ^m ( 1 ... N ) ) C_ ( ZZ ^m ( 1 ... N ) )
9 8 sseli 
 |-  ( t e. ( NN0 ^m ( 1 ... N ) ) -> t e. ( ZZ ^m ( 1 ... N ) ) )
10 9 adantl 
 |-  ( ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> t e. ( ZZ ^m ( 1 ... N ) ) )
11 mzpf 
 |-  ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) -> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) : ( ZZ ^m ( 1 ... N ) ) --> ZZ )
12 mptfcl 
 |-  ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) : ( ZZ ^m ( 1 ... N ) ) --> ZZ -> ( t e. ( ZZ ^m ( 1 ... N ) ) -> A e. ZZ ) )
13 12 imp 
 |-  ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) : ( ZZ ^m ( 1 ... N ) ) --> ZZ /\ t e. ( ZZ ^m ( 1 ... N ) ) ) -> A e. ZZ )
14 11 9 13 syl2an 
 |-  ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> A e. ZZ )
15 14 adantll 
 |-  ( ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> A e. ZZ )
16 eqid 
 |-  ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) = ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A )
17 16 fvmpt2 
 |-  ( ( t e. ( ZZ ^m ( 1 ... N ) ) /\ A e. ZZ ) -> ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` t ) = A )
18 10 15 17 syl2anc 
 |-  ( ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` t ) = A )
19 18 eqcomd 
 |-  ( ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> A = ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` t ) )
20 19 eqeq1d 
 |-  ( ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> ( A = 0 <-> ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` t ) = 0 ) )
21 20 ex 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( t e. ( NN0 ^m ( 1 ... N ) ) -> ( A = 0 <-> ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` t ) = 0 ) ) )
22 4 21 ralrimi 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) ( A = 0 <-> ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` t ) = 0 ) )
23 rabbi 
 |-  ( A. t e. ( NN0 ^m ( 1 ... N ) ) ( A = 0 <-> ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` t ) = 0 ) <-> { t e. ( NN0 ^m ( 1 ... N ) ) | A = 0 } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` t ) = 0 } )
24 22 23 sylib 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A = 0 } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` t ) = 0 } )
25 nfcv 
 |-  F/_ t ( NN0 ^m ( 1 ... N ) )
26 nfcv 
 |-  F/_ a ( NN0 ^m ( 1 ... N ) )
27 nfv 
 |-  F/ a ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` t ) = 0
28 nffvmpt1 
 |-  F/_ t ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` a )
29 28 nfeq1 
 |-  F/ t ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` a ) = 0
30 fveqeq2 
 |-  ( t = a -> ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` t ) = 0 <-> ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` a ) = 0 ) )
31 25 26 27 29 30 cbvrabw 
 |-  { t e. ( NN0 ^m ( 1 ... N ) ) | ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` t ) = 0 } = { a e. ( NN0 ^m ( 1 ... N ) ) | ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` a ) = 0 }
32 24 31 eqtrdi 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A = 0 } = { a e. ( NN0 ^m ( 1 ... N ) ) | ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` a ) = 0 } )
33 df-rab 
 |-  { a e. ( NN0 ^m ( 1 ... N ) ) | ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` a ) = 0 } = { a | ( a e. ( NN0 ^m ( 1 ... N ) ) /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` a ) = 0 ) }
34 32 33 eqtrdi 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A = 0 } = { a | ( a e. ( NN0 ^m ( 1 ... N ) ) /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` a ) = 0 ) } )
35 elmapi 
 |-  ( b e. ( NN0 ^m ( 1 ... N ) ) -> b : ( 1 ... N ) --> NN0 )
36 ffn 
 |-  ( b : ( 1 ... N ) --> NN0 -> b Fn ( 1 ... N ) )
37 fnresdm 
 |-  ( b Fn ( 1 ... N ) -> ( b |` ( 1 ... N ) ) = b )
38 35 36 37 3syl 
 |-  ( b e. ( NN0 ^m ( 1 ... N ) ) -> ( b |` ( 1 ... N ) ) = b )
39 38 eqeq2d 
 |-  ( b e. ( NN0 ^m ( 1 ... N ) ) -> ( a = ( b |` ( 1 ... N ) ) <-> a = b ) )
40 equcom 
 |-  ( a = b <-> b = a )
41 39 40 syl6bb 
 |-  ( b e. ( NN0 ^m ( 1 ... N ) ) -> ( a = ( b |` ( 1 ... N ) ) <-> b = a ) )
42 41 anbi1d 
 |-  ( b e. ( NN0 ^m ( 1 ... N ) ) -> ( ( a = ( b |` ( 1 ... N ) ) /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` b ) = 0 ) <-> ( b = a /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` b ) = 0 ) ) )
43 42 rexbiia 
 |-  ( E. b e. ( NN0 ^m ( 1 ... N ) ) ( a = ( b |` ( 1 ... N ) ) /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` b ) = 0 ) <-> E. b e. ( NN0 ^m ( 1 ... N ) ) ( b = a /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` b ) = 0 ) )
44 fveqeq2 
 |-  ( b = a -> ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` b ) = 0 <-> ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` a ) = 0 ) )
45 44 ceqsrexbv 
 |-  ( E. b e. ( NN0 ^m ( 1 ... N ) ) ( b = a /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` b ) = 0 ) <-> ( a e. ( NN0 ^m ( 1 ... N ) ) /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` a ) = 0 ) )
46 43 45 bitr2i 
 |-  ( ( a e. ( NN0 ^m ( 1 ... N ) ) /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` a ) = 0 ) <-> E. b e. ( NN0 ^m ( 1 ... N ) ) ( a = ( b |` ( 1 ... N ) ) /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` b ) = 0 ) )
47 46 abbii 
 |-  { a | ( a e. ( NN0 ^m ( 1 ... N ) ) /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` a ) = 0 ) } = { a | E. b e. ( NN0 ^m ( 1 ... N ) ) ( a = ( b |` ( 1 ... N ) ) /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` b ) = 0 ) }
48 34 47 eqtrdi 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A = 0 } = { a | E. b e. ( NN0 ^m ( 1 ... N ) ) ( a = ( b |` ( 1 ... N ) ) /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` b ) = 0 ) } )
49 simpl 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> N e. NN0 )
50 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
51 uzid 
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
52 50 51 syl 
 |-  ( N e. NN0 -> N e. ( ZZ>= ` N ) )
53 52 adantr 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> N e. ( ZZ>= ` N ) )
54 simpr 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) )
55 eldioph 
 |-  ( ( N e. NN0 /\ N e. ( ZZ>= ` N ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { a | E. b e. ( NN0 ^m ( 1 ... N ) ) ( a = ( b |` ( 1 ... N ) ) /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` b ) = 0 ) } e. ( Dioph ` N ) )
56 49 53 54 55 syl3anc 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { a | E. b e. ( NN0 ^m ( 1 ... N ) ) ( a = ( b |` ( 1 ... N ) ) /\ ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) ` b ) = 0 ) } e. ( Dioph ` N ) )
57 48 56 eqeltrd 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A = 0 } e. ( Dioph ` N ) )