Metamath Proof Explorer


Theorem ply1pid

Description: The polynomials over a field are a PID. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypothesis ply1lpir.p P=Poly1R
Assertion ply1pid RFieldPPID

Proof

Step Hyp Ref Expression
1 ply1lpir.p P=Poly1R
2 fldidom RFieldRIDomn
3 1 ply1idom RIDomnPIDomn
4 2 3 syl RFieldPIDomn
5 isfld RFieldRDivRingRCRing
6 5 simplbi RFieldRDivRing
7 1 ply1lpir RDivRingPLPIR
8 6 7 syl RFieldPLPIR
9 df-pid PID=IDomnLPIR
10 9 elin2 PPIDPIDomnPLPIR
11 4 8 10 sylanbrc RFieldPPID