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

Metamath Proof Explorer

Theorem 0ringmon1p

Description: There are no monic polynomials over a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025)

Ref Expression
Hypotheses 0ringmon1p.1 
|- M = ( Monic1p ` R )
0ringmon1p.2 
|- B = ( Base ` R )
0ringmon1p.3 
|- ( ph -> R e. Ring )
0ringmon1p.4 
|- ( ph -> ( # ` B ) = 1 )
Assertion 0ringmon1p 
|- ( ph -> M = (/) )

Proof

Step Hyp Ref Expression
1 0ringmon1p.1 
 |-  M = ( Monic1p ` R )
2 0ringmon1p.2 
 |-  B = ( Base ` R )
3 0ringmon1p.3 
 |-  ( ph -> R e. Ring )
4 0ringmon1p.4 
 |-  ( ph -> ( # ` B ) = 1 )
5 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
6 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
7 eqid 
 |-  ( 0g ` ( Poly1 ` R ) ) = ( 0g ` ( Poly1 ` R ) )
8 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
9 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
10 5 6 7 8 1 9 ismon1p 
 |-  ( p e. M <-> ( p e. ( Base ` ( Poly1 ` R ) ) /\ p =/= ( 0g ` ( Poly1 ` R ) ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) )
11 10 biimpi 
 |-  ( p e. M -> ( p e. ( Base ` ( Poly1 ` R ) ) /\ p =/= ( 0g ` ( Poly1 ` R ) ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) )
12 11 adantl 
 |-  ( ( ph /\ p e. M ) -> ( p e. ( Base ` ( Poly1 ` R ) ) /\ p =/= ( 0g ` ( Poly1 ` R ) ) /\ ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) ) )
13 12 simp3d 
 |-  ( ( ph /\ p e. M ) -> ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) )
14 3 adantr 
 |-  ( ( ph /\ p e. M ) -> R e. Ring )
15 12 simp1d 
 |-  ( ( ph /\ p e. M ) -> p e. ( Base ` ( Poly1 ` R ) ) )
16 12 simp2d 
 |-  ( ( ph /\ p e. M ) -> p =/= ( 0g ` ( Poly1 ` R ) ) )
17 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
18 eqid 
 |-  ( coe1 ` p ) = ( coe1 ` p )
19 8 5 7 6 17 18 deg1ldg 
 |-  ( ( R e. Ring /\ p e. ( Base ` ( Poly1 ` R ) ) /\ p =/= ( 0g ` ( Poly1 ` R ) ) ) -> ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) =/= ( 0g ` R ) )
20 14 15 16 19 syl3anc 
 |-  ( ( ph /\ p e. M ) -> ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) =/= ( 0g ` R ) )
21 2 17 9 0ring01eq 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( 0g ` R ) = ( 1r ` R ) )
22 3 4 21 syl2anc 
 |-  ( ph -> ( 0g ` R ) = ( 1r ` R ) )
23 22 adantr 
 |-  ( ( ph /\ p e. M ) -> ( 0g ` R ) = ( 1r ` R ) )
24 20 23 neeqtrd 
 |-  ( ( ph /\ p e. M ) -> ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) =/= ( 1r ` R ) )
25 24 neneqd 
 |-  ( ( ph /\ p e. M ) -> -. ( ( coe1 ` p ) ` ( ( deg1 ` R ) ` p ) ) = ( 1r ` R ) )
26 13 25 pm2.65da 
 |-  ( ph -> -. p e. M )
27 26 eq0rdv 
 |-  ( ph -> M = (/) )