Definition df-ig1p 22639

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.)

Assertion

Ref	Expression
df-ig1p	|- idlGen1p = ( r e. _V |-> ( i e. (LIdeal ` (Poly1 ` r ) ) |-> if ( i = { ( 0g ` (Poly1 ` r ) ) } , ( 0g ` (Poly1 ` r ) ) , ( iota_ g e. ( i i^i (Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = sup ( ( ( deg1 ` r ) " ( i \ { ( 0g ` (Poly1 ` r ) ) } ) ) , RR , `' < ) ) ) ) )

Distinct variable group:   g, r, i

Detailed syntax breakdown of Definition df-ig1p

Step	Hyp	Ref	Expression
1		cig1p 22634	. 2 class idlGen1p
2		vr	. . 3 setvar r
3		cvv 3047	. . 3 class _V
4		vi	. . . 4 setvar i
5	2	cv 1398	. . . . . 6 class r
6		cpl1 18348	. . . . . 6 class Poly1
7	5, 6	cfv 5509	. . . . 5 class (Poly1 ` r )
8		clidl 17948	. . . . 5 class LIdeal
9	7, 8	cfv 5509	. . . 4 class (LIdeal ` (Poly1 ` r ) )
10	4	cv 1398	. . . . . 6 class i
11		c0g 14866	. . . . . . . 8 class 0g
12	7, 11	cfv 5509	. . . . . . 7 class ( 0g ` (Poly1 ` r ) )
13	12	csn 3957	. . . . . 6 class { ( 0g ` (Poly1 ` r ) ) }
14	10, 13	wceq 1399	. . . . 5 wff i = { ( 0g ` (Poly1 ` r ) ) }
15		vg	. . . . . . . . 9 setvar g
16	15	cv 1398	. . . . . . . 8 class g
17		cdg1 22556	. . . . . . . . 9 class deg1
18	5, 17	cfv 5509	. . . . . . . 8 class ( deg1 ` r )
19	16, 18	cfv 5509	. . . . . . 7 class ( ( deg1 ` r ) ` g )
20	10, 13	cdif 3399	. . . . . . . . 9 class ( i \ { ( 0g ` (Poly1 ` r ) ) } )
21	18, 20	cima 4929	. . . . . . . 8 class ( ( deg1 ` r ) " ( i \ { ( 0g ` (Poly1 ` r ) ) } ) )
22		cr 9420	. . . . . . . 8 class RR
23		clt 9557	. . . . . . . . 9 class <
24	23	ccnv 4925	. . . . . . . 8 class `' <
25	21, 22, 24	csup 7833	. . . . . . 7 class sup ( ( ( deg1 ` r ) " ( i \ { ( 0g ` (Poly1 ` r ) ) } ) ) , RR , `' < )
26	19, 25	wceq 1399	. . . . . 6 wff ( ( deg1 ` r ) ` g ) = sup ( ( ( deg1 ` r ) " ( i \ { ( 0g ` (Poly1 ` r ) ) } ) ) , RR , `' < )
27		cmn1 22630	. . . . . . . 8 class Monic1p
28	5, 27	cfv 5509	. . . . . . 7 class (Monic1p ` r )
29	10, 28	cin 3401	. . . . . 6 class ( i i^i (Monic1p ` r ) )
30	26, 15, 29	crio 6175	. . . . 5 class ( iota_ g e. ( i i^i (Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = sup ( ( ( deg1 ` r ) " ( i \ { ( 0g ` (Poly1 ` r ) ) } ) ) , RR , `' < ) )
31	14, 12, 30	cif 3870	. . . 4 class if ( i = { ( 0g ` (Poly1 ` r ) ) } , ( 0g ` (Poly1 ` r ) ) , ( iota_ g e. ( i i^i (Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = sup ( ( ( deg1 ` r ) " ( i \ { ( 0g ` (Poly1 ` r ) ) } ) ) , RR , `' < ) ) )
32	4, 9, 31	cmpt 4438	. . 3 class ( i e. (LIdeal ` (Poly1 ` r ) ) |-> if ( i = { ( 0g ` (Poly1 ` r ) ) } , ( 0g ` (Poly1 ` r ) ) , ( iota_ g e. ( i i^i (Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = sup ( ( ( deg1 ` r ) " ( i \ { ( 0g ` (Poly1 ` r ) ) } ) ) , RR , `' < ) ) ) )
33	2, 3, 32	cmpt 4438	. 2 class ( r e. _V |-> ( i e. (LIdeal ` (Poly1 ` r ) ) |-> if ( i = { ( 0g ` (Poly1 ` r ) ) } , ( 0g ` (Poly1 ` r ) ) , ( iota_ g e. ( i i^i (Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = sup ( ( ( deg1 ` r ) " ( i \ { ( 0g ` (Poly1 ` r ) ) } ) ) , RR , `' < ) ) ) ) )
34	1, 33	wceq 1399	1 wff idlGen1p = ( r e. _V |-> ( i e. (LIdeal ` (Poly1 ` r ) ) |-> if ( i = { ( 0g ` (Poly1 ` r ) ) } , ( 0g ` (Poly1 ` r ) ) , ( iota_ g e. ( i i^i (Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = sup ( ( ( deg1 ` r ) " ( i \ { ( 0g ` (Poly1 ` r ) ) } ) ) , RR , `' < ) ) ) ) )

This definition is referenced by:  ig1pval  22677