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)=inf\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	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vi	$$setvari$$
4		clidl	$$class\mathrm{LIdeal}$$
5		cpl1	$$class{\mathrm{Poly}}_1$$
6	1	cv	$$setvarr$$
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	$$setvari$$
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	$$wffi=\left\{0_{{\mathrm{Poly}}_1\left(r\right)}\right\}$$
14		vg	$$setvarg$$
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	$$setvarg$$
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	$$classinf\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)=inf\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)=inf\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	$$classif\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)=inf\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)=inf\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)=inf\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)=inf\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)$$