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 
|- 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 ) = inf ( ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) , RR , < ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cig1p 
 |-  idlGen1p
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vi 
 |-  i
4 clidl 
 |-  LIdeal
5 cpl1 
 |-  Poly1
6 1 cv 
 |-  r
7 6 5 cfv 
 |-  ( Poly1 ` r )
8 7 4 cfv 
 |-  ( LIdeal ` ( Poly1 ` r ) )
9 3 cv 
 |-  i
10 c0g 
 |-  0g
11 7 10 cfv 
 |-  ( 0g ` ( Poly1 ` r ) )
12 11 csn 
 |-  { ( 0g ` ( Poly1 ` r ) ) }
13 9 12 wceq 
 |-  i = { ( 0g ` ( Poly1 ` r ) ) }
14 vg 
 |-  g
15 cmn1 
 |-  Monic1p
16 6 15 cfv 
 |-  ( Monic1p ` r )
17 9 16 cin 
 |-  ( i i^i ( Monic1p ` r ) )
18 cdg1 
 |-  deg1
19 6 18 cfv 
 |-  ( deg1 ` r )
20 14 cv 
 |-  g
21 20 19 cfv 
 |-  ( ( deg1 ` r ) ` g )
22 9 12 cdif 
 |-  ( i \ { ( 0g ` ( Poly1 ` r ) ) } )
23 19 22 cima 
 |-  ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) )
24 cr 
 |-  RR
25 clt 
 |-  <
26 23 24 25 cinf 
 |-  inf ( ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) , RR , < )
27 21 26 wceq 
 |-  ( ( deg1 ` r ) ` g ) = inf ( ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) , RR , < )
28 27 14 17 crio 
 |-  ( iota_ g e. ( i i^i ( Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = inf ( ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) , RR , < ) )
29 13 11 28 cif 
 |-  if ( i = { ( 0g ` ( Poly1 ` r ) ) } , ( 0g ` ( Poly1 ` r ) ) , ( iota_ g e. ( i i^i ( Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = inf ( ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) , RR , < ) ) )
30 3 8 29 cmpt 
 |-  ( i e. ( LIdeal ` ( Poly1 ` r ) ) |-> if ( i = { ( 0g ` ( Poly1 ` r ) ) } , ( 0g ` ( Poly1 ` r ) ) , ( iota_ g e. ( i i^i ( Monic1p ` r ) ) ( ( deg1 ` r ) ` g ) = inf ( ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) , RR , < ) ) ) )
31 1 2 30 cmpt 
 |-  ( 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 ) = inf ( ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) , RR , < ) ) ) ) )
32 0 31 wceq 
 |-  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 ) = inf ( ( ( deg1 ` r ) " ( i \ { ( 0g ` ( Poly1 ` r ) ) } ) ) , RR , < ) ) ) ) )