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 \in Field \to P \in PID$

Step	Hyp	Ref	Expression
1		ply1lpir.p	$⊢ P = {Poly}_{1} (R)$
2		fldidom	$⊢ R \in Field \to R \in IDomn$
3	1	ply1idom	$⊢ R \in IDomn \to P \in IDomn$
4	2 3	syl	$⊢ R \in Field \to P \in IDomn$
5		isfld	$⊢ R \in Field \leftrightarrow (R \in DivRing \land R \in CRing)$
6	5	simplbi	$⊢ R \in Field \to R \in DivRing$
7	1	ply1lpir	$⊢ R \in DivRing \to P \in LPIR$
8	6 7	syl	$⊢ R \in Field \to P \in LPIR$
9		df-pid	$⊢ PID = IDomn \cap LPIR$
10	9	elin2	$⊢ P \in PID \leftrightarrow (P \in IDomn \land P \in LPIR)$
11	4 8 10	sylanbrc	$⊢ R \in Field \to P \in PID$

Metamath Proof Explorer