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 24234
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 24229 . 2 class idlGen1p
2 vr . . 3 setvar 𝑟
3 cvv 3386 . . 3 class V
4 vi . . . 4 setvar 𝑖
52cv 1652 . . . . . 6 class 𝑟
6 cpl1 19868 . . . . . 6 class Poly1
75, 6cfv 6102 . . . . 5 class (Poly1𝑟)
8 clidl 19492 . . . . 5 class LIdeal
97, 8cfv 6102 . . . 4 class (LIdeal‘(Poly1𝑟))
104cv 1652 . . . . . 6 class 𝑖
11 c0g 16414 . . . . . . . 8 class 0g
127, 11cfv 6102 . . . . . . 7 class (0g‘(Poly1𝑟))
1312csn 4369 . . . . . 6 class {(0g‘(Poly1𝑟))}
1410, 13wceq 1653 . . . . 5 wff 𝑖 = {(0g‘(Poly1𝑟))}
15 vg . . . . . . . . 9 setvar 𝑔
1615cv 1652 . . . . . . . 8 class 𝑔
17 cdg1 24154 . . . . . . . . 9 class deg1
185, 17cfv 6102 . . . . . . . 8 class ( deg1𝑟)
1916, 18cfv 6102 . . . . . . 7 class (( deg1𝑟)‘𝑔)
2010, 13cdif 3767 . . . . . . . . 9 class (𝑖 ∖ {(0g‘(Poly1𝑟))})
2118, 20cima 5316 . . . . . . . 8 class (( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))}))
22 cr 10224 . . . . . . . 8 class
23 clt 10364 . . . . . . . 8 class <
2421, 22, 23cinf 8590 . . . . . . 7 class inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < )
2519, 24wceq 1653 . . . . . 6 wff (( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < )
26 cmn1 24225 . . . . . . . 8 class Monic1p
275, 26cfv 6102 . . . . . . 7 class (Monic1p𝑟)
2810, 27cin 3769 . . . . . 6 class (𝑖 ∩ (Monic1p𝑟))
2925, 15, 28crio 6839 . . . . 5 class (𝑔 ∈ (𝑖 ∩ (Monic1p𝑟))(( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < ))
3014, 12, 29cif 4278 . . . 4 class if(𝑖 = {(0g‘(Poly1𝑟))}, (0g‘(Poly1𝑟)), (𝑔 ∈ (𝑖 ∩ (Monic1p𝑟))(( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < )))
314, 9, 30cmpt 4923 . . 3 class (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ if(𝑖 = {(0g‘(Poly1𝑟))}, (0g‘(Poly1𝑟)), (𝑔 ∈ (𝑖 ∩ (Monic1p𝑟))(( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < ))))
322, 3, 31cmpt 4923 . 2 class (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ if(𝑖 = {(0g‘(Poly1𝑟))}, (0g‘(Poly1𝑟)), (𝑔 ∈ (𝑖 ∩ (Monic1p𝑟))(( deg1𝑟)‘𝑔) = inf((( deg1𝑟) “ (𝑖 ∖ {(0g‘(Poly1𝑟))})), ℝ, < )))))
331, 32wceq 1653 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  24272
  Copyright terms: Public domain W3C validator