# Metamath Proof Explorer

## Definition df-ig1p

Description: Define a choice function for generators of ideals over a division ring; this is the unique monic polynomial of minimal degree in the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015) (Revised by AV, 25-Sep-2020)

Ref Expression
Assertion df-ig1p ${⊢}{idlGen}_{\mathrm{1p}}=\left({r}\in \mathrm{V}⟼\left({i}\in \mathrm{LIdeal}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)⟼if\left({i}=\left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\},{0}_{{\mathrm{Poly}}_{1}\left({r}\right)},\left(\iota {g}\in \left({i}\cap {Monic}_{\mathrm{1p}}\left({r}\right)\right)|{\mathrm{deg}}_{1}\left({r}\right)\left({g}\right)=sup\left({\mathrm{deg}}_{1}\left({r}\right)\left[{i}\setminus \left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\}\right],ℝ,<\right)\right)\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cig1p ${class}{idlGen}_{\mathrm{1p}}$
1 vr ${setvar}{r}$
2 cvv ${class}\mathrm{V}$
3 vi ${setvar}{i}$
4 clidl ${class}\mathrm{LIdeal}$
5 cpl1 ${class}{\mathrm{Poly}}_{1}$
6 1 cv ${setvar}{r}$
7 6 5 cfv ${class}{\mathrm{Poly}}_{1}\left({r}\right)$
8 7 4 cfv ${class}\mathrm{LIdeal}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)$
9 3 cv ${setvar}{i}$
10 c0g ${class}{0}_{𝑔}$
11 7 10 cfv ${class}{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}$
12 11 csn ${class}\left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\}$
13 9 12 wceq ${wff}{i}=\left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\}$
14 vg ${setvar}{g}$
15 cmn1 ${class}{Monic}_{\mathrm{1p}}$
16 6 15 cfv ${class}{Monic}_{\mathrm{1p}}\left({r}\right)$
17 9 16 cin ${class}\left({i}\cap {Monic}_{\mathrm{1p}}\left({r}\right)\right)$
18 cdg1 ${class}{\mathrm{deg}}_{1}$
19 6 18 cfv ${class}{\mathrm{deg}}_{1}\left({r}\right)$
20 14 cv ${setvar}{g}$
21 20 19 cfv ${class}{\mathrm{deg}}_{1}\left({r}\right)\left({g}\right)$
22 9 12 cdif ${class}\left({i}\setminus \left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\}\right)$
23 19 22 cima ${class}{\mathrm{deg}}_{1}\left({r}\right)\left[{i}\setminus \left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\}\right]$
24 cr ${class}ℝ$
25 clt ${class}<$
26 23 24 25 cinf ${class}sup\left({\mathrm{deg}}_{1}\left({r}\right)\left[{i}\setminus \left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\}\right],ℝ,<\right)$
27 21 26 wceq ${wff}{\mathrm{deg}}_{1}\left({r}\right)\left({g}\right)=sup\left({\mathrm{deg}}_{1}\left({r}\right)\left[{i}\setminus \left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\}\right],ℝ,<\right)$
28 27 14 17 crio ${class}\left(\iota {g}\in \left({i}\cap {Monic}_{\mathrm{1p}}\left({r}\right)\right)|{\mathrm{deg}}_{1}\left({r}\right)\left({g}\right)=sup\left({\mathrm{deg}}_{1}\left({r}\right)\left[{i}\setminus \left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\}\right],ℝ,<\right)\right)$
29 13 11 28 cif ${class}if\left({i}=\left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\},{0}_{{\mathrm{Poly}}_{1}\left({r}\right)},\left(\iota {g}\in \left({i}\cap {Monic}_{\mathrm{1p}}\left({r}\right)\right)|{\mathrm{deg}}_{1}\left({r}\right)\left({g}\right)=sup\left({\mathrm{deg}}_{1}\left({r}\right)\left[{i}\setminus \left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\}\right],ℝ,<\right)\right)\right)$
30 3 8 29 cmpt ${class}\left({i}\in \mathrm{LIdeal}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)⟼if\left({i}=\left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\},{0}_{{\mathrm{Poly}}_{1}\left({r}\right)},\left(\iota {g}\in \left({i}\cap {Monic}_{\mathrm{1p}}\left({r}\right)\right)|{\mathrm{deg}}_{1}\left({r}\right)\left({g}\right)=sup\left({\mathrm{deg}}_{1}\left({r}\right)\left[{i}\setminus \left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\}\right],ℝ,<\right)\right)\right)\right)$
31 1 2 30 cmpt ${class}\left({r}\in \mathrm{V}⟼\left({i}\in \mathrm{LIdeal}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)⟼if\left({i}=\left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\},{0}_{{\mathrm{Poly}}_{1}\left({r}\right)},\left(\iota {g}\in \left({i}\cap {Monic}_{\mathrm{1p}}\left({r}\right)\right)|{\mathrm{deg}}_{1}\left({r}\right)\left({g}\right)=sup\left({\mathrm{deg}}_{1}\left({r}\right)\left[{i}\setminus \left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\}\right],ℝ,<\right)\right)\right)\right)\right)$
32 0 31 wceq ${wff}{idlGen}_{\mathrm{1p}}=\left({r}\in \mathrm{V}⟼\left({i}\in \mathrm{LIdeal}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)⟼if\left({i}=\left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\},{0}_{{\mathrm{Poly}}_{1}\left({r}\right)},\left(\iota {g}\in \left({i}\cap {Monic}_{\mathrm{1p}}\left({r}\right)\right)|{\mathrm{deg}}_{1}\left({r}\right)\left({g}\right)=sup\left({\mathrm{deg}}_{1}\left({r}\right)\left[{i}\setminus \left\{{0}_{{\mathrm{Poly}}_{1}\left({r}\right)}\right\}\right],ℝ,<\right)\right)\right)\right)\right)$