Definition df-ldgis

Description: Define a function which carries polynomial ideals to the sequence of coefficient ideals of leading coefficients of degree- x elements in the polynomial ideal. The proof that this map is strictly monotone is the core of the Hilbert Basis Theorem hbt . (Contributed by Stefan O'Rear, 31-Mar-2015)

	Ref	Expression
Assertion	df-ldgis	⊢ ldgIdlSeq = ( 𝑟 ∈ V ↦ ( 𝑖 ∈ ( LIdeal ‘ ( Poly1 ‘ 𝑟 ) ) ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘 ∈ 𝑖 ( ( ( deg1 ‘ 𝑟 ) ‘ 𝑘 ) ≤ 𝑥 ∧ 𝑗 = ( ( coe1 ‘ 𝑘 ) ‘ 𝑥 ) ) } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cldgis	⊢ ldgIdlSeq
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		vx	⊢ 𝑥
10		cn0	⊢ ℕ0
11		vj	⊢ 𝑗
12		vk	⊢ 𝑘
13	3	cv	⊢ 𝑖
14		cdg1	⊢ deg1
15	6 14	cfv	⊢ ( deg1 ‘ 𝑟 )
16	12	cv	⊢ 𝑘
17	16 15	cfv	⊢ ( ( deg1 ‘ 𝑟 ) ‘ 𝑘 )
18		cle	⊢ ≤
19	9	cv	⊢ 𝑥
20	17 19 18	wbr	⊢ ( ( deg1 ‘ 𝑟 ) ‘ 𝑘 ) ≤ 𝑥
21	11	cv	⊢ 𝑗
22		cco1	⊢ coe1
23	16 22	cfv	⊢ ( coe1 ‘ 𝑘 )
24	19 23	cfv	⊢ ( ( coe1 ‘ 𝑘 ) ‘ 𝑥 )
25	21 24	wceq	⊢ 𝑗 = ( ( coe1 ‘ 𝑘 ) ‘ 𝑥 )
26	20 25	wa	⊢ ( ( ( deg1 ‘ 𝑟 ) ‘ 𝑘 ) ≤ 𝑥 ∧ 𝑗 = ( ( coe1 ‘ 𝑘 ) ‘ 𝑥 ) )
27	26 12 13	wrex	⊢ ∃ 𝑘 ∈ 𝑖 ( ( ( deg1 ‘ 𝑟 ) ‘ 𝑘 ) ≤ 𝑥 ∧ 𝑗 = ( ( coe1 ‘ 𝑘 ) ‘ 𝑥 ) )
28	27 11	cab	⊢ { 𝑗 ∣ ∃ 𝑘 ∈ 𝑖 ( ( ( deg1 ‘ 𝑟 ) ‘ 𝑘 ) ≤ 𝑥 ∧ 𝑗 = ( ( coe1 ‘ 𝑘 ) ‘ 𝑥 ) ) }
29	9 10 28	cmpt	⊢ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘 ∈ 𝑖 ( ( ( deg1 ‘ 𝑟 ) ‘ 𝑘 ) ≤ 𝑥 ∧ 𝑗 = ( ( coe1 ‘ 𝑘 ) ‘ 𝑥 ) ) } )
30	3 8 29	cmpt	⊢ ( 𝑖 ∈ ( LIdeal ‘ ( Poly1 ‘ 𝑟 ) ) ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘 ∈ 𝑖 ( ( ( deg1 ‘ 𝑟 ) ‘ 𝑘 ) ≤ 𝑥 ∧ 𝑗 = ( ( coe1 ‘ 𝑘 ) ‘ 𝑥 ) ) } ) )
31	1 2 30	cmpt	⊢ ( 𝑟 ∈ V ↦ ( 𝑖 ∈ ( LIdeal ‘ ( Poly1 ‘ 𝑟 ) ) ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘 ∈ 𝑖 ( ( ( deg1 ‘ 𝑟 ) ‘ 𝑘 ) ≤ 𝑥 ∧ 𝑗 = ( ( coe1 ‘ 𝑘 ) ‘ 𝑥 ) ) } ) ) )
32	0 31	wceq	⊢ ldgIdlSeq = ( 𝑟 ∈ V ↦ ( 𝑖 ∈ ( LIdeal ‘ ( Poly1 ‘ 𝑟 ) ) ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘 ∈ 𝑖 ( ( ( deg1 ‘ 𝑟 ) ‘ 𝑘 ) ≤ 𝑥 ∧ 𝑗 = ( ( coe1 ‘ 𝑘 ) ‘ 𝑥 ) ) } ) ) )