# 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}={\mathrm{Poly}}_{1}\left({R}\right)$
ig1pval.g ${⊢}{G}={idlGen}_{\mathrm{1p}}\left({R}\right)$
ig1pcl.u ${⊢}{U}=\mathrm{LIdeal}\left({P}\right)$
Assertion ig1pcl ${⊢}\left({R}\in \mathrm{DivRing}\wedge {I}\in {U}\right)\to {G}\left({I}\right)\in {I}$

### Proof

Step Hyp Ref Expression
1 ig1pval.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 ig1pval.g ${⊢}{G}={idlGen}_{\mathrm{1p}}\left({R}\right)$
3 ig1pcl.u ${⊢}{U}=\mathrm{LIdeal}\left({P}\right)$
4 fveq2 ${⊢}{I}=\left\{{0}_{{P}}\right\}\to {G}\left({I}\right)={G}\left(\left\{{0}_{{P}}\right\}\right)$
5 id ${⊢}{I}=\left\{{0}_{{P}}\right\}\to {I}=\left\{{0}_{{P}}\right\}$
6 4 5 eleq12d ${⊢}{I}=\left\{{0}_{{P}}\right\}\to \left({G}\left({I}\right)\in {I}↔{G}\left(\left\{{0}_{{P}}\right\}\right)\in \left\{{0}_{{P}}\right\}\right)$
7 eqid ${⊢}{0}_{{P}}={0}_{{P}}$
8 eqid ${⊢}{\mathrm{deg}}_{1}\left({R}\right)={\mathrm{deg}}_{1}\left({R}\right)$
9 eqid ${⊢}{Monic}_{\mathrm{1p}}\left({R}\right)={Monic}_{\mathrm{1p}}\left({R}\right)$
10 1 2 7 3 8 9 ig1pval3 ${⊢}\left({R}\in \mathrm{DivRing}\wedge {I}\in {U}\wedge {I}\ne \left\{{0}_{{P}}\right\}\right)\to \left({G}\left({I}\right)\in {I}\wedge {G}\left({I}\right)\in {Monic}_{\mathrm{1p}}\left({R}\right)\wedge {\mathrm{deg}}_{1}\left({R}\right)\left({G}\left({I}\right)\right)=sup\left({\mathrm{deg}}_{1}\left({R}\right)\left[{I}\setminus \left\{{0}_{{P}}\right\}\right],ℝ,<\right)\right)$
11 10 simp1d ${⊢}\left({R}\in \mathrm{DivRing}\wedge {I}\in {U}\wedge {I}\ne \left\{{0}_{{P}}\right\}\right)\to {G}\left({I}\right)\in {I}$
12 11 3expa ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge {I}\in {U}\right)\wedge {I}\ne \left\{{0}_{{P}}\right\}\right)\to {G}\left({I}\right)\in {I}$
13 drngring ${⊢}{R}\in \mathrm{DivRing}\to {R}\in \mathrm{Ring}$
14 1 2 7 ig1pval2 ${⊢}{R}\in \mathrm{Ring}\to {G}\left(\left\{{0}_{{P}}\right\}\right)={0}_{{P}}$
15 13 14 syl ${⊢}{R}\in \mathrm{DivRing}\to {G}\left(\left\{{0}_{{P}}\right\}\right)={0}_{{P}}$
16 fvex ${⊢}{G}\left(\left\{{0}_{{P}}\right\}\right)\in \mathrm{V}$
17 16 elsn ${⊢}{G}\left(\left\{{0}_{{P}}\right\}\right)\in \left\{{0}_{{P}}\right\}↔{G}\left(\left\{{0}_{{P}}\right\}\right)={0}_{{P}}$
18 15 17 sylibr ${⊢}{R}\in \mathrm{DivRing}\to {G}\left(\left\{{0}_{{P}}\right\}\right)\in \left\{{0}_{{P}}\right\}$
19 18 adantr ${⊢}\left({R}\in \mathrm{DivRing}\wedge {I}\in {U}\right)\to {G}\left(\left\{{0}_{{P}}\right\}\right)\in \left\{{0}_{{P}}\right\}$
20 6 12 19 pm2.61ne ${⊢}\left({R}\in \mathrm{DivRing}\wedge {I}\in {U}\right)\to {G}\left({I}\right)\in {I}$