Metamath Proof Explorer

Theorem elmnc

Description: Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014)

Ref Expression
Assertion elmnc 
|- ( P e. ( Monic ` S ) <-> ( P e. ( Poly ` S ) /\ ( ( coeff ` P ) ` ( deg ` P ) ) = 1 ) )

Proof

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