This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )