Metamath Proof Explorer

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 = r ∈ V ⟼ i ∈ LIdeal ⁡ Poly 1 ⁡ r ⟼ x ∈ ℕ 0 ⟼ j | ∃ k ∈ i deg 1 ⁡ r ⁡ k ≤ x ∧ j = coe 1 ⁡ k ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cldgis class ldgIdlSeq
1 vr setvar r
2 cvv class V
3 vi setvar i
4 clidl class LIdeal
5 cpl1 class Poly 1
6 1 cv setvar r
7 6 5 cfv class Poly 1 ⁡ r
8 7 4 cfv class LIdeal ⁡ Poly 1 ⁡ r
9 vx setvar x
10 cn0 class ℕ 0
11 vj setvar j
12 vk setvar k
13 3 cv setvar i
14 cdg1 class deg 1
15 6 14 cfv class deg 1 ⁡ r
16 12 cv setvar k
17 16 15 cfv class deg 1 ⁡ r ⁡ k
18 cle class ≤
19 9 cv setvar x
20 17 19 18 wbr wff deg 1 ⁡ r ⁡ k ≤ x
21 11 cv setvar j
22 cco1 class coe 1
23 16 22 cfv class coe 1 ⁡ k
24 19 23 cfv class coe 1 ⁡ k ⁡ x
25 21 24 wceq wff j = coe 1 ⁡ k ⁡ x
26 20 25 wa wff deg 1 ⁡ r ⁡ k ≤ x ∧ j = coe 1 ⁡ k ⁡ x
27 26 12 13 wrex wff ∃ k ∈ i deg 1 ⁡ r ⁡ k ≤ x ∧ j = coe 1 ⁡ k ⁡ x
28 27 11 cab class j | ∃ k ∈ i deg 1 ⁡ r ⁡ k ≤ x ∧ j = coe 1 ⁡ k ⁡ x
29 9 10 28 cmpt class x ∈ ℕ 0 ⟼ j | ∃ k ∈ i deg 1 ⁡ r ⁡ k ≤ x ∧ j = coe 1 ⁡ k ⁡ x
30 3 8 29 cmpt class i ∈ LIdeal ⁡ Poly 1 ⁡ r ⟼ x ∈ ℕ 0 ⟼ j | ∃ k ∈ i deg 1 ⁡ r ⁡ k ≤ x ∧ j = coe 1 ⁡ k ⁡ x
31 1 2 30 cmpt class r ∈ V ⟼ i ∈ LIdeal ⁡ Poly 1 ⁡ r ⟼ x ∈ ℕ 0 ⟼ j | ∃ k ∈ i deg 1 ⁡ r ⁡ k ≤ x ∧ j = coe 1 ⁡ k ⁡ x
32 0 31 wceq wff ldgIdlSeq = r ∈ V ⟼ i ∈ LIdeal ⁡ Poly 1 ⁡ r ⟼ x ∈ ℕ 0 ⟼ j | ∃ k ∈ i deg 1 ⁡ r ⁡ k ≤ x ∧ j = coe 1 ⁡ k ⁡ x