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