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 = Poly 1 R
Assertion ply1pid R Field P PID

Proof

Step Hyp Ref Expression
1 ply1lpir.p P = Poly 1 R
2 fldidom R Field R IDomn
3 1 ply1idom R IDomn P IDomn
4 2 3 syl R Field P IDomn
5 isfld R Field R DivRing R CRing
6 5 simplbi R Field R DivRing
7 1 ply1lpir R DivRing P LPIR
8 6 7 syl R Field P LPIR
9 df-pid PID = IDomn LPIR
10 9 elin2 P PID P IDomn P LPIR
11 4 8 10 sylanbrc R Field P PID