Metamath Proof Explorer

Theorem eldioph2b

Description: While Diophantine sets were defined to have a finite number of witness variables consequtively following the observable variables, this is not necessary; they can equivalently be taken to use any witness set ( S \ ( 1 ... N ) ) . For instance, in diophin we use this to take the two input sets to have disjoint witness sets. (Contributed by Stefan O'Rear, 8-Oct-2014)

Ref Expression
Assertion eldioph2b 
|- ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) -> ( A e. ( Dioph ` N ) <-> E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )

Proof

Step Hyp Ref Expression
1 eldiophb 
 |-  ( A e. ( Dioph ` N ) <-> ( N e. NN0 /\ E. a e. ( ZZ>= ` N ) E. b e. ( mzPoly ` ( 1 ... a ) ) A = { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } ) )
2 simp-5r 
 |-  ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> S e. _V )
3 simprr 
 |-  ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> b e. ( mzPoly ` ( 1 ... a ) ) )
4 3 ad2antrr 
 |-  ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> b e. ( mzPoly ` ( 1 ... a ) ) )
5 simprl 
 |-  ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> c : ( 1 ... a ) -1-1-> S )
6 f1f 
 |-  ( c : ( 1 ... a ) -1-1-> S -> c : ( 1 ... a ) --> S )
7 5 6 syl 
 |-  ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> c : ( 1 ... a ) --> S )
8 mzprename 
 |-  ( ( S e. _V /\ b e. ( mzPoly ` ( 1 ... a ) ) /\ c : ( 1 ... a ) --> S ) -> ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) e. ( mzPoly ` S ) )
9 2 4 7 8 syl3anc 
 |-  ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) e. ( mzPoly ` S ) )
10 simprr 
 |-  ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) )
11 diophrw 
 |-  ( ( S e. _V /\ c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) } = { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } )
12 11 eqcomd 
 |-  ( ( S e. _V /\ c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) -> { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) } )
13 2 5 10 12 syl3anc 
 |-  ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) } )
14 fveq1 
 |-  ( p = ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) -> ( p ` u ) = ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) )
15 14 eqeq1d 
 |-  ( p = ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) -> ( ( p ` u ) = 0 <-> ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) )
16 15 anbi2d 
 |-  ( p = ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) -> ( ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) <-> ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) ) )
17 16 rexbidv 
 |-  ( p = ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) -> ( E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) <-> E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) ) )
18 17 abbidv 
 |-  ( p = ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) } )
19 18 rspceeqv 
 |-  ( ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) e. ( mzPoly ` S ) /\ { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) } ) -> E. p e. ( mzPoly ` S ) { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } )
20 9 13 19 syl2anc 
 |-  ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> E. p e. ( mzPoly ` S ) { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } )
21 simplll 
 |-  ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> N e. NN0 )
22 simplrl 
 |-  ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> -. S e. Fin )
23 simplrr 
 |-  ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> ( 1 ... N ) C_ S )
24 simprl 
 |-  ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> a e. ( ZZ>= ` N ) )
25 eldioph2lem2 
 |-  ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ a e. ( ZZ>= ` N ) ) ) -> E. c ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
26 21 22 23 24 25 syl22anc 
 |-  ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> E. c ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
27 rexv 
 |-  ( E. c e. _V ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) <-> E. c ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
28 26 27 sylibr 
 |-  ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> E. c e. _V ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
29 20 28 r19.29a 
 |-  ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> E. p e. ( mzPoly ` S ) { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } )
30 eqeq1 
 |-  ( A = { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } -> ( A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } <-> { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
31 30 rexbidv 
 |-  ( A = { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } -> ( E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } <-> E. p e. ( mzPoly ` S ) { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
32 29 31 syl5ibrcom 
 |-  ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> ( A = { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } -> E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
33 32 rexlimdvva 
 |-  ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) -> ( E. a e. ( ZZ>= ` N ) E. b e. ( mzPoly ` ( 1 ... a ) ) A = { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } -> E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
34 33 adantld 
 |-  ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) -> ( ( N e. NN0 /\ E. a e. ( ZZ>= ` N ) E. b e. ( mzPoly ` ( 1 ... a ) ) A = { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } ) -> E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
35 1 34 biimtrid 
 |-  ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) -> ( A e. ( Dioph ` N ) -> E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
36 simpr 
 |-  ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) /\ A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) -> A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } )
37 simplll 
 |-  ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) -> N e. NN0 )
38 simpllr 
 |-  ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) -> S e. _V )
39 simplrr 
 |-  ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) -> ( 1 ... N ) C_ S )
40 simpr 
 |-  ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) -> p e. ( mzPoly ` S ) )
41 eldioph2 
 |-  ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) /\ p e. ( mzPoly ` S ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } e. ( Dioph ` N ) )
42 37 38 39 40 41 syl121anc 
 |-  ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } e. ( Dioph ` N ) )
43 42 adantr 
 |-  ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) /\ A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } e. ( Dioph ` N ) )
44 36 43 eqeltrd 
 |-  ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) /\ A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) -> A e. ( Dioph ` N ) )
45 44 rexlimdva2 
 |-  ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) -> ( E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } -> A e. ( Dioph ` N ) ) )
46 35 45 impbid 
 |-  ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) -> ( A e. ( Dioph ` N ) <-> E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )