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 = Poly 1 ⁡ R
ig1pirred.g ⊢ G = idlGen 1p ⁡ R
ig1pirred.u ⊢ U = Base P
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 = Poly 1 ⁡ R
2 ig1pirred.g ⊢ G = idlGen 1p ⁡ R
3 ig1pirred.u ⊢ U = Base P
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