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 )