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