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 𝑃 = ( Poly1𝑅 )
Assertion ply1idom ( 𝑅 ∈ IDomn → 𝑃 ∈ IDomn )

Proof

Step Hyp Ref Expression
1 ply1domn.p 𝑃 = ( Poly1𝑅 )
2 1 ply1crng ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
3 1 ply1domn ( 𝑅 ∈ Domn → 𝑃 ∈ Domn )
4 2 3 anim12i ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) → ( 𝑃 ∈ CRing ∧ 𝑃 ∈ Domn ) )
5 isidom ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
6 isidom ( 𝑃 ∈ IDomn ↔ ( 𝑃 ∈ CRing ∧ 𝑃 ∈ Domn ) )
7 4 5 6 3imtr4i ( 𝑅 ∈ IDomn → 𝑃 ∈ IDomn )