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 syl5bi
 |-  ( ( ( 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 ) } ) )