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 = ( 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 )