Metamath Proof Explorer

Theorem eldioph4b

Description: Membership in Dioph expressed using a quantified union to add witness variables instead of a restriction to remove them. (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 eldioph4b 
|- ( S e. ( Dioph ` N ) <-> ( N e. NN0 /\ E. p e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) S = { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 } ) )

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 eldiophelnn0 
 |-  ( S e. ( Dioph ` N ) -> N e. NN0 )
5 ovex 
 |-  ( 1 ... N ) e. _V
6 1 5 unex 
 |-  ( W u. ( 1 ... N ) ) e. _V
7 6 jctr 
 |-  ( N e. NN0 -> ( N e. NN0 /\ ( W u. ( 1 ... N ) ) e. _V ) )
8 2 intnanr 
 |-  -. ( W e. Fin /\ ( 1 ... N ) e. Fin )
9 unfir 
 |-  ( ( W u. ( 1 ... N ) ) e. Fin -> ( W e. Fin /\ ( 1 ... N ) e. Fin ) )
10 8 9 mto 
 |-  -. ( W u. ( 1 ... N ) ) e. Fin
11 ssun2 
 |-  ( 1 ... N ) C_ ( W u. ( 1 ... N ) )
12 10 11 pm3.2i 
 |-  ( -. ( W u. ( 1 ... N ) ) e. Fin /\ ( 1 ... N ) C_ ( W u. ( 1 ... N ) ) )
13 eldioph2b 
 |-  ( ( ( N e. NN0 /\ ( W u. ( 1 ... N ) ) e. _V ) /\ ( -. ( W u. ( 1 ... N ) ) e. Fin /\ ( 1 ... N ) C_ ( W u. ( 1 ... N ) ) ) ) -> ( S e. ( Dioph ` N ) <-> E. p e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) S = { t | E. u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
14 7 12 13 sylancl 
 |-  ( N e. NN0 -> ( S e. ( Dioph ` N ) <-> E. p e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) S = { t | E. u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
15 elmapssres 
 |-  ( ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) /\ ( 1 ... N ) C_ ( W u. ( 1 ... N ) ) ) -> ( u |` ( 1 ... N ) ) e. ( NN0 ^m ( 1 ... N ) ) )
16 11 15 mpan2 
 |-  ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) -> ( u |` ( 1 ... N ) ) e. ( NN0 ^m ( 1 ... N ) ) )
17 16 adantr 
 |-  ( ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) /\ ( p ` u ) = 0 ) -> ( u |` ( 1 ... N ) ) e. ( NN0 ^m ( 1 ... N ) ) )
18 ssun1 
 |-  W C_ ( W u. ( 1 ... N ) )
19 elmapssres 
 |-  ( ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) /\ W C_ ( W u. ( 1 ... N ) ) ) -> ( u |` W ) e. ( NN0 ^m W ) )
20 18 19 mpan2 
 |-  ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) -> ( u |` W ) e. ( NN0 ^m W ) )
21 20 adantr 
 |-  ( ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) /\ ( p ` u ) = 0 ) -> ( u |` W ) e. ( NN0 ^m W ) )
22 uncom 
 |-  ( ( u |` ( 1 ... N ) ) u. ( u |` W ) ) = ( ( u |` W ) u. ( u |` ( 1 ... N ) ) )
23 resundi 
 |-  ( u |` ( W u. ( 1 ... N ) ) ) = ( ( u |` W ) u. ( u |` ( 1 ... N ) ) )
24 22 23 eqtr4i 
 |-  ( ( u |` ( 1 ... N ) ) u. ( u |` W ) ) = ( u |` ( W u. ( 1 ... N ) ) )
25 elmapi 
 |-  ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) -> u : ( W u. ( 1 ... N ) ) --> NN0 )
26 ffn 
 |-  ( u : ( W u. ( 1 ... N ) ) --> NN0 -> u Fn ( W u. ( 1 ... N ) ) )
27 fnresdm 
 |-  ( u Fn ( W u. ( 1 ... N ) ) -> ( u |` ( W u. ( 1 ... N ) ) ) = u )
28 25 26 27 3syl 
 |-  ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) -> ( u |` ( W u. ( 1 ... N ) ) ) = u )
29 24 28 syl5eq 
 |-  ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) -> ( ( u |` ( 1 ... N ) ) u. ( u |` W ) ) = u )
30 29 fveqeq2d 
 |-  ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) -> ( ( p ` ( ( u |` ( 1 ... N ) ) u. ( u |` W ) ) ) = 0 <-> ( p ` u ) = 0 ) )
31 30 biimpar 
 |-  ( ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) /\ ( p ` u ) = 0 ) -> ( p ` ( ( u |` ( 1 ... N ) ) u. ( u |` W ) ) ) = 0 )
32 uneq2 
 |-  ( w = ( u |` W ) -> ( ( u |` ( 1 ... N ) ) u. w ) = ( ( u |` ( 1 ... N ) ) u. ( u |` W ) ) )
33 32 fveqeq2d 
 |-  ( w = ( u |` W ) -> ( ( p ` ( ( u |` ( 1 ... N ) ) u. w ) ) = 0 <-> ( p ` ( ( u |` ( 1 ... N ) ) u. ( u |` W ) ) ) = 0 ) )
34 33 rspcev 
 |-  ( ( ( u |` W ) e. ( NN0 ^m W ) /\ ( p ` ( ( u |` ( 1 ... N ) ) u. ( u |` W ) ) ) = 0 ) -> E. w e. ( NN0 ^m W ) ( p ` ( ( u |` ( 1 ... N ) ) u. w ) ) = 0 )
35 21 31 34 syl2anc 
 |-  ( ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) /\ ( p ` u ) = 0 ) -> E. w e. ( NN0 ^m W ) ( p ` ( ( u |` ( 1 ... N ) ) u. w ) ) = 0 )
36 17 35 jca 
 |-  ( ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) /\ ( p ` u ) = 0 ) -> ( ( u |` ( 1 ... N ) ) e. ( NN0 ^m ( 1 ... N ) ) /\ E. w e. ( NN0 ^m W ) ( p ` ( ( u |` ( 1 ... N ) ) u. w ) ) = 0 ) )
37 eleq1 
 |-  ( t = ( u |` ( 1 ... N ) ) -> ( t e. ( NN0 ^m ( 1 ... N ) ) <-> ( u |` ( 1 ... N ) ) e. ( NN0 ^m ( 1 ... N ) ) ) )
38 uneq1 
 |-  ( t = ( u |` ( 1 ... N ) ) -> ( t u. w ) = ( ( u |` ( 1 ... N ) ) u. w ) )
39 38 fveqeq2d 
 |-  ( t = ( u |` ( 1 ... N ) ) -> ( ( p ` ( t u. w ) ) = 0 <-> ( p ` ( ( u |` ( 1 ... N ) ) u. w ) ) = 0 ) )
40 39 rexbidv 
 |-  ( t = ( u |` ( 1 ... N ) ) -> ( E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 <-> E. w e. ( NN0 ^m W ) ( p ` ( ( u |` ( 1 ... N ) ) u. w ) ) = 0 ) )
41 37 40 anbi12d 
 |-  ( t = ( u |` ( 1 ... N ) ) -> ( ( t e. ( NN0 ^m ( 1 ... N ) ) /\ E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 ) <-> ( ( u |` ( 1 ... N ) ) e. ( NN0 ^m ( 1 ... N ) ) /\ E. w e. ( NN0 ^m W ) ( p ` ( ( u |` ( 1 ... N ) ) u. w ) ) = 0 ) ) )
42 36 41 syl5ibrcom 
 |-  ( ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) /\ ( p ` u ) = 0 ) -> ( t = ( u |` ( 1 ... N ) ) -> ( t e. ( NN0 ^m ( 1 ... N ) ) /\ E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 ) ) )
43 42 expimpd 
 |-  ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) -> ( ( ( p ` u ) = 0 /\ t = ( u |` ( 1 ... N ) ) ) -> ( t e. ( NN0 ^m ( 1 ... N ) ) /\ E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 ) ) )
44 43 ancomsd 
 |-  ( u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) -> ( ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) -> ( t e. ( NN0 ^m ( 1 ... N ) ) /\ E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 ) ) )
45 44 rexlimiv 
 |-  ( E. u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) -> ( t e. ( NN0 ^m ( 1 ... N ) ) /\ E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 ) )
46 uncom 
 |-  ( t u. w ) = ( w u. t )
47 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
48 sslin 
 |-  ( ( 1 ... N ) C_ NN -> ( W i^i ( 1 ... N ) ) C_ ( W i^i NN ) )
49 47 48 ax-mp 
 |-  ( W i^i ( 1 ... N ) ) C_ ( W i^i NN )
50 49 3 sseqtri 
 |-  ( W i^i ( 1 ... N ) ) C_ (/)
51 ss0 
 |-  ( ( W i^i ( 1 ... N ) ) C_ (/) -> ( W i^i ( 1 ... N ) ) = (/) )
52 50 51 ax-mp 
 |-  ( W i^i ( 1 ... N ) ) = (/)
53 52 reseq2i 
 |-  ( w |` ( W i^i ( 1 ... N ) ) ) = ( w |` (/) )
54 res0 
 |-  ( w |` (/) ) = (/)
55 53 54 eqtri 
 |-  ( w |` ( W i^i ( 1 ... N ) ) ) = (/)
56 52 reseq2i 
 |-  ( t |` ( W i^i ( 1 ... N ) ) ) = ( t |` (/) )
57 res0 
 |-  ( t |` (/) ) = (/)
58 56 57 eqtri 
 |-  ( t |` ( W i^i ( 1 ... N ) ) ) = (/)
59 55 58 eqtr4i 
 |-  ( w |` ( W i^i ( 1 ... N ) ) ) = ( t |` ( W i^i ( 1 ... N ) ) )
60 elmapresaun 
 |-  ( ( w e. ( NN0 ^m W ) /\ t e. ( NN0 ^m ( 1 ... N ) ) /\ ( w |` ( W i^i ( 1 ... N ) ) ) = ( t |` ( W i^i ( 1 ... N ) ) ) ) -> ( w u. t ) e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) )
61 59 60 mp3an3 
 |-  ( ( w e. ( NN0 ^m W ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> ( w u. t ) e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) )
62 61 ancoms 
 |-  ( ( t e. ( NN0 ^m ( 1 ... N ) ) /\ w e. ( NN0 ^m W ) ) -> ( w u. t ) e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) )
63 46 62 eqeltrid 
 |-  ( ( t e. ( NN0 ^m ( 1 ... N ) ) /\ w e. ( NN0 ^m W ) ) -> ( t u. w ) e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) )
64 63 adantr 
 |-  ( ( ( t e. ( NN0 ^m ( 1 ... N ) ) /\ w e. ( NN0 ^m W ) ) /\ ( p ` ( t u. w ) ) = 0 ) -> ( t u. w ) e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) )
65 46 reseq1i 
 |-  ( ( t u. w ) |` ( 1 ... N ) ) = ( ( w u. t ) |` ( 1 ... N ) )
66 elmapresaunres2 
 |-  ( ( w e. ( NN0 ^m W ) /\ t e. ( NN0 ^m ( 1 ... N ) ) /\ ( w |` ( W i^i ( 1 ... N ) ) ) = ( t |` ( W i^i ( 1 ... N ) ) ) ) -> ( ( w u. t ) |` ( 1 ... N ) ) = t )
67 59 66 mp3an3 
 |-  ( ( w e. ( NN0 ^m W ) /\ t e. ( NN0 ^m ( 1 ... N ) ) ) -> ( ( w u. t ) |` ( 1 ... N ) ) = t )
68 67 ancoms 
 |-  ( ( t e. ( NN0 ^m ( 1 ... N ) ) /\ w e. ( NN0 ^m W ) ) -> ( ( w u. t ) |` ( 1 ... N ) ) = t )
69 65 68 eqtr2id 
 |-  ( ( t e. ( NN0 ^m ( 1 ... N ) ) /\ w e. ( NN0 ^m W ) ) -> t = ( ( t u. w ) |` ( 1 ... N ) ) )
70 69 adantr 
 |-  ( ( ( t e. ( NN0 ^m ( 1 ... N ) ) /\ w e. ( NN0 ^m W ) ) /\ ( p ` ( t u. w ) ) = 0 ) -> t = ( ( t u. w ) |` ( 1 ... N ) ) )
71 simpr 
 |-  ( ( ( t e. ( NN0 ^m ( 1 ... N ) ) /\ w e. ( NN0 ^m W ) ) /\ ( p ` ( t u. w ) ) = 0 ) -> ( p ` ( t u. w ) ) = 0 )
72 reseq1 
 |-  ( u = ( t u. w ) -> ( u |` ( 1 ... N ) ) = ( ( t u. w ) |` ( 1 ... N ) ) )
73 72 eqeq2d 
 |-  ( u = ( t u. w ) -> ( t = ( u |` ( 1 ... N ) ) <-> t = ( ( t u. w ) |` ( 1 ... N ) ) ) )
74 fveqeq2 
 |-  ( u = ( t u. w ) -> ( ( p ` u ) = 0 <-> ( p ` ( t u. w ) ) = 0 ) )
75 73 74 anbi12d 
 |-  ( u = ( t u. w ) -> ( ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) <-> ( t = ( ( t u. w ) |` ( 1 ... N ) ) /\ ( p ` ( t u. w ) ) = 0 ) ) )
76 75 rspcev 
 |-  ( ( ( t u. w ) e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) /\ ( t = ( ( t u. w ) |` ( 1 ... N ) ) /\ ( p ` ( t u. w ) ) = 0 ) ) -> E. u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) )
77 64 70 71 76 syl12anc 
 |-  ( ( ( t e. ( NN0 ^m ( 1 ... N ) ) /\ w e. ( NN0 ^m W ) ) /\ ( p ` ( t u. w ) ) = 0 ) -> E. u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) )
78 77 r19.29an 
 |-  ( ( t e. ( NN0 ^m ( 1 ... N ) ) /\ E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 ) -> E. u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) )
79 45 78 impbii 
 |-  ( E. u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) <-> ( t e. ( NN0 ^m ( 1 ... N ) ) /\ E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 ) )
80 79 abbii 
 |-  { t | E. u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } = { t | ( t e. ( NN0 ^m ( 1 ... N ) ) /\ E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 ) }
81 df-rab 
 |-  { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 } = { t | ( t e. ( NN0 ^m ( 1 ... N ) ) /\ E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 ) }
82 80 81 eqtr4i 
 |-  { t | E. u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } = { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 }
83 82 eqeq2i 
 |-  ( S = { t | E. u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } <-> S = { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 } )
84 83 rexbii 
 |-  ( E. p e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) S = { t | E. u e. ( NN0 ^m ( W u. ( 1 ... N ) ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } <-> E. p e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) S = { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 } )
85 14 84 bitrdi 
 |-  ( N e. NN0 -> ( S e. ( Dioph ` N ) <-> E. p e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) S = { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 } ) )
86 4 85 biadanii 
 |-  ( S e. ( Dioph ` N ) <-> ( N e. NN0 /\ E. p e. ( mzPoly ` ( W u. ( 1 ... N ) ) ) S = { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 } ) )