Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ig1p Structured version   Unicode version

Definition df-ig1p 21724
 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 LIdealPoly1 Poly1 Poly1 Monic1p deg1 deg1 Poly1
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-ig1p
StepHypRef Expression
1 cig1p 21719 . 2 idlGen1p
2 vr . . 3
3 cvv 3070 . . 3
4 vi . . . 4
52cv 1369 . . . . . 6
6 cpl1 17742 . . . . . 6 Poly1
75, 6cfv 5518 . . . . 5 Poly1
8 clidl 17359 . . . . 5 LIdeal
97, 8cfv 5518 . . . 4 LIdealPoly1
104cv 1369 . . . . . 6
11 c0g 14482 . . . . . . . 8
127, 11cfv 5518 . . . . . . 7 Poly1
1312csn 3977 . . . . . 6 Poly1
1410, 13wceq 1370 . . . . 5 Poly1
15 vg . . . . . . . . 9
1615cv 1369 . . . . . . . 8
17 cdg1 21641 . . . . . . . . 9 deg1
185, 17cfv 5518 . . . . . . . 8 deg1
1916, 18cfv 5518 . . . . . . 7 deg1
2010, 13cdif 3425 . . . . . . . . 9 Poly1
2118, 20cima 4943 . . . . . . . 8 deg1 Poly1
22 cr 9384 . . . . . . . 8
23 clt 9521 . . . . . . . . 9
2423ccnv 4939 . . . . . . . 8
2521, 22, 24csup 7793 . . . . . . 7 deg1 Poly1
2619, 25wceq 1370 . . . . . 6 deg1 deg1 Poly1
27 cmn1 21715 . . . . . . . 8 Monic1p
285, 27cfv 5518 . . . . . . 7 Monic1p
2910, 28cin 3427 . . . . . 6 Monic1p
3026, 15, 29crio 6152 . . . . 5 Monic1p deg1 deg1 Poly1
3114, 12, 30cif 3891 . . . 4 Poly1 Poly1 Monic1p deg1 deg1 Poly1
324, 9, 31cmpt 4450 . . 3 LIdealPoly1 Poly1 Poly1 Monic1p deg1 deg1 Poly1
332, 3, 32cmpt 4450 . 2 LIdealPoly1 Poly1 Poly1 Monic1p deg1 deg1 Poly1
341, 33wceq 1370 1 idlGen1p LIdealPoly1 Poly1 Poly1 Monic1p deg1 deg1 Poly1
 Colors of variables: wff setvar class This definition is referenced by:  ig1pval  21762
 Copyright terms: Public domain W3C validator