Theorem hbtlem3

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

	Ref	Expression
Hypotheses	hbtlem.p	|- P = ( Poly1 ` R )
	hbtlem.u	|- U = ( LIdeal ` P )
	hbtlem.s	|- S = ( ldgIdlSeq ` R )
	hbtlem3.r	|- ( ph -> R e. Ring )
	hbtlem3.i	|- ( ph -> I e. U )
	hbtlem3.j	|- ( ph -> J e. U )
	hbtlem3.ij	|- ( ph -> I C_ J )
	hbtlem3.x	|- ( ph -> X e. NN0 )
Assertion	hbtlem3	|- ( ph -> ( ( S ` I ) ` X ) C_ ( ( S ` J ) ` X ) )

Proof

Step	Hyp	Ref	Expression
1		hbtlem.p	|- P = ( Poly1 ` R )
2		hbtlem.u	|- U = ( LIdeal ` P )
3		hbtlem.s	|- S = ( ldgIdlSeq ` R )
4		hbtlem3.r	|- ( ph -> R e. Ring )
5		hbtlem3.i	|- ( ph -> I e. U )
6		hbtlem3.j	|- ( ph -> J e. U )
7		hbtlem3.ij	|- ( ph -> I C_ J )
8		hbtlem3.x	|- ( ph -> X e. NN0 )
9		ssrexv	|- ( I C_ J -> ( E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) -> E. b e. J ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) ) )
10	7 9	syl	|- ( ph -> ( E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) -> E. b e. J ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) ) )
11	10	ss2abdv	|- ( ph -> { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } C_ { a | E. b e. J ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } )
12		eqid	|- ( deg1 ` R ) = ( deg1 ` R )
13	1 2 3 12	hbtlem1	|- ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( ( S ` I ) ` X ) = { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } )
14	4 5 8 13	syl3anc	|- ( ph -> ( ( S ` I ) ` X ) = { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } )
15	1 2 3 12	hbtlem1	|- ( ( R e. Ring /\ J e. U /\ X e. NN0 ) -> ( ( S ` J ) ` X ) = { a | E. b e. J ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } )
16	4 6 8 15	syl3anc	|- ( ph -> ( ( S ` J ) ` X ) = { a | E. b e. J ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } )
17	11 14 16	3sstr4d	|- ( ph -> ( ( S ` I ) ` X ) C_ ( ( S ` J ) ` X ) )