Metamath Proof Explorer

Theorem ig1pcl

Description: The monic generator of an ideal is always in the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015) (Proof shortened by AV, 25-Sep-2020)

Ref Expression
Hypotheses ig1pval.p ⊢ P = Poly 1 ⁡ R
ig1pval.g ⊢ G = idlGen 1p ⁡ R
ig1pcl.u ⊢ U = LIdeal ⁡ P
Assertion ig1pcl ⊢ R ∈ DivRing ∧ I ∈ U → G ⁡ I ∈ I

Proof

Step Hyp Ref Expression
1 ig1pval.p ⊢ P = Poly 1 ⁡ R
2 ig1pval.g ⊢ G = idlGen 1p ⁡ R
3 ig1pcl.u ⊢ U = LIdeal ⁡ P
4 fveq2 ⊢ I = 0 P → G ⁡ I = G ⁡ 0 P
5 id ⊢ I = 0 P → I = 0 P
6 4 5 eleq12d ⊢ I = 0 P → G ⁡ I ∈ I ↔ G ⁡ 0 P ∈ 0 P
7 eqid ⊢ 0 P = 0 P
8 eqid ⊢ deg 1 ⁡ R = deg 1 ⁡ R
9 eqid ⊢ Monic 1p ⁡ R = Monic 1p ⁡ R
10 1 2 7 3 8 9 ig1pval3 ⊢ R ∈ DivRing ∧ I ∈ U ∧ I ≠ 0 P → G ⁡ I ∈ I ∧ G ⁡ I ∈ Monic 1p ⁡ R ∧ deg 1 ⁡ R ⁡ G ⁡ I = sup deg 1 ⁡ R I ∖ 0 P ℝ <
11 10 simp1d ⊢ R ∈ DivRing ∧ I ∈ U ∧ I ≠ 0 P → G ⁡ I ∈ I
12 11 3expa ⊢ R ∈ DivRing ∧ I ∈ U ∧ I ≠ 0 P → G ⁡ I ∈ I
13 drngring ⊢ R ∈ DivRing → R ∈ Ring
14 1 2 7 ig1pval2 ⊢ R ∈ Ring → G ⁡ 0 P = 0 P
15 13 14 syl ⊢ R ∈ DivRing → G ⁡ 0 P = 0 P
16 fvex ⊢ G ⁡ 0 P ∈ V
17 16 elsn ⊢ G ⁡ 0 P ∈ 0 P ↔ G ⁡ 0 P = 0 P
18 15 17 sylibr ⊢ R ∈ DivRing → G ⁡ 0 P ∈ 0 P
19 18 adantr ⊢ R ∈ DivRing ∧ I ∈ U → G ⁡ 0 P ∈ 0 P
20 6 12 19 pm2.61ne ⊢ R ∈ DivRing ∧ I ∈ U → G ⁡ I ∈ I