Metamath Proof Explorer

Theorem eldioph4i

Description: Forward-only version of eldioph4b . (Contributed by Stefan O'Rear, 16-Oct-2014)

Ref Expression
Hypotheses eldioph4b.a 
|- W e. _V
eldioph4b.b 
|- -. W e. Fin
eldioph4b.c 
|- ( W i^i NN ) = (/)
Assertion eldioph4i 
|- ( ( N e. NN0 /\ P e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( P ` ( t u. w ) ) = 0 } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 eldioph4b.a 
 |-  W e. _V
2 eldioph4b.b 
 |-  -. W e. Fin
3 eldioph4b.c 
 |-  ( W i^i NN ) = (/)
4 uneq1 
 |-  ( t = a -> ( t u. w ) = ( a u. w ) )
5 4 fveqeq2d 
 |-  ( t = a -> ( ( P ` ( t u. w ) ) = 0 <-> ( P ` ( a u. w ) ) = 0 ) )
6 5 rexbidv 
 |-  ( t = a -> ( E. w e. ( NN0 ^m W ) ( P ` ( t u. w ) ) = 0 <-> E. w e. ( NN0 ^m W ) ( P ` ( a u. w ) ) = 0 ) )
7 uneq2 
 |-  ( w = b -> ( a u. w ) = ( a u. b ) )
8 7 fveqeq2d 
 |-  ( w = b -> ( ( P ` ( a u. w ) ) = 0 <-> ( P ` ( a u. b ) ) = 0 ) )
9 8 cbvrexvw 
 |-  ( E. w e. ( NN0 ^m W ) ( P ` ( a u. w ) ) = 0 <-> E. b e. ( NN0 ^m W ) ( P ` ( a u. b ) ) = 0 )
10 6 9 bitrdi 
 |-  ( t = a -> ( E. w e. ( NN0 ^m W ) ( P ` ( t u. w ) ) = 0 <-> E. b e. ( NN0 ^m W ) ( P ` ( a u. b ) ) = 0 ) )
11 10 cbvrabv 
 |-  { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( P ` ( t u. w ) ) = 0 } = { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. ( NN0 ^m W ) ( P ` ( a u. b ) ) = 0 }
12 fveq1 
 |-  ( p = P -> ( p ` ( a u. b ) ) = ( P ` ( a u. b ) ) )
13 12 eqeq1d 
 |-  ( p = P -> ( ( p ` ( a u. b ) ) = 0 <-> ( P ` ( a u. b ) ) = 0 ) )
14 13 rexbidv 
 |-  ( p = P -> ( E. b e. ( NN0 ^m W ) ( p ` ( a u. b ) ) = 0 <-> E. b e. ( NN0 ^m W ) ( P ` ( a u. b ) ) = 0 ) )
15 14 rabbidv 
 |-  ( p = P -> { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. ( NN0 ^m W ) ( p ` ( a u. b ) ) = 0 } = { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. ( NN0 ^m W ) ( P ` ( a u. b ) ) = 0 } )
16 15 rspceeqv 
 |-  ( ( P e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( P ` ( t u. w ) ) = 0 } = { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. ( NN0 ^m W ) ( P ` ( a u. b ) ) = 0 } ) -> E. p e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( P ` ( t u. w ) ) = 0 } = { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. ( NN0 ^m W ) ( p ` ( a u. b ) ) = 0 } )
17 11 16 mpan2 
 |-  ( P e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) -> E. p e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( P ` ( t u. w ) ) = 0 } = { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. ( NN0 ^m W ) ( p ` ( a u. b ) ) = 0 } )
18 17 anim2i 
 |-  ( ( N e. NN0 /\ P e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) ) -> ( N e. NN0 /\ E. p e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( P ` ( t u. w ) ) = 0 } = { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. ( NN0 ^m W ) ( p ` ( a u. b ) ) = 0 } ) )
19 1 2 3 eldioph4b 
 |-  ( { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( P ` ( t u. w ) ) = 0 } e. ( Dioph ` N ) <-> ( N e. NN0 /\ E. p e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( P ` ( t u. w ) ) = 0 } = { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. ( NN0 ^m W ) ( p ` ( a u. b ) ) = 0 } ) )
20 18 19 sylibr 
 |-  ( ( N e. NN0 /\ P e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( P ` ( t u. w ) ) = 0 } e. ( Dioph ` N ) )