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

Definition df-ig1p 23698
 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.)
Assertion
Ref Expression
df-ig1p idlGen1p = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ if(𝑖 = {(0g‘(Poly1𝑟))}, (0g‘(Poly1𝑟)), (𝑔 ∈ (𝑖 ∩ (Monic1p𝑟))(( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < )))))
Distinct variable group:   𝑔,𝑟,𝑖

Detailed syntax breakdown of Definition df-ig1p
StepHypRef Expression
1 cig1p 23693 . 2 class idlGen1p
2 vr . . 3 setvar 𝑟
3 cvv 3173 . . 3 class V
4 vi . . . 4 setvar 𝑖
52cv 1474 . . . . . 6 class 𝑟
6 cpl1 19368 . . . . . 6 class Poly1
75, 6cfv 5804 . . . . 5 class (Poly1𝑟)
8 clidl 18991 . . . . 5 class LIdeal
97, 8cfv 5804 . . . 4 class (LIdeal‘(Poly1𝑟))
104cv 1474 . . . . . 6 class 𝑖
11 c0g 15923 . . . . . . . 8 class 0g
127, 11cfv 5804 . . . . . . 7 class (0g‘(Poly1𝑟))
1312csn 4125 . . . . . 6 class {(0g‘(Poly1𝑟))}
1410, 13wceq 1475 . . . . 5 wff 𝑖 = {(0g‘(Poly1𝑟))}
15 vg . . . . . . . . 9 setvar 𝑔
1615cv 1474 . . . . . . . 8 class 𝑔
17 cdg1 23618 . . . . . . . . 9 class deg1
185, 17cfv 5804 . . . . . . . 8 class ( deg1𝑟)
1916, 18cfv 5804 . . . . . . 7 class (( deg1𝑟)‘𝑔)
2010, 13cdif 3537 . . . . . . . . 9 class (𝑖 ∖ {(0g‘(Poly1𝑟))})
2118, 20cima 5041 . . . . . . . 8 class (( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))}))
22 cr 9814 . . . . . . . 8 class
23 clt 9953 . . . . . . . 8 class <
2421, 22, 23cinf 8230 . . . . . . 7 class inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < )
2519, 24wceq 1475 . . . . . 6 wff (( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < )
26 cmn1 23689 . . . . . . . 8 class Monic1p
275, 26cfv 5804 . . . . . . 7 class (Monic1p𝑟)
2810, 27cin 3539 . . . . . 6 class (𝑖 ∩ (Monic1p𝑟))
2925, 15, 28crio 6510 . . . . 5 class (𝑔 ∈ (𝑖 ∩ (Monic1p𝑟))(( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < ))
3014, 12, 29cif 4036 . . . 4 class if(𝑖 = {(0g‘(Poly1𝑟))}, (0g‘(Poly1𝑟)), (𝑔 ∈ (𝑖 ∩ (Monic1p𝑟))(( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < )))
314, 9, 30cmpt 4643 . . 3 class (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ if(𝑖 = {(0g‘(Poly1𝑟))}, (0g‘(Poly1𝑟)), (𝑔 ∈ (𝑖 ∩ (Monic1p𝑟))(( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < ))))
322, 3, 31cmpt 4643 . 2 class (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ if(𝑖 = {(0g‘(Poly1𝑟))}, (0g‘(Poly1𝑟)), (𝑔 ∈ (𝑖 ∩ (Monic1p𝑟))(( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < )))))
331, 32wceq 1475 1 wff idlGen1p = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ if(𝑖 = {(0g‘(Poly1𝑟))}, (0g‘(Poly1𝑟)), (𝑔 ∈ (𝑖 ∩ (Monic1p𝑟))(( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < )))))
 Colors of variables: wff setvar class This definition is referenced by:  ig1pval  23736
 Copyright terms: Public domain W3C validator