Database
BASIC REAL AND COMPLEX FUNCTIONS
Polynomials
The division algorithm for univariate polynomials
ply1pid
Next ⟩
Elementary properties of complex polynomials
Metamath Proof Explorer
Ascii
Unicode
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