Metamath Proof Explorer

Theorem ply1idom

Description: The ring of univariate polynomials over an integral domain is itself an integral domain. (Contributed by Stefan O'Rear, 29-Mar-2015)

		Ref	Expression
	Hypothesis	ply1domn.p	$⊢ P = {Poly}_{1} (R)$
	Assertion	ply1idom	$⊢ R \in IDomn \to P \in IDomn$

Step	Hyp	Ref	Expression
1		ply1domn.p	$⊢ P = {Poly}_{1} (R)$
2	1	ply1crng	$⊢ R \in CRing \to P \in CRing$
3	1	ply1domn	$⊢ R \in Domn \to P \in Domn$
4	2 3	anim12i	$⊢ (R \in CRing \land R \in Domn) \to (P \in CRing \land P \in Domn)$
5		isidom	$⊢ R \in IDomn \leftrightarrow (R \in CRing \land R \in Domn)$
6		isidom	$⊢ P \in IDomn \leftrightarrow (P \in CRing \land P \in Domn)$
7	4 5 6	3imtr4i	$⊢ R \in IDomn \to P \in IDomn$