This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( Poly1 ` R )
Assertion ply1pid 
|- ( R e. Field -> P e. PID )

Proof

Step Hyp Ref Expression
1 ply1lpir.p 
 |-  P = ( Poly1 ` R )
2 fldidom 
 |-  ( R e. Field -> R e. IDomn )
3 1 ply1idom 
 |-  ( R e. IDomn -> P e. IDomn )
4 2 3 syl 
 |-  ( R e. Field -> P e. IDomn )
5 isfld 
 |-  ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
6 5 simplbi 
 |-  ( R e. Field -> R e. DivRing )
7 1 ply1lpir 
 |-  ( R e. DivRing -> P e. LPIR )
8 6 7 syl 
 |-  ( R e. Field -> P e. LPIR )
9 df-pid 
 |-  PID = ( IDomn i^i LPIR )
10 9 elin2 
 |-  ( P e. PID <-> ( P e. IDomn /\ P e. LPIR ) )
11 4 8 10 sylanbrc 
 |-  ( R e. Field -> P e. PID )