# Metamath Proof Explorer

## Theorem ig1peu

Description: There is a unique monic polynomial of minimal degree in any nonzero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015) (Revised by AV, 25-Sep-2020)

Ref Expression
Hypotheses ig1peu.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
ig1peu.u ${⊢}{U}=\mathrm{LIdeal}\left({P}\right)$
ig1peu.z
ig1peu.m ${⊢}{M}={Monic}_{\mathrm{1p}}\left({R}\right)$
ig1peu.d ${⊢}{D}={\mathrm{deg}}_{1}\left({R}\right)$
Assertion ig1peu

### Proof

Step Hyp Ref Expression
1 ig1peu.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 ig1peu.u ${⊢}{U}=\mathrm{LIdeal}\left({P}\right)$
3 ig1peu.z
4 ig1peu.m ${⊢}{M}={Monic}_{\mathrm{1p}}\left({R}\right)$
5 ig1peu.d ${⊢}{D}={\mathrm{deg}}_{1}\left({R}\right)$
6 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
7 6 2 lidlss ${⊢}{I}\in {U}\to {I}\subseteq {\mathrm{Base}}_{{P}}$
9 8 ssdifd
10 imass2
11 9 10 syl
12 drngring ${⊢}{R}\in \mathrm{DivRing}\to {R}\in \mathrm{Ring}$
14 5 1 3 6 deg1n0ima
15 13 14 syl
16 11 15 sstrd
17 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
18 16 17 sseqtrdi
19 1 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
20 13 19 syl
21 simp2
22 2 3 lidl0cl
23 20 21 22 syl2anc
24 23 snssd
25 simp3
26 25 necomd
27 pssdifn0
28 24 26 27 syl2anc
29 5 1 6 deg1xrf ${⊢}{D}:{\mathrm{Base}}_{{P}}⟶{ℝ}^{*}$
30 ffn ${⊢}{D}:{\mathrm{Base}}_{{P}}⟶{ℝ}^{*}\to {D}Fn{\mathrm{Base}}_{{P}}$
31 29 30 ax-mp ${⊢}{D}Fn{\mathrm{Base}}_{{P}}$
32 31 a1i
33 8 ssdifssd
34 fnimaeq0
35 32 33 34 syl2anc
36 35 necon3bid
37 28 36 mpbird
38 infssuzcl
39 18 37 38 syl2anc
40 32 33 fvelimabd
41 39 40 mpbid
43 simpl2
45 eqid ${⊢}\mathrm{algSc}\left({P}\right)=\mathrm{algSc}\left({P}\right)$
46 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
47 1 45 46 6 ply1sclf ${⊢}{R}\in \mathrm{Ring}\to \mathrm{algSc}\left({P}\right):{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{P}}$
48 44 47 syl
49 simpl1
50 33 sselda
51 eldifsni
53 eqid ${⊢}{Unic}_{\mathrm{1p}}\left({R}\right)={Unic}_{\mathrm{1p}}\left({R}\right)$
54 1 6 3 53 drnguc1p
55 49 50 52 54 syl3anc
56 eqid ${⊢}\mathrm{Unit}\left({R}\right)=\mathrm{Unit}\left({R}\right)$
57 5 56 53 uc1pldg ${⊢}{h}\in {Unic}_{\mathrm{1p}}\left({R}\right)\to {\mathrm{coe}}_{1}\left({h}\right)\left({D}\left({h}\right)\right)\in \mathrm{Unit}\left({R}\right)$
58 55 57 syl
59 eqid ${⊢}{inv}_{r}\left({R}\right)={inv}_{r}\left({R}\right)$
60 56 59 unitinvcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {\mathrm{coe}}_{1}\left({h}\right)\left({D}\left({h}\right)\right)\in \mathrm{Unit}\left({R}\right)\right)\to {inv}_{r}\left({R}\right)\left({\mathrm{coe}}_{1}\left({h}\right)\left({D}\left({h}\right)\right)\right)\in \mathrm{Unit}\left({R}\right)$
61 44 58 60 syl2anc
62 46 56 unitcl ${⊢}{inv}_{r}\left({R}\right)\left({\mathrm{coe}}_{1}\left({h}\right)\left({D}\left({h}\right)\right)\right)\in \mathrm{Unit}\left({R}\right)\to {inv}_{r}\left({R}\right)\left({\mathrm{coe}}_{1}\left({h}\right)\left({D}\left({h}\right)\right)\right)\in {\mathrm{Base}}_{{R}}$
63 61 62 syl
64 48 63 ffvelrnd
65 eldifi
67 eqid ${⊢}{\cdot }_{{P}}={\cdot }_{{P}}$
68 2 6 67 lidlmcl ${⊢}\left(\left({P}\in \mathrm{Ring}\wedge {I}\in {U}\right)\wedge \left(\mathrm{algSc}\left({P}\right)\left({inv}_{r}\left({R}\right)\left({\mathrm{coe}}_{1}\left({h}\right)\left({D}\left({h}\right)\right)\right)\right)\in {\mathrm{Base}}_{{P}}\wedge {h}\in {I}\right)\right)\to \mathrm{algSc}\left({P}\right)\left({inv}_{r}\left({R}\right)\left({\mathrm{coe}}_{1}\left({h}\right)\left({D}\left({h}\right)\right)\right)\right){\cdot }_{{P}}{h}\in {I}$
69 42 43 64 66 68 syl22anc
70 53 4 1 67 45 5 59 uc1pmon1p ${⊢}\left({R}\in \mathrm{Ring}\wedge {h}\in {Unic}_{\mathrm{1p}}\left({R}\right)\right)\to \mathrm{algSc}\left({P}\right)\left({inv}_{r}\left({R}\right)\left({\mathrm{coe}}_{1}\left({h}\right)\left({D}\left({h}\right)\right)\right)\right){\cdot }_{{P}}{h}\in {M}$
71 44 55 70 syl2anc
72 69 71 elind
73 eqid ${⊢}\mathrm{RLReg}\left({R}\right)=\mathrm{RLReg}\left({R}\right)$
74 73 56 unitrrg ${⊢}{R}\in \mathrm{Ring}\to \mathrm{Unit}\left({R}\right)\subseteq \mathrm{RLReg}\left({R}\right)$
75 44 74 syl
76 75 61 sseldd
77 5 1 73 6 67 45 deg1mul3 ${⊢}\left({R}\in \mathrm{Ring}\wedge {inv}_{r}\left({R}\right)\left({\mathrm{coe}}_{1}\left({h}\right)\left({D}\left({h}\right)\right)\right)\in \mathrm{RLReg}\left({R}\right)\wedge {h}\in {\mathrm{Base}}_{{P}}\right)\to {D}\left(\mathrm{algSc}\left({P}\right)\left({inv}_{r}\left({R}\right)\left({\mathrm{coe}}_{1}\left({h}\right)\left({D}\left({h}\right)\right)\right)\right){\cdot }_{{P}}{h}\right)={D}\left({h}\right)$
78 44 76 50 77 syl3anc
79 fveqeq2 ${⊢}{g}=\mathrm{algSc}\left({P}\right)\left({inv}_{r}\left({R}\right)\left({\mathrm{coe}}_{1}\left({h}\right)\left({D}\left({h}\right)\right)\right)\right){\cdot }_{{P}}{h}\to \left({D}\left({g}\right)={D}\left({h}\right)↔{D}\left(\mathrm{algSc}\left({P}\right)\left({inv}_{r}\left({R}\right)\left({\mathrm{coe}}_{1}\left({h}\right)\left({D}\left({h}\right)\right)\right)\right){\cdot }_{{P}}{h}\right)={D}\left({h}\right)\right)$
80 79 rspcev ${⊢}\left(\mathrm{algSc}\left({P}\right)\left({inv}_{r}\left({R}\right)\left({\mathrm{coe}}_{1}\left({h}\right)\left({D}\left({h}\right)\right)\right)\right){\cdot }_{{P}}{h}\in \left({I}\cap {M}\right)\wedge {D}\left(\mathrm{algSc}\left({P}\right)\left({inv}_{r}\left({R}\right)\left({\mathrm{coe}}_{1}\left({h}\right)\left({D}\left({h}\right)\right)\right)\right){\cdot }_{{P}}{h}\right)={D}\left({h}\right)\right)\to \exists {g}\in \left({I}\cap {M}\right)\phantom{\rule{.4em}{0ex}}{D}\left({g}\right)={D}\left({h}\right)$
81 72 78 80 syl2anc
82 eqeq2
83 82 rexbidv
84 81 83 syl5ibcom
85 84 rexlimdva
86 41 85 mpd
87 eqid ${⊢}{-}_{{P}}={-}_{{P}}$
89 simprl
90 89 elin2d
92 simprl
93 simprr
94 93 elin2d
96 simprr
97 5 4 1 87 88 91 92 95 96 deg1submon1p
98 97 ex
100 31 a1i
103 simpl2
104 89 elin1d
105 93 elin1d
106 2 87 lidlsubcl ${⊢}\left(\left({P}\in \mathrm{Ring}\wedge {I}\in {U}\right)\wedge \left({g}\in {I}\wedge {h}\in {I}\right)\right)\to {g}{-}_{{P}}{h}\in {I}$
107 102 103 104 105 106 syl22anc
109 simpr
110 eldifsn
111 108 109 110 sylanbrc
112 fnfvima
113 100 101 111 112 syl3anc
114 infssuzle
115 99 113 114 syl2anc
116 115 ex
117 imassrn
118 frn ${⊢}{D}:{\mathrm{Base}}_{{P}}⟶{ℝ}^{*}\to \mathrm{ran}{D}\subseteq {ℝ}^{*}$
119 29 118 ax-mp ${⊢}\mathrm{ran}{D}\subseteq {ℝ}^{*}$
120 117 119 sstri
121 120 39 sseldi
123 ringgrp ${⊢}{P}\in \mathrm{Ring}\to {P}\in \mathrm{Grp}$
124 20 123 syl
126 inss1 ${⊢}{I}\cap {M}\subseteq {I}$
127 126 8 sstrid
129 128 89 sseldd
130 128 93 sseldd
131 6 87 grpsubcl ${⊢}\left({P}\in \mathrm{Grp}\wedge {g}\in {\mathrm{Base}}_{{P}}\wedge {h}\in {\mathrm{Base}}_{{P}}\right)\to {g}{-}_{{P}}{h}\in {\mathrm{Base}}_{{P}}$
132 125 129 130 131 syl3anc
133 5 1 6 deg1xrcl ${⊢}{g}{-}_{{P}}{h}\in {\mathrm{Base}}_{{P}}\to {D}\left({g}{-}_{{P}}{h}\right)\in {ℝ}^{*}$
134 132 133 syl
135 122 134 xrlenltd
136 116 135 sylibd