Theorem ply1nz

Description: Univariate polynomials over a nonzero ring are a nonzero ring. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypothesis	ply1domn.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
Assertion	ply1nz	⊢ ( 𝑅 ∈ NzRing → 𝑃 ∈ NzRing )

Proof

Step	Hyp	Ref	Expression
1		ply1domn.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
3	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
4	2 3	syl	⊢ ( 𝑅 ∈ NzRing → 𝑃 ∈ Ring )
5		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
6		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
8	1 5 6 7	ply1sclf	⊢ ( 𝑅 ∈ Ring → ( algSc ‘ 𝑃 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑃 ) )
9	2 8	syl	⊢ ( 𝑅 ∈ NzRing → ( algSc ‘ 𝑃 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑃 ) )
10		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
11	6 10	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
12	2 11	syl	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
13	9 12	ffvelcdmd	⊢ ( 𝑅 ∈ NzRing → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
14		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
15	10 14	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
16		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
17	1 5 14 16 6	ply1scln0	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ≠ ( 0g ‘ 𝑃 ) )
18	2 12 15 17	syl3anc	⊢ ( 𝑅 ∈ NzRing → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ≠ ( 0g ‘ 𝑃 ) )
19		eldifsn	⊢ ( ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( ( Base ‘ 𝑃 ) ∖ { ( 0g ‘ 𝑃 ) } ) ↔ ( ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) ∧ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ≠ ( 0g ‘ 𝑃 ) ) )
20	13 18 19	sylanbrc	⊢ ( 𝑅 ∈ NzRing → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( ( Base ‘ 𝑃 ) ∖ { ( 0g ‘ 𝑃 ) } ) )
21	16 7	ringelnzr	⊢ ( ( 𝑃 ∈ Ring ∧ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( ( Base ‘ 𝑃 ) ∖ { ( 0g ‘ 𝑃 ) } ) ) → 𝑃 ∈ NzRing )
22	4 20 21	syl2anc	⊢ ( 𝑅 ∈ NzRing → 𝑃 ∈ NzRing )