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

Definition df-ig1p 24657
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 24652 . 2 class idlGen1p
2 vr . . 3 setvar 𝑟
3 cvv 3495 . . 3 class V
4 vi . . . 4 setvar 𝑖
52cv 1527 . . . . . 6 class 𝑟
6 cpl1 20275 . . . . . 6 class Poly1
75, 6cfv 6349 . . . . 5 class (Poly1𝑟)
8 clidl 19873 . . . . 5 class LIdeal
97, 8cfv 6349 . . . 4 class (LIdeal‘(Poly1𝑟))
104cv 1527 . . . . . 6 class 𝑖
11 c0g 16703 . . . . . . . 8 class 0g
127, 11cfv 6349 . . . . . . 7 class (0g‘(Poly1𝑟))
1312csn 4559 . . . . . 6 class {(0g‘(Poly1𝑟))}
1410, 13wceq 1528 . . . . 5 wff 𝑖 = {(0g‘(Poly1𝑟))}
15 vg . . . . . . . . 9 setvar 𝑔
1615cv 1527 . . . . . . . 8 class 𝑔
17 cdg1 24577 . . . . . . . . 9 class deg1
185, 17cfv 6349 . . . . . . . 8 class ( deg1𝑟)
1916, 18cfv 6349 . . . . . . 7 class (( deg1𝑟)‘𝑔)
2010, 13cdif 3932 . . . . . . . . 9 class (𝑖 ∖ {(0g‘(Poly1𝑟))})
2118, 20cima 5552 . . . . . . . 8 class (( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))}))
22 cr 10525 . . . . . . . 8 class
23 clt 10664 . . . . . . . 8 class <
2421, 22, 23cinf 8894 . . . . . . 7 class inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < )
2519, 24wceq 1528 . . . . . 6 wff (( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < )
26 cmn1 24648 . . . . . . . 8 class Monic1p
275, 26cfv 6349 . . . . . . 7 class (Monic1p𝑟)
2810, 27cin 3934 . . . . . 6 class (𝑖 ∩ (Monic1p𝑟))
2925, 15, 28crio 7102 . . . . 5 class (𝑔 ∈ (𝑖 ∩ (Monic1p𝑟))(( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < ))
3014, 12, 29cif 4465 . . . 4 class if(𝑖 = {(0g‘(Poly1𝑟))}, (0g‘(Poly1𝑟)), (𝑔 ∈ (𝑖 ∩ (Monic1p𝑟))(( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < )))
314, 9, 30cmpt 5138 . . 3 class (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ if(𝑖 = {(0g‘(Poly1𝑟))}, (0g‘(Poly1𝑟)), (𝑔 ∈ (𝑖 ∩ (Monic1p𝑟))(( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < ))))
322, 3, 31cmpt 5138 . 2 class (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ if(𝑖 = {(0g‘(Poly1𝑟))}, (0g‘(Poly1𝑟)), (𝑔 ∈ (𝑖 ∩ (Monic1p𝑟))(( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < )))))
331, 32wceq 1528 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  24695
  Copyright terms: Public domain W3C validator