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