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 ∈ IDomn → P ∈ IDomn

Proof

Step Hyp Ref Expression
1 ply1domn.p ⊢ P = Poly 1 ⁡ R
2 1 ply1crng ⊢ R ∈ CRing → P ∈ CRing
3 1 ply1domn ⊢ R ∈ Domn → P ∈ Domn
4 2 3 anim12i ⊢ R ∈ CRing ∧ R ∈ Domn → P ∈ CRing ∧ P ∈ Domn
5 isidom ⊢ R ∈ IDomn ↔ R ∈ CRing ∧ R ∈ Domn
6 isidom ⊢ P ∈ IDomn ↔ P ∈ CRing ∧ P ∈ Domn
7 4 5 6 3imtr4i ⊢ R ∈ IDomn → P ∈ IDomn