This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑟 ) ) } ) ) , ℝ , < ) ) ) ) )