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 = ( Poly1 ` R )
Assertion	ply1idom	|- ( R e. IDomn -> P e. IDomn )

Proof

Step	Hyp	Ref	Expression
1		ply1domn.p	|- P = ( Poly1 ` R )
2	1	ply1crng	|- ( R e. CRing -> P e. CRing )
3	1	ply1domn	|- ( R e. Domn -> P e. Domn )
4	2 3	anim12i	|- ( ( R e. CRing /\ R e. Domn ) -> ( P e. CRing /\ P e. Domn ) )
5		isidom	|- ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
6		isidom	|- ( P e. IDomn <-> ( P e. CRing /\ P e. Domn ) )
7	4 5 6	3imtr4i	|- ( R e. IDomn -> P e. IDomn )