# Metamath Proof Explorer

## Theorem ig1pval3

Description: Characterizing properties of the monic generator of a nonzero ideal of polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015) (Revised 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)$
ig1pval3.z
ig1pval3.u ${⊢}{U}=\mathrm{LIdeal}\left({P}\right)$
ig1pval3.d ${⊢}{D}={\mathrm{deg}}_{1}\left({R}\right)$
ig1pval3.m ${⊢}{M}={Monic}_{\mathrm{1p}}\left({R}\right)$
Assertion ig1pval3

### 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 ig1pval3.z
4 ig1pval3.u ${⊢}{U}=\mathrm{LIdeal}\left({P}\right)$
5 ig1pval3.d ${⊢}{D}={\mathrm{deg}}_{1}\left({R}\right)$
6 ig1pval3.m ${⊢}{M}={Monic}_{\mathrm{1p}}\left({R}\right)$
7 1 2 3 4 5 6 ig1pval
8 7 3adant3
9 simp3
10 9 neneqd
11 10 iffalsed
12 8 11 eqtrd
13 1 4 3 6 5 ig1peu
14 riotacl2
15 13 14 syl
16 12 15 eqeltrd
17 elin ${⊢}{G}\left({I}\right)\in \left({I}\cap {M}\right)↔\left({G}\left({I}\right)\in {I}\wedge {G}\left({I}\right)\in {M}\right)$
18 17 anbi1i
19 fveqeq2
20 19 elrab
21 df-3an
22 18 20 21 3bitr4i
23 16 22 sylib