Step |
Hyp |
Ref |
Expression |
1 |
|
df-mnc |
|- Monic = ( s e. ~P CC |-> { p e. ( Poly ` s ) | ( ( coeff ` p ) ` ( deg ` p ) ) = 1 } ) |
2 |
1
|
dmmptss |
|- dom Monic C_ ~P CC |
3 |
|
elfvdm |
|- ( P e. ( Monic ` S ) -> S e. dom Monic ) |
4 |
2 3
|
sseldi |
|- ( P e. ( Monic ` S ) -> S e. ~P CC ) |
5 |
4
|
elpwid |
|- ( P e. ( Monic ` S ) -> S C_ CC ) |
6 |
|
plybss |
|- ( P e. ( Poly ` S ) -> S C_ CC ) |
7 |
6
|
adantr |
|- ( ( P e. ( Poly ` S ) /\ ( ( coeff ` P ) ` ( deg ` P ) ) = 1 ) -> S C_ CC ) |
8 |
|
cnex |
|- CC e. _V |
9 |
8
|
elpw2 |
|- ( S e. ~P CC <-> S C_ CC ) |
10 |
|
fveq2 |
|- ( s = S -> ( Poly ` s ) = ( Poly ` S ) ) |
11 |
|
rabeq |
|- ( ( Poly ` s ) = ( Poly ` S ) -> { p e. ( Poly ` s ) | ( ( coeff ` p ) ` ( deg ` p ) ) = 1 } = { p e. ( Poly ` S ) | ( ( coeff ` p ) ` ( deg ` p ) ) = 1 } ) |
12 |
10 11
|
syl |
|- ( s = S -> { p e. ( Poly ` s ) | ( ( coeff ` p ) ` ( deg ` p ) ) = 1 } = { p e. ( Poly ` S ) | ( ( coeff ` p ) ` ( deg ` p ) ) = 1 } ) |
13 |
|
fvex |
|- ( Poly ` S ) e. _V |
14 |
13
|
rabex |
|- { p e. ( Poly ` S ) | ( ( coeff ` p ) ` ( deg ` p ) ) = 1 } e. _V |
15 |
12 1 14
|
fvmpt |
|- ( S e. ~P CC -> ( Monic ` S ) = { p e. ( Poly ` S ) | ( ( coeff ` p ) ` ( deg ` p ) ) = 1 } ) |
16 |
9 15
|
sylbir |
|- ( S C_ CC -> ( Monic ` S ) = { p e. ( Poly ` S ) | ( ( coeff ` p ) ` ( deg ` p ) ) = 1 } ) |
17 |
16
|
eleq2d |
|- ( S C_ CC -> ( P e. ( Monic ` S ) <-> P e. { p e. ( Poly ` S ) | ( ( coeff ` p ) ` ( deg ` p ) ) = 1 } ) ) |
18 |
|
fveq2 |
|- ( p = P -> ( coeff ` p ) = ( coeff ` P ) ) |
19 |
|
fveq2 |
|- ( p = P -> ( deg ` p ) = ( deg ` P ) ) |
20 |
18 19
|
fveq12d |
|- ( p = P -> ( ( coeff ` p ) ` ( deg ` p ) ) = ( ( coeff ` P ) ` ( deg ` P ) ) ) |
21 |
20
|
eqeq1d |
|- ( p = P -> ( ( ( coeff ` p ) ` ( deg ` p ) ) = 1 <-> ( ( coeff ` P ) ` ( deg ` P ) ) = 1 ) ) |
22 |
21
|
elrab |
|- ( P e. { p e. ( Poly ` S ) | ( ( coeff ` p ) ` ( deg ` p ) ) = 1 } <-> ( P e. ( Poly ` S ) /\ ( ( coeff ` P ) ` ( deg ` P ) ) = 1 ) ) |
23 |
17 22
|
bitrdi |
|- ( S C_ CC -> ( P e. ( Monic ` S ) <-> ( P e. ( Poly ` S ) /\ ( ( coeff ` P ) ` ( deg ` P ) ) = 1 ) ) ) |
24 |
5 7 23
|
pm5.21nii |
|- ( P e. ( Monic ` S ) <-> ( P e. ( Poly ` S ) /\ ( ( coeff ` P ) ` ( deg ` P ) ) = 1 ) ) |