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