Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( N e. NN0 /\ P e. ( mzPoly ` NN ) ) -> N e. NN0 ) |
2 |
|
simpr |
|- ( ( N e. NN0 /\ P e. ( mzPoly ` NN ) ) -> P e. ( mzPoly ` NN ) ) |
3 |
|
eqidd |
|- ( ( N e. NN0 /\ P e. ( mzPoly ` NN ) ) -> { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } = { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } ) |
4 |
|
fveq1 |
|- ( p = P -> ( p ` b ) = ( P ` b ) ) |
5 |
4
|
eqeq1d |
|- ( p = P -> ( ( p ` b ) = 0 <-> ( P ` b ) = 0 ) ) |
6 |
5
|
anbi2d |
|- ( p = P -> ( ( a = ( b |` ( 1 ... N ) ) /\ ( p ` b ) = 0 ) <-> ( a = ( b |` ( 1 ... N ) ) /\ ( P ` b ) = 0 ) ) ) |
7 |
6
|
rexbidv |
|- ( p = P -> ( E. b e. ( NN0 ^m NN ) ( a = ( b |` ( 1 ... N ) ) /\ ( p ` b ) = 0 ) <-> E. b e. ( NN0 ^m NN ) ( a = ( b |` ( 1 ... N ) ) /\ ( P ` b ) = 0 ) ) ) |
8 |
7
|
abbidv |
|- ( p = P -> { a | E. b e. ( NN0 ^m NN ) ( a = ( b |` ( 1 ... N ) ) /\ ( p ` b ) = 0 ) } = { a | E. b e. ( NN0 ^m NN ) ( a = ( b |` ( 1 ... N ) ) /\ ( P ` b ) = 0 ) } ) |
9 |
|
eqeq1 |
|- ( a = t -> ( a = ( b |` ( 1 ... N ) ) <-> t = ( b |` ( 1 ... N ) ) ) ) |
10 |
9
|
anbi1d |
|- ( a = t -> ( ( a = ( b |` ( 1 ... N ) ) /\ ( P ` b ) = 0 ) <-> ( t = ( b |` ( 1 ... N ) ) /\ ( P ` b ) = 0 ) ) ) |
11 |
10
|
rexbidv |
|- ( a = t -> ( E. b e. ( NN0 ^m NN ) ( a = ( b |` ( 1 ... N ) ) /\ ( P ` b ) = 0 ) <-> E. b e. ( NN0 ^m NN ) ( t = ( b |` ( 1 ... N ) ) /\ ( P ` b ) = 0 ) ) ) |
12 |
|
reseq1 |
|- ( b = u -> ( b |` ( 1 ... N ) ) = ( u |` ( 1 ... N ) ) ) |
13 |
12
|
eqeq2d |
|- ( b = u -> ( t = ( b |` ( 1 ... N ) ) <-> t = ( u |` ( 1 ... N ) ) ) ) |
14 |
|
fveqeq2 |
|- ( b = u -> ( ( P ` b ) = 0 <-> ( P ` u ) = 0 ) ) |
15 |
13 14
|
anbi12d |
|- ( b = u -> ( ( t = ( b |` ( 1 ... N ) ) /\ ( P ` b ) = 0 ) <-> ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) ) ) |
16 |
15
|
cbvrexvw |
|- ( E. b e. ( NN0 ^m NN ) ( t = ( b |` ( 1 ... N ) ) /\ ( P ` b ) = 0 ) <-> E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) ) |
17 |
11 16
|
bitrdi |
|- ( a = t -> ( E. b e. ( NN0 ^m NN ) ( a = ( b |` ( 1 ... N ) ) /\ ( P ` b ) = 0 ) <-> E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) ) ) |
18 |
17
|
cbvabv |
|- { a | E. b e. ( NN0 ^m NN ) ( a = ( b |` ( 1 ... N ) ) /\ ( P ` b ) = 0 ) } = { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } |
19 |
8 18
|
eqtrdi |
|- ( p = P -> { a | E. b e. ( NN0 ^m NN ) ( a = ( b |` ( 1 ... N ) ) /\ ( p ` b ) = 0 ) } = { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } ) |
20 |
19
|
rspceeqv |
|- ( ( P e. ( mzPoly ` NN ) /\ { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } = { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } ) -> E. p e. ( mzPoly ` NN ) { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } = { a | E. b e. ( NN0 ^m NN ) ( a = ( b |` ( 1 ... N ) ) /\ ( p ` b ) = 0 ) } ) |
21 |
2 3 20
|
syl2anc |
|- ( ( N e. NN0 /\ P e. ( mzPoly ` NN ) ) -> E. p e. ( mzPoly ` NN ) { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } = { a | E. b e. ( NN0 ^m NN ) ( a = ( b |` ( 1 ... N ) ) /\ ( p ` b ) = 0 ) } ) |
22 |
|
eldioph3b |
|- ( { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } e. ( Dioph ` N ) <-> ( N e. NN0 /\ E. p e. ( mzPoly ` NN ) { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } = { a | E. b e. ( NN0 ^m NN ) ( a = ( b |` ( 1 ... N ) ) /\ ( p ` b ) = 0 ) } ) ) |
23 |
1 21 22
|
sylanbrc |
|- ( ( N e. NN0 /\ P e. ( mzPoly ` NN ) ) -> { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } e. ( Dioph ` N ) ) |