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 )