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

Metamath Proof Explorer

Theorem ig1pnunit

Description: The polynomial ideal generator is not a unit polynomial. (Contributed by Thierry Arnoux, 19-Mar-2025)

Ref Expression
Hypotheses ig1pirred.p 
|- P = ( Poly1 ` R )
ig1pirred.g 
|- G = ( idlGen1p ` R )
ig1pirred.u 
|- U = ( Base ` P )
ig1pirred.r 
|- ( ph -> R e. DivRing )
ig1pirred.1 
|- ( ph -> I e. ( LIdeal ` P ) )
ig1pirred.2 
|- ( ph -> I =/= U )
Assertion ig1pnunit 
|- ( ph -> -. ( G ` I ) e. ( Unit ` P ) )

Proof

Step Hyp Ref Expression
1 ig1pirred.p 
 |-  P = ( Poly1 ` R )
2 ig1pirred.g 
 |-  G = ( idlGen1p ` R )
3 ig1pirred.u 
 |-  U = ( Base ` P )
4 ig1pirred.r 
 |-  ( ph -> R e. DivRing )
5 ig1pirred.1 
 |-  ( ph -> I e. ( LIdeal ` P ) )
6 ig1pirred.2 
 |-  ( ph -> I =/= U )
7 eqid 
 |-  ( Unit ` P ) = ( Unit ` P )
8 simpr 
 |-  ( ( ph /\ ( G ` I ) e. ( Unit ` P ) ) -> ( G ` I ) e. ( Unit ` P ) )
9 eqid 
 |-  ( LIdeal ` P ) = ( LIdeal ` P )
10 1 2 9 ig1pcl 
 |-  ( ( R e. DivRing /\ I e. ( LIdeal ` P ) ) -> ( G ` I ) e. I )
11 4 5 10 syl2anc 
 |-  ( ph -> ( G ` I ) e. I )
12 11 adantr 
 |-  ( ( ph /\ ( G ` I ) e. ( Unit ` P ) ) -> ( G ` I ) e. I )
13 4 drngringd 
 |-  ( ph -> R e. Ring )
14 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
15 13 14 syl 
 |-  ( ph -> P e. Ring )
16 15 adantr 
 |-  ( ( ph /\ ( G ` I ) e. ( Unit ` P ) ) -> P e. Ring )
17 5 adantr 
 |-  ( ( ph /\ ( G ` I ) e. ( Unit ` P ) ) -> I e. ( LIdeal ` P ) )
18 3 7 8 12 16 17 lidlunitel 
 |-  ( ( ph /\ ( G ` I ) e. ( Unit ` P ) ) -> I = U )
19 6 adantr 
 |-  ( ( ph /\ ( G ` I ) e. ( Unit ` P ) ) -> I =/= U )
20 19 neneqd 
 |-  ( ( ph /\ ( G ` I ) e. ( Unit ` P ) ) -> -. I = U )
21 18 20 pm2.65da 
 |-  ( ph -> -. ( G ` I ) e. ( Unit ` P ) )