Theorem ply1pid

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

	Ref	Expression
Hypothesis	ply1lpir.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
Assertion	ply1pid	⊢ ( 𝑅 ∈ Field → 𝑃 ∈ PID )

Proof

Step	Hyp	Ref	Expression
1		ply1lpir.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		fldidom	⊢ ( 𝑅 ∈ Field → 𝑅 ∈ IDomn )
3	1	ply1idom	⊢ ( 𝑅 ∈ IDomn → 𝑃 ∈ IDomn )
4	2 3	syl	⊢ ( 𝑅 ∈ Field → 𝑃 ∈ IDomn )
5		isfld	⊢ ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing ) )
6	5	simplbi	⊢ ( 𝑅 ∈ Field → 𝑅 ∈ DivRing )
7	1	ply1lpir	⊢ ( 𝑅 ∈ DivRing → 𝑃 ∈ LPIR )
8	6 7	syl	⊢ ( 𝑅 ∈ Field → 𝑃 ∈ LPIR )
9		df-pid	⊢ PID = ( IDomn ∩ LPIR )
10	9	elin2	⊢ ( 𝑃 ∈ PID ↔ ( 𝑃 ∈ IDomn ∧ 𝑃 ∈ LPIR ) )
11	4 8 10	sylanbrc	⊢ ( 𝑅 ∈ Field → 𝑃 ∈ PID )