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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ig1pirred.g ⊢ 𝐺 = ( idlGen1p ‘ 𝑅 )
ig1pirred.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
ig1pirred.r ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
ig1pirred.1 ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑃 ) )
ig1pirred.2 ⊢ ( 𝜑 → 𝐼 ≠ 𝑈 )
Assertion ig1pnunit ( 𝜑 → ¬ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 ig1pirred.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ig1pirred.g ⊢ 𝐺 = ( idlGen1p ‘ 𝑅 )
3 ig1pirred.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
4 ig1pirred.r ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
5 ig1pirred.1 ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑃 ) )
6 ig1pirred.2 ⊢ ( 𝜑 → 𝐼 ≠ 𝑈 )
7 eqid ⊢ ( Unit ‘ 𝑃 ) = ( Unit ‘ 𝑃 )
8 simpr ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) ) → ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) )
9 eqid ⊢ ( LIdeal ‘ 𝑃 ) = ( LIdeal ‘ 𝑃 )
10 1 2 9 ig1pcl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑃 ) ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )
11 4 5 10 syl2anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )
12 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )
13 4 drngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
14 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15 13 14 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) ) → 𝑃 ∈ Ring )
17 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) ) → 𝐼 ∈ ( LIdeal ‘ 𝑃 ) )
18 3 7 8 12 16 17 lidlunitel ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) ) → 𝐼 = 𝑈 )
19 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) ) → 𝐼 ≠ 𝑈 )
20 19 neneqd ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) ) → ¬ 𝐼 = 𝑈 )
21 18 20 pm2.65da ⊢ ( 𝜑 → ¬ ( 𝐺 ‘ 𝐼 ) ∈ ( Unit ‘ 𝑃 ) )