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 
|- P = ( Poly1 ` R )
Assertion ply1nz 
|- ( R e. NzRing -> P e. NzRing )

Proof

Step Hyp Ref Expression
1 ply1domn.p 
 |-  P = ( Poly1 ` R )
2 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
3 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
4 2 3 syl 
 |-  ( R e. NzRing -> P e. Ring )
5 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  ( Base ` P ) = ( Base ` P )
8 1 5 6 7 ply1sclf 
 |-  ( R e. Ring -> ( algSc ` P ) : ( Base ` R ) --> ( Base ` P ) )
9 2 8 syl 
 |-  ( R e. NzRing -> ( algSc ` P ) : ( Base ` R ) --> ( Base ` P ) )
10 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
11 6 10 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
12 2 11 syl 
 |-  ( R e. NzRing -> ( 1r ` R ) e. ( Base ` R ) )
13 9 12 ffvelrnd 
 |-  ( R e. NzRing -> ( ( algSc ` P ) ` ( 1r ` R ) ) e. ( Base ` P ) )
14 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
15 10 14 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
16 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
17 1 5 14 16 6 ply1scln0 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. ( Base ` R ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( ( algSc ` P ) ` ( 1r ` R ) ) =/= ( 0g ` P ) )
18 2 12 15 17 syl3anc 
 |-  ( R e. NzRing -> ( ( algSc ` P ) ` ( 1r ` R ) ) =/= ( 0g ` P ) )
19 eldifsn 
 |-  ( ( ( algSc ` P ) ` ( 1r ` R ) ) e. ( ( Base ` P ) \ { ( 0g ` P ) } ) <-> ( ( ( algSc ` P ) ` ( 1r ` R ) ) e. ( Base ` P ) /\ ( ( algSc ` P ) ` ( 1r ` R ) ) =/= ( 0g ` P ) ) )
20 13 18 19 sylanbrc 
 |-  ( R e. NzRing -> ( ( algSc ` P ) ` ( 1r ` R ) ) e. ( ( Base ` P ) \ { ( 0g ` P ) } ) )
21 16 7 ringelnzr 
 |-  ( ( P e. Ring /\ ( ( algSc ` P ) ` ( 1r ` R ) ) e. ( ( Base ` P ) \ { ( 0g ` P ) } ) ) -> P e. NzRing )
22 4 20 21 syl2anc 
 |-  ( R e. NzRing -> P e. NzRing )