Metamath Proof Explorer

Theorem diophrex

Description: Projecting a Diophantine set by removing a coordinate results in a Diophantine set. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion diophrex 
|- ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) -> { t | E. u e. S t = ( u |` ( 1 ... N ) ) } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( a = t -> ( a = ( b |` ( 1 ... N ) ) <-> t = ( b |` ( 1 ... N ) ) ) )
2 1 rexbidv 
 |-  ( a = t -> ( E. b e. S a = ( b |` ( 1 ... N ) ) <-> E. b e. S t = ( b |` ( 1 ... N ) ) ) )
3 reseq1 
 |-  ( b = u -> ( b |` ( 1 ... N ) ) = ( u |` ( 1 ... N ) ) )
4 3 eqeq2d 
 |-  ( b = u -> ( t = ( b |` ( 1 ... N ) ) <-> t = ( u |` ( 1 ... N ) ) ) )
5 4 cbvrexvw 
 |-  ( E. b e. S t = ( b |` ( 1 ... N ) ) <-> E. u e. S t = ( u |` ( 1 ... N ) ) )
6 2 5 bitrdi 
 |-  ( a = t -> ( E. b e. S a = ( b |` ( 1 ... N ) ) <-> E. u e. S t = ( u |` ( 1 ... N ) ) ) )
7 6 cbvabv 
 |-  { a | E. b e. S a = ( b |` ( 1 ... N ) ) } = { t | E. u e. S t = ( u |` ( 1 ... N ) ) }
8 rexeq 
 |-  ( S = { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } -> ( E. b e. S a = ( b |` ( 1 ... N ) ) <-> E. b e. { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } a = ( b |` ( 1 ... N ) ) ) )
9 8 abbidv 
 |-  ( S = { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } -> { a | E. b e. S a = ( b |` ( 1 ... N ) ) } = { a | E. b e. { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } a = ( b |` ( 1 ... N ) ) } )
10 9 adantl 
 |-  ( ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) /\ S = { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } ) -> { a | E. b e. S a = ( b |` ( 1 ... N ) ) } = { a | E. b e. { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } a = ( b |` ( 1 ... N ) ) } )
11 eqeq1 
 |-  ( d = b -> ( d = ( e |` ( 1 ... M ) ) <-> b = ( e |` ( 1 ... M ) ) ) )
12 11 anbi1d 
 |-  ( d = b -> ( ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) <-> ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) ) )
13 12 rexbidv 
 |-  ( d = b -> ( E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) <-> E. e e. ( NN0 ^m NN ) ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) ) )
14 13 rexab 
 |-  ( E. b e. { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } a = ( b |` ( 1 ... N ) ) <-> E. b ( E. e e. ( NN0 ^m NN ) ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) /\ a = ( b |` ( 1 ... N ) ) ) )
15 r19.41v 
 |-  ( E. e e. ( NN0 ^m NN ) ( ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) /\ a = ( b |` ( 1 ... N ) ) ) <-> ( E. e e. ( NN0 ^m NN ) ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) /\ a = ( b |` ( 1 ... N ) ) ) )
16 15 exbii 
 |-  ( E. b E. e e. ( NN0 ^m NN ) ( ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) /\ a = ( b |` ( 1 ... N ) ) ) <-> E. b ( E. e e. ( NN0 ^m NN ) ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) /\ a = ( b |` ( 1 ... N ) ) ) )
17 rexcom4 
 |-  ( E. e e. ( NN0 ^m NN ) E. b ( ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) /\ a = ( b |` ( 1 ... N ) ) ) <-> E. b E. e e. ( NN0 ^m NN ) ( ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) /\ a = ( b |` ( 1 ... N ) ) ) )
18 anass 
 |-  ( ( ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) /\ a = ( b |` ( 1 ... N ) ) ) <-> ( b = ( e |` ( 1 ... M ) ) /\ ( ( c ` e ) = 0 /\ a = ( b |` ( 1 ... N ) ) ) ) )
19 18 exbii 
 |-  ( E. b ( ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) /\ a = ( b |` ( 1 ... N ) ) ) <-> E. b ( b = ( e |` ( 1 ... M ) ) /\ ( ( c ` e ) = 0 /\ a = ( b |` ( 1 ... N ) ) ) ) )
20 vex 
 |-  e e. _V
21 20 resex 
 |-  ( e |` ( 1 ... M ) ) e. _V
22 reseq1 
 |-  ( b = ( e |` ( 1 ... M ) ) -> ( b |` ( 1 ... N ) ) = ( ( e |` ( 1 ... M ) ) |` ( 1 ... N ) ) )
23 22 eqeq2d 
 |-  ( b = ( e |` ( 1 ... M ) ) -> ( a = ( b |` ( 1 ... N ) ) <-> a = ( ( e |` ( 1 ... M ) ) |` ( 1 ... N ) ) ) )
24 23 anbi2d 
 |-  ( b = ( e |` ( 1 ... M ) ) -> ( ( ( c ` e ) = 0 /\ a = ( b |` ( 1 ... N ) ) ) <-> ( ( c ` e ) = 0 /\ a = ( ( e |` ( 1 ... M ) ) |` ( 1 ... N ) ) ) ) )
25 21 24 ceqsexv 
 |-  ( E. b ( b = ( e |` ( 1 ... M ) ) /\ ( ( c ` e ) = 0 /\ a = ( b |` ( 1 ... N ) ) ) ) <-> ( ( c ` e ) = 0 /\ a = ( ( e |` ( 1 ... M ) ) |` ( 1 ... N ) ) ) )
26 19 25 bitri 
 |-  ( E. b ( ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) /\ a = ( b |` ( 1 ... N ) ) ) <-> ( ( c ` e ) = 0 /\ a = ( ( e |` ( 1 ... M ) ) |` ( 1 ... N ) ) ) )
27 ancom 
 |-  ( ( ( c ` e ) = 0 /\ a = ( ( e |` ( 1 ... M ) ) |` ( 1 ... N ) ) ) <-> ( a = ( ( e |` ( 1 ... M ) ) |` ( 1 ... N ) ) /\ ( c ` e ) = 0 ) )
28 simpl2 
 |-  ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) -> M e. ( ZZ>= ` N ) )
29 fzss2 
 |-  ( M e. ( ZZ>= ` N ) -> ( 1 ... N ) C_ ( 1 ... M ) )
30 resabs1 
 |-  ( ( 1 ... N ) C_ ( 1 ... M ) -> ( ( e |` ( 1 ... M ) ) |` ( 1 ... N ) ) = ( e |` ( 1 ... N ) ) )
31 28 29 30 3syl 
 |-  ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) -> ( ( e |` ( 1 ... M ) ) |` ( 1 ... N ) ) = ( e |` ( 1 ... N ) ) )
32 31 eqeq2d 
 |-  ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) -> ( a = ( ( e |` ( 1 ... M ) ) |` ( 1 ... N ) ) <-> a = ( e |` ( 1 ... N ) ) ) )
33 32 anbi1d 
 |-  ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) -> ( ( a = ( ( e |` ( 1 ... M ) ) |` ( 1 ... N ) ) /\ ( c ` e ) = 0 ) <-> ( a = ( e |` ( 1 ... N ) ) /\ ( c ` e ) = 0 ) ) )
34 27 33 syl5bb 
 |-  ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) -> ( ( ( c ` e ) = 0 /\ a = ( ( e |` ( 1 ... M ) ) |` ( 1 ... N ) ) ) <-> ( a = ( e |` ( 1 ... N ) ) /\ ( c ` e ) = 0 ) ) )
35 26 34 syl5bb 
 |-  ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) -> ( E. b ( ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) /\ a = ( b |` ( 1 ... N ) ) ) <-> ( a = ( e |` ( 1 ... N ) ) /\ ( c ` e ) = 0 ) ) )
36 35 rexbidv 
 |-  ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) -> ( E. e e. ( NN0 ^m NN ) E. b ( ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) /\ a = ( b |` ( 1 ... N ) ) ) <-> E. e e. ( NN0 ^m NN ) ( a = ( e |` ( 1 ... N ) ) /\ ( c ` e ) = 0 ) ) )
37 17 36 bitr3id 
 |-  ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) -> ( E. b E. e e. ( NN0 ^m NN ) ( ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) /\ a = ( b |` ( 1 ... N ) ) ) <-> E. e e. ( NN0 ^m NN ) ( a = ( e |` ( 1 ... N ) ) /\ ( c ` e ) = 0 ) ) )
38 16 37 bitr3id 
 |-  ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) -> ( E. b ( E. e e. ( NN0 ^m NN ) ( b = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) /\ a = ( b |` ( 1 ... N ) ) ) <-> E. e e. ( NN0 ^m NN ) ( a = ( e |` ( 1 ... N ) ) /\ ( c ` e ) = 0 ) ) )
39 14 38 syl5bb 
 |-  ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) -> ( E. b e. { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } a = ( b |` ( 1 ... N ) ) <-> E. e e. ( NN0 ^m NN ) ( a = ( e |` ( 1 ... N ) ) /\ ( c ` e ) = 0 ) ) )
40 39 abbidv 
 |-  ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) -> { a | E. b e. { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } a = ( b |` ( 1 ... N ) ) } = { a | E. e e. ( NN0 ^m NN ) ( a = ( e |` ( 1 ... N ) ) /\ ( c ` e ) = 0 ) } )
41 eldioph3 
 |-  ( ( N e. NN0 /\ c e. ( mzPoly ` NN ) ) -> { a | E. e e. ( NN0 ^m NN ) ( a = ( e |` ( 1 ... N ) ) /\ ( c ` e ) = 0 ) } e. ( Dioph ` N ) )
42 41 3ad2antl1 
 |-  ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) -> { a | E. e e. ( NN0 ^m NN ) ( a = ( e |` ( 1 ... N ) ) /\ ( c ` e ) = 0 ) } e. ( Dioph ` N ) )
43 40 42 eqeltrd 
 |-  ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) -> { a | E. b e. { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } a = ( b |` ( 1 ... N ) ) } e. ( Dioph ` N ) )
44 43 adantr 
 |-  ( ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) /\ S = { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } ) -> { a | E. b e. { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } a = ( b |` ( 1 ... N ) ) } e. ( Dioph ` N ) )
45 10 44 eqeltrd 
 |-  ( ( ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) /\ c e. ( mzPoly ` NN ) ) /\ S = { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } ) -> { a | E. b e. S a = ( b |` ( 1 ... N ) ) } e. ( Dioph ` N ) )
46 eldioph3b 
 |-  ( S e. ( Dioph ` M ) <-> ( M e. NN0 /\ E. c e. ( mzPoly ` NN ) S = { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } ) )
47 46 simprbi 
 |-  ( S e. ( Dioph ` M ) -> E. c e. ( mzPoly ` NN ) S = { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } )
48 47 3ad2ant3 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) -> E. c e. ( mzPoly ` NN ) S = { d | E. e e. ( NN0 ^m NN ) ( d = ( e |` ( 1 ... M ) ) /\ ( c ` e ) = 0 ) } )
49 45 48 r19.29a 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) -> { a | E. b e. S a = ( b |` ( 1 ... N ) ) } e. ( Dioph ` N ) )
50 7 49 eqeltrrid 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) -> { t | E. u e. S t = ( u |` ( 1 ... N ) ) } e. ( Dioph ` N ) )