Metamath Proof Explorer

Theorem ply1nzb

Description: Univariate polynomials are nonzero iff the base is nonzero. Or in contraposition, the univariate polynomials over the zero ring are also zero. (Contributed by Mario Carneiro, 13-Jun-2015)

Ref Expression
Hypothesis ply1domn.p 
|- P = ( Poly1 ` R )
Assertion ply1nzb 
|- ( R e. Ring -> ( R e. NzRing <-> P e. NzRing ) )

Proof

Step Hyp Ref Expression
1 ply1domn.p 
 |-  P = ( Poly1 ` R )
2 1 ply1nz 
 |-  ( R e. NzRing -> P e. NzRing )
3 simpl 
 |-  ( ( R e. Ring /\ P e. NzRing ) -> R e. Ring )
4 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
5 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
6 4 5 nzrnz 
 |-  ( P e. NzRing -> ( 1r ` P ) =/= ( 0g ` P ) )
7 6 adantl 
 |-  ( ( R e. Ring /\ P e. NzRing ) -> ( 1r ` P ) =/= ( 0g ` P ) )
8 ifeq1 
 |-  ( ( 1r ` R ) = ( 0g ` R ) -> if ( y = ( 1o X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( y = ( 1o X. { 0 } ) , ( 0g ` R ) , ( 0g ` R ) ) )
9 ifid 
 |-  if ( y = ( 1o X. { 0 } ) , ( 0g ` R ) , ( 0g ` R ) ) = ( 0g ` R )
10 8 9 eqtrdi 
 |-  ( ( 1r ` R ) = ( 0g ` R ) -> if ( y = ( 1o X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
11 10 ralrimivw 
 |-  ( ( 1r ` R ) = ( 0g ` R ) -> A. y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } if ( y = ( 1o X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
12 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
13 eqid 
 |-  { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } = { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin }
14 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
15 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
16 12 1 4 ply1mpl1 
 |-  ( 1r ` P ) = ( 1r ` ( 1o mPoly R ) )
17 1on 
 |-  1o e. On
18 17 a1i 
 |-  ( ( R e. Ring /\ P e. NzRing ) -> 1o e. On )
19 12 13 14 15 16 18 3 mpl1 
 |-  ( ( R e. Ring /\ P e. NzRing ) -> ( 1r ` P ) = ( y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } |-> if ( y = ( 1o X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
20 12 1 5 ply1mpl0 
 |-  ( 0g ` P ) = ( 0g ` ( 1o mPoly R ) )
21 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
22 3 21 syl 
 |-  ( ( R e. Ring /\ P e. NzRing ) -> R e. Grp )
23 12 13 14 20 18 22 mpl0 
 |-  ( ( R e. Ring /\ P e. NzRing ) -> ( 0g ` P ) = ( { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } X. { ( 0g ` R ) } ) )
24 fconstmpt 
 |-  ( { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } X. { ( 0g ` R ) } ) = ( y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } |-> ( 0g ` R ) )
25 23 24 eqtrdi 
 |-  ( ( R e. Ring /\ P e. NzRing ) -> ( 0g ` P ) = ( y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } |-> ( 0g ` R ) ) )
26 19 25 eqeq12d 
 |-  ( ( R e. Ring /\ P e. NzRing ) -> ( ( 1r ` P ) = ( 0g ` P ) <-> ( y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } |-> if ( y = ( 1o X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } |-> ( 0g ` R ) ) ) )
27 fvex 
 |-  ( 1r ` R ) e. _V
28 fvex 
 |-  ( 0g ` R ) e. _V
29 27 28 ifex 
 |-  if ( y = ( 1o X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) e. _V
30 29 rgenw 
 |-  A. y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } if ( y = ( 1o X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) e. _V
31 mpteqb 
 |-  ( A. y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } if ( y = ( 1o X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) e. _V -> ( ( y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } |-> if ( y = ( 1o X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } |-> ( 0g ` R ) ) <-> A. y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } if ( y = ( 1o X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) ) )
32 30 31 ax-mp 
 |-  ( ( y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } |-> if ( y = ( 1o X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } |-> ( 0g ` R ) ) <-> A. y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } if ( y = ( 1o X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
33 26 32 bitrdi 
 |-  ( ( R e. Ring /\ P e. NzRing ) -> ( ( 1r ` P ) = ( 0g ` P ) <-> A. y e. { x e. ( NN0 ^m 1o ) | ( `' x " NN ) e. Fin } if ( y = ( 1o X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) ) )
34 11 33 syl5ibr 
 |-  ( ( R e. Ring /\ P e. NzRing ) -> ( ( 1r ` R ) = ( 0g ` R ) -> ( 1r ` P ) = ( 0g ` P ) ) )
35 34 necon3d 
 |-  ( ( R e. Ring /\ P e. NzRing ) -> ( ( 1r ` P ) =/= ( 0g ` P ) -> ( 1r ` R ) =/= ( 0g ` R ) ) )
36 7 35 mpd 
 |-  ( ( R e. Ring /\ P e. NzRing ) -> ( 1r ` R ) =/= ( 0g ` R ) )
37 15 14 isnzr 
 |-  ( R e. NzRing <-> ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) )
38 3 36 37 sylanbrc 
 |-  ( ( R e. Ring /\ P e. NzRing ) -> R e. NzRing )
39 38 ex 
 |-  ( R e. Ring -> ( P e. NzRing -> R e. NzRing ) )
40 2 39 impbid2 
 |-  ( R e. Ring -> ( R e. NzRing <-> P e. NzRing ) )