Definition df-ig1p

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)

	Ref	Expression
Assertion	df-ig1p	⊢ idlGen1p = ( 𝑟 ∈ V ↦ ( 𝑖 ∈ ( LIdeal ‘ ( Poly1 ‘ 𝑟 ) ) ↦ if ( 𝑖 = { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } , ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) , ( ℩ 𝑔 ∈ ( 𝑖 ∩ ( Monic1p ‘ 𝑟 ) ) ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) = inf ( ( ( deg1 ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } ) ) , ℝ , < ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cig1p	⊢ idlGen1p
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vi	⊢ 𝑖
4		clidl	⊢ LIdeal
5		cpl1	⊢ Poly1
6	1	cv	⊢ 𝑟
7	6 5	cfv	⊢ ( Poly1 ‘ 𝑟 )
8	7 4	cfv	⊢ ( LIdeal ‘ ( Poly1 ‘ 𝑟 ) )
9	3	cv	⊢ 𝑖
10		c0g	⊢ 0g
11	7 10	cfv	⊢ ( 0g ‘ ( Poly1 ‘ 𝑟 ) )
12	11	csn	⊢ { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) }
13	9 12	wceq	⊢ 𝑖 = { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) }
14		vg	⊢ 𝑔
15		cmn1	⊢ Monic1p
16	6 15	cfv	⊢ ( Monic1p ‘ 𝑟 )
17	9 16	cin	⊢ ( 𝑖 ∩ ( Monic1p ‘ 𝑟 ) )
18		cdg1	⊢ deg1
19	6 18	cfv	⊢ ( deg1 ‘ 𝑟 )
20	14	cv	⊢ 𝑔
21	20 19	cfv	⊢ ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 )
22	9 12	cdif	⊢ ( 𝑖 ∖ { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } )
23	19 22	cima	⊢ ( ( deg1 ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } ) )
24		cr	⊢ ℝ
25		clt	⊢ <
26	23 24 25	cinf	⊢ inf ( ( ( deg1 ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } ) ) , ℝ , < )
27	21 26	wceq	⊢ ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) = inf ( ( ( deg1 ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } ) ) , ℝ , < )
28	27 14 17	crio	⊢ ( ℩ 𝑔 ∈ ( 𝑖 ∩ ( Monic1p ‘ 𝑟 ) ) ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) = inf ( ( ( deg1 ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } ) ) , ℝ , < ) )
29	13 11 28	cif	⊢ if ( 𝑖 = { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } , ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) , ( ℩ 𝑔 ∈ ( 𝑖 ∩ ( Monic1p ‘ 𝑟 ) ) ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) = inf ( ( ( deg1 ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } ) ) , ℝ , < ) ) )
30	3 8 29	cmpt	⊢ ( 𝑖 ∈ ( LIdeal ‘ ( Poly1 ‘ 𝑟 ) ) ↦ if ( 𝑖 = { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } , ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) , ( ℩ 𝑔 ∈ ( 𝑖 ∩ ( Monic1p ‘ 𝑟 ) ) ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) = inf ( ( ( deg1 ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } ) ) , ℝ , < ) ) ) )
31	1 2 30	cmpt	⊢ ( 𝑟 ∈ V ↦ ( 𝑖 ∈ ( LIdeal ‘ ( Poly1 ‘ 𝑟 ) ) ↦ if ( 𝑖 = { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } , ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) , ( ℩ 𝑔 ∈ ( 𝑖 ∩ ( Monic1p ‘ 𝑟 ) ) ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) = inf ( ( ( deg1 ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } ) ) , ℝ , < ) ) ) ) )
32	0 31	wceq	⊢ idlGen1p = ( 𝑟 ∈ V ↦ ( 𝑖 ∈ ( LIdeal ‘ ( Poly1 ‘ 𝑟 ) ) ↦ if ( 𝑖 = { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } , ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) , ( ℩ 𝑔 ∈ ( 𝑖 ∩ ( Monic1p ‘ 𝑟 ) ) ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) = inf ( ( ( deg1 ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) } ) ) , ℝ , < ) ) ) ) )