Step |
Hyp |
Ref |
Expression |
1 |
|
eldiophb |
|- ( A e. ( Dioph ` N ) <-> ( N e. NN0 /\ E. a e. ( ZZ>= ` N ) E. b e. ( mzPoly ` ( 1 ... a ) ) A = { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } ) ) |
2 |
|
simp-5r |
|- ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> S e. _V ) |
3 |
|
simprr |
|- ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> b e. ( mzPoly ` ( 1 ... a ) ) ) |
4 |
3
|
ad2antrr |
|- ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> b e. ( mzPoly ` ( 1 ... a ) ) ) |
5 |
|
simprl |
|- ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> c : ( 1 ... a ) -1-1-> S ) |
6 |
|
f1f |
|- ( c : ( 1 ... a ) -1-1-> S -> c : ( 1 ... a ) --> S ) |
7 |
5 6
|
syl |
|- ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> c : ( 1 ... a ) --> S ) |
8 |
|
mzprename |
|- ( ( S e. _V /\ b e. ( mzPoly ` ( 1 ... a ) ) /\ c : ( 1 ... a ) --> S ) -> ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) e. ( mzPoly ` S ) ) |
9 |
2 4 7 8
|
syl3anc |
|- ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) e. ( mzPoly ` S ) ) |
10 |
|
simprr |
|- ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) |
11 |
|
diophrw |
|- ( ( S e. _V /\ c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) } = { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } ) |
12 |
11
|
eqcomd |
|- ( ( S e. _V /\ c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) -> { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) } ) |
13 |
2 5 10 12
|
syl3anc |
|- ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) } ) |
14 |
|
fveq1 |
|- ( p = ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) -> ( p ` u ) = ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) ) |
15 |
14
|
eqeq1d |
|- ( p = ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) -> ( ( p ` u ) = 0 <-> ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) ) |
16 |
15
|
anbi2d |
|- ( p = ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) -> ( ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) <-> ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) ) ) |
17 |
16
|
rexbidv |
|- ( p = ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) -> ( E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) <-> E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) ) ) |
18 |
17
|
abbidv |
|- ( p = ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) } ) |
19 |
18
|
rspceeqv |
|- ( ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) e. ( mzPoly ` S ) /\ { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m S ) |-> ( b ` ( e o. c ) ) ) ` u ) = 0 ) } ) -> E. p e. ( mzPoly ` S ) { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) |
20 |
9 13 19
|
syl2anc |
|- ( ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) /\ c e. _V ) /\ ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> E. p e. ( mzPoly ` S ) { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) |
21 |
|
simplll |
|- ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> N e. NN0 ) |
22 |
|
simplrl |
|- ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> -. S e. Fin ) |
23 |
|
simplrr |
|- ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> ( 1 ... N ) C_ S ) |
24 |
|
simprl |
|- ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> a e. ( ZZ>= ` N ) ) |
25 |
|
eldioph2lem2 |
|- ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ a e. ( ZZ>= ` N ) ) ) -> E. c ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) |
26 |
21 22 23 24 25
|
syl22anc |
|- ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> E. c ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) |
27 |
|
rexv |
|- ( E. c e. _V ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) <-> E. c ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) |
28 |
26 27
|
sylibr |
|- ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> E. c e. _V ( c : ( 1 ... a ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) |
29 |
20 28
|
r19.29a |
|- ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> E. p e. ( mzPoly ` S ) { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) |
30 |
|
eqeq1 |
|- ( A = { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } -> ( A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } <-> { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) ) |
31 |
30
|
rexbidv |
|- ( A = { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } -> ( E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } <-> E. p e. ( mzPoly ` S ) { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) ) |
32 |
29 31
|
syl5ibrcom |
|- ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ ( a e. ( ZZ>= ` N ) /\ b e. ( mzPoly ` ( 1 ... a ) ) ) ) -> ( A = { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } -> E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) ) |
33 |
32
|
rexlimdvva |
|- ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) -> ( E. a e. ( ZZ>= ` N ) E. b e. ( mzPoly ` ( 1 ... a ) ) A = { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } -> E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) ) |
34 |
33
|
adantld |
|- ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) -> ( ( N e. NN0 /\ E. a e. ( ZZ>= ` N ) E. b e. ( mzPoly ` ( 1 ... a ) ) A = { t | E. d e. ( NN0 ^m ( 1 ... a ) ) ( t = ( d |` ( 1 ... N ) ) /\ ( b ` d ) = 0 ) } ) -> E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) ) |
35 |
1 34
|
syl5bi |
|- ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) -> ( A e. ( Dioph ` N ) -> E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) ) |
36 |
|
simpr |
|- ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) /\ A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) -> A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) |
37 |
|
simplll |
|- ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) -> N e. NN0 ) |
38 |
|
simpllr |
|- ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) -> S e. _V ) |
39 |
|
simplrr |
|- ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) -> ( 1 ... N ) C_ S ) |
40 |
|
simpr |
|- ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) -> p e. ( mzPoly ` S ) ) |
41 |
|
eldioph2 |
|- ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) /\ p e. ( mzPoly ` S ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } e. ( Dioph ` N ) ) |
42 |
37 38 39 40 41
|
syl121anc |
|- ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } e. ( Dioph ` N ) ) |
43 |
42
|
adantr |
|- ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) /\ A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } e. ( Dioph ` N ) ) |
44 |
36 43
|
eqeltrd |
|- ( ( ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) /\ p e. ( mzPoly ` S ) ) /\ A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) -> A e. ( Dioph ` N ) ) |
45 |
44
|
rexlimdva2 |
|- ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) -> ( E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } -> A e. ( Dioph ` N ) ) ) |
46 |
35 45
|
impbid |
|- ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) -> ( A e. ( Dioph ` N ) <-> E. p e. ( mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) ) |