Metamath Proof Explorer

Theorem eldioph3

Description: Inference version of eldioph3b with quantifier expanded. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion eldioph3 
|- ( ( N e. NN0 /\ P e. ( mzPoly ` NN ) ) -> { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } e. ( Dioph ` N ) )

Proof

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 ) )