Theorem hbtlem3

Description: The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015)

	Ref	Expression
Hypotheses	hbtlem.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	hbtlem.u	⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
	hbtlem.s	⊢ 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
	hbtlem3.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	hbtlem3.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
	hbtlem3.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑈 )
	hbtlem3.ij	⊢ ( 𝜑 → 𝐼 ⊆ 𝐽 )
	hbtlem3.x	⊢ ( 𝜑 → 𝑋 ∈ ℕ0 )
Assertion	hbtlem3	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		hbtlem.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		hbtlem.u	⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
3		hbtlem.s	⊢ 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
4		hbtlem3.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		hbtlem3.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
6		hbtlem3.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑈 )
7		hbtlem3.ij	⊢ ( 𝜑 → 𝐼 ⊆ 𝐽 )
8		hbtlem3.x	⊢ ( 𝜑 → 𝑋 ∈ ℕ0 )
9		ssrexv	⊢ ( 𝐼 ⊆ 𝐽 → ( ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) → ∃ 𝑏 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) )
10	7 9	syl	⊢ ( 𝜑 → ( ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) → ∃ 𝑏 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) )
11	10	ss2abdv	⊢ ( 𝜑 → { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ⊆ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
12		eqid	⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
13	1 2 3 12	hbtlem1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
14	4 5 8 13	syl3anc	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
15	1 2 3 12	hbtlem1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐽 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑋 ) = { 𝑎 ∣ ∃ 𝑏 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
16	4 6 8 15	syl3anc	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑋 ) = { 𝑎 ∣ ∃ 𝑏 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
17	11 14 16	3sstr4d	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑋 ) )