Metamath Proof Explorer


Theorem elmnc

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

Ref Expression
Assertion elmnc PMonicSPPolyScoeffPdegP=1

Proof

Step Hyp Ref Expression
1 df-mnc Monic=s𝒫pPolys|coeffpdegp=1
2 1 dmmptss domMonic𝒫
3 elfvdm PMonicSSdomMonic
4 2 3 sselid PMonicSS𝒫
5 4 elpwid PMonicSS
6 plybss PPolySS
7 6 adantr PPolyScoeffPdegP=1S
8 cnex V
9 8 elpw2 S𝒫S
10 fveq2 s=SPolys=PolyS
11 rabeq Polys=PolySpPolys|coeffpdegp=1=pPolyS|coeffpdegp=1
12 10 11 syl s=SpPolys|coeffpdegp=1=pPolyS|coeffpdegp=1
13 fvex PolySV
14 13 rabex pPolyS|coeffpdegp=1V
15 12 1 14 fvmpt S𝒫MonicS=pPolyS|coeffpdegp=1
16 9 15 sylbir SMonicS=pPolyS|coeffpdegp=1
17 16 eleq2d SPMonicSPpPolyS|coeffpdegp=1
18 fveq2 p=Pcoeffp=coeffP
19 fveq2 p=Pdegp=degP
20 18 19 fveq12d p=Pcoeffpdegp=coeffPdegP
21 20 eqeq1d p=Pcoeffpdegp=1coeffPdegP=1
22 21 elrab PpPolyS|coeffpdegp=1PPolyScoeffPdegP=1
23 17 22 bitrdi SPMonicSPPolyScoeffPdegP=1
24 5 7 23 pm5.21nii PMonicSPPolyScoeffPdegP=1