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=BaseP
ig1pirred.r ⊢φ→R∈DivRing
ig1pirred.1 ⊢φ→I∈LIdeal⁡P
ig1pirred.2 ⊢φ→I≠U
Assertion ig1pnunit ⊢φ→¬G⁡I∈Unit⁡P

Proof

Step Hyp Ref Expression
1 ig1pirred.p ⊢P=Poly1⁡R
2 ig1pirred.g ⊢G=idlGen1p⁡R
3 ig1pirred.u ⊢U=BaseP
4 ig1pirred.r ⊢φ→R∈DivRing
5 ig1pirred.1 ⊢φ→I∈LIdeal⁡P
6 ig1pirred.2 ⊢φ→I≠U
7 eqid ⊢Unit⁡P=Unit⁡P
8 simpr ⊢φ∧G⁡I∈Unit⁡P→G⁡I∈Unit⁡P
9 eqid ⊢LIdeal⁡P=LIdeal⁡P
10 1 2 9 ig1pcl ⊢R∈DivRing∧I∈LIdeal⁡P→G⁡I∈I
11 4 5 10 syl2anc ⊢φ→G⁡I∈I
12 11 adantr ⊢φ∧G⁡I∈Unit⁡P→G⁡I∈I
13 4 drngringd ⊢φ→R∈Ring
14 1 ply1ring ⊢R∈Ring→P∈Ring
15 13 14 syl ⊢φ→P∈Ring
16 15 adantr ⊢φ∧G⁡I∈Unit⁡P→P∈Ring
17 5 adantr ⊢φ∧G⁡I∈Unit⁡P→I∈LIdeal⁡P
18 3 7 8 12 16 17 lidlunitel ⊢φ∧G⁡I∈Unit⁡P→I=U
19 6 adantr ⊢φ∧G⁡I∈Unit⁡P→I≠U
20 19 neneqd ⊢φ∧G⁡I∈Unit⁡P→¬I=U
21 18 20 pm2.65da ⊢φ→¬G⁡I∈Unit⁡P