Definition df-ig1p 25652

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

Step	Hyp	Ref	Expression
1		cig1p 25647	. 2 class idlGen1p
2		vr	. . 3 setvar 𝑟
3		cvv 3475	. . 3 class V
4		vi	. . . 4 setvar 𝑖
5	2	cv 1541	. . . . . 6 class 𝑟
6		cpl1 21701	. . . . . 6 class Poly1
7	5, 6	cfv 6544	. . . . 5 class (Poly1‘𝑟)
8		clidl 20783	. . . . 5 class LIdeal
9	7, 8	cfv 6544	. . . 4 class (LIdeal‘(Poly1‘𝑟))
10	4	cv 1541	. . . . . 6 class 𝑖
11		c0g 17385	. . . . . . . 8 class 0g
12	7, 11	cfv 6544	. . . . . . 7 class (0g‘(Poly1‘𝑟))
13	12	csn 4629	. . . . . 6 class {(0g‘(Poly1‘𝑟))}
14	10, 13	wceq 1542	. . . . 5 wff 𝑖 = {(0g‘(Poly1‘𝑟))}
15		vg	. . . . . . . . 9 setvar 𝑔
16	15	cv 1541	. . . . . . . 8 class 𝑔
17		cdg1 25569	. . . . . . . . 9 class deg1
18	5, 17	cfv 6544	. . . . . . . 8 class ( deg1 ‘𝑟)
19	16, 18	cfv 6544	. . . . . . 7 class (( deg1 ‘𝑟)‘𝑔)
20	10, 13	cdif 3946	. . . . . . . . 9 class (𝑖 ∖ {(0g‘(Poly1‘𝑟))})
21	18, 20	cima 5680	. . . . . . . 8 class (( deg1 ‘𝑟) “ (𝑖 ∖ {(0g‘(Poly1‘𝑟))}))
22		cr 11109	. . . . . . . 8 class ℝ
23		clt 11248	. . . . . . . 8 class <
24	21, 22, 23	cinf 9436	. . . . . . 7 class inf((( deg1 ‘𝑟) “ (𝑖 ∖ {(0g‘(Poly1‘𝑟))})), ℝ, < )
25	19, 24	wceq 1542	. . . . . 6 wff (( deg1 ‘𝑟)‘𝑔) = inf((( deg1 ‘𝑟) “ (𝑖 ∖ {(0g‘(Poly1‘𝑟))})), ℝ, < )
26		cmn1 25643	. . . . . . . 8 class Monic1p
27	5, 26	cfv 6544	. . . . . . 7 class (Monic1p‘𝑟)
28	10, 27	cin 3948	. . . . . 6 class (𝑖 ∩ (Monic1p‘𝑟))
29	25, 15, 28	crio 7364	. . . . 5 class (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))(( deg1 ‘𝑟)‘𝑔) = inf((( deg1 ‘𝑟) “ (𝑖 ∖ {(0g‘(Poly1‘𝑟))})), ℝ, < ))
30	14, 12, 29	cif 4529	. . . 4 class if(𝑖 = {(0g‘(Poly1‘𝑟))}, (0g‘(Poly1‘𝑟)), (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))(( deg1 ‘𝑟)‘𝑔) = inf((( deg1 ‘𝑟) “ (𝑖 ∖ {(0g‘(Poly1‘𝑟))})), ℝ, < )))
31	4, 9, 30	cmpt 5232	. . 3 class (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ if(𝑖 = {(0g‘(Poly1‘𝑟))}, (0g‘(Poly1‘𝑟)), (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))(( deg1 ‘𝑟)‘𝑔) = inf((( deg1 ‘𝑟) “ (𝑖 ∖ {(0g‘(Poly1‘𝑟))})), ℝ, < ))))
32	2, 3, 31	cmpt 5232	. 2 class (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ if(𝑖 = {(0g‘(Poly1‘𝑟))}, (0g‘(Poly1‘𝑟)), (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))(( deg1 ‘𝑟)‘𝑔) = inf((( deg1 ‘𝑟) “ (𝑖 ∖ {(0g‘(Poly1‘𝑟))})), ℝ, < )))))
33	1, 32	wceq 1542	1 wff idlGen1p = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ if(𝑖 = {(0g‘(Poly1‘𝑟))}, (0g‘(Poly1‘𝑟)), (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))(( deg1 ‘𝑟)‘𝑔) = inf((( deg1 ‘𝑟) “ (𝑖 ∖ {(0g‘(Poly1‘𝑟))})), ℝ, < )))))

This definition is referenced by:  ig1pval  25690