hbtlem4

Description: The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015)

	Ref	Expression
Hypotheses	hbtlem.p	$⊢ P = {Poly}_{1} (R)$
	hbtlem.u	$⊢ U = LIdeal (P)$
	hbtlem.s	$⊢ S = ldgIdlSeq (R)$
	hbtlem4.r	$⊢ φ \to R \in Ring$
	hbtlem4.i	$⊢ φ \to I \in U$
	hbtlem4.x	$⊢ φ \to X \in ℕ_{0}$
	hbtlem4.y	$⊢ φ \to Y \in ℕ_{0}$
	hbtlem4.xy	$⊢ φ \to X \leq Y$
Assertion	hbtlem4	$⊢ φ \to S (I) (X) \subseteq S (I) (Y)$

Proof

Step	Hyp	Ref	Expression
1		hbtlem.p	$⊢ P = {Poly}_{1} (R)$
2		hbtlem.u	$⊢ U = LIdeal (P)$
3		hbtlem.s	$⊢ S = ldgIdlSeq (R)$
4		hbtlem4.r	$⊢ φ \to R \in Ring$
5		hbtlem4.i	$⊢ φ \to I \in U$
6		hbtlem4.x	$⊢ φ \to X \in ℕ_{0}$
7		hbtlem4.y	$⊢ φ \to Y \in ℕ_{0}$
8		hbtlem4.xy	$⊢ φ \to X \leq Y$
9	4	ad2antrr	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to R \in Ring$
10	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
11	9 10	syl	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to P \in Ring$
12	5	ad2antrr	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to I \in U$
13		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
14		eqid	$⊢ {Base}_{P} = {Base}_{P}$
15	13 14	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
16		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
17	13	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
18	11 17	syl	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to {mulGrp}_{P} \in Mnd$
19	6	ad2antrr	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to X \in ℕ_{0}$
20	7	ad2antrr	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to Y \in ℕ_{0}$
21	8	ad2antrr	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to X \leq Y$
22		nn0sub2	$⊢ (X \in ℕ_{0} \land Y \in ℕ_{0} \land X \leq Y) \to Y - X \in ℕ_{0}$
23	19 20 21 22	syl3anc	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to Y - X \in ℕ_{0}$
24		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
25	24 1 14	vr1cl	$⊢ R \in Ring \to {var}_{1} (R) \in {Base}_{P}$
26	9 25	syl	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to {var}_{1} (R) \in {Base}_{P}$
27	15 16 18 23 26	mulgnn0cld	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to (Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in {Base}_{P}$
28		simplr	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to c \in I$
29		eqid	$⊢ \cdot_{P} = \cdot_{P}$
30	2 14 29	lidlmcl	$⊢ ((P \in Ring \land I \in U) \land ((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in {Base}_{P} \land c \in I)) \to ((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c \in I$
31	11 12 27 28 30	syl22anc	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to ((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c \in I$
32		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
33	14 2	lidlss	$⊢ I \in U \to I \subseteq {Base}_{P}$
34	12 33	syl	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to I \subseteq {Base}_{P}$
35	34 28	sseldd	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to c \in {Base}_{P}$
36	32 1 24 13 16	deg1pwle	$⊢ (R \in Ring \land Y - X \in ℕ_{0}) \to \deg_{1} (R) ((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \leq Y - X$
37	9 23 36	syl2anc	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to \deg_{1} (R) ((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \leq Y - X$
38		simpr	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to \deg_{1} (R) (c) \leq X$
39	1 32 9 14 29 27 35 23 19 37 38	deg1mulle2	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to \deg_{1} (R) (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c) \leq Y - X + X$
40	20	nn0cnd	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to Y \in ℂ$
41	19	nn0cnd	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to X \in ℂ$
42	40 41	npcand	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to Y - X + X = Y$
43	39 42	breqtrd	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to \deg_{1} (R) (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c) \leq Y$
44		eqid	$⊢ 0_{R} = 0_{R}$
45	44 1 24 13 16 14 29 9 35 23 19	coe1pwmulfv	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to {coe}_{1} (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c) (Y - X + X) = {coe}_{1} (c) (X)$
46	42	fveq2d	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to {coe}_{1} (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c) (Y - X + X) = {coe}_{1} (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c) (Y)$
47	45 46	eqtr3d	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to {coe}_{1} (c) (X) = {coe}_{1} (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c) (Y)$
48		fveq2	$⊢ b = ((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c \to \deg_{1} (R) (b) = \deg_{1} (R) (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c)$
49	48	breq1d	$⊢ b = ((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c \to (\deg_{1} (R) (b) \leq Y \leftrightarrow \deg_{1} (R) (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c) \leq Y)$
50		fveq2	$⊢ b = ((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c \to {coe}_{1} (b) = {coe}_{1} (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c)$
51	50	fveq1d	$⊢ b = ((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c \to {coe}_{1} (b) (Y) = {coe}_{1} (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c) (Y)$
52	51	eqeq2d	$⊢ b = ((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c \to ({coe}_{1} (c) (X) = {coe}_{1} (b) (Y) \leftrightarrow {coe}_{1} (c) (X) = {coe}_{1} (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c) (Y))$
53	49 52	anbi12d	$⊢ b = ((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c \to ((\deg_{1} (R) (b) \leq Y \land {coe}_{1} (c) (X) = {coe}_{1} (b) (Y)) \leftrightarrow (\deg_{1} (R) (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c) \leq Y \land {coe}_{1} (c) (X) = {coe}_{1} (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c) (Y)))$
54	53	rspcev	$⊢ (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c \in I \land (\deg_{1} (R) (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c) \leq Y \land {coe}_{1} (c) (X) = {coe}_{1} (((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \cdot_{P} c) (Y))) \to \exists b \in I (\deg_{1} (R) (b) \leq Y \land {coe}_{1} (c) (X) = {coe}_{1} (b) (Y))$
55	31 43 47 54	syl12anc	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to \exists b \in I (\deg_{1} (R) (b) \leq Y \land {coe}_{1} (c) (X) = {coe}_{1} (b) (Y))$
56		eqeq1	$⊢ a = {coe}_{1} (c) (X) \to (a = {coe}_{1} (b) (Y) \leftrightarrow {coe}_{1} (c) (X) = {coe}_{1} (b) (Y))$
57	56	anbi2d	$⊢ a = {coe}_{1} (c) (X) \to ((\deg_{1} (R) (b) \leq Y \land a = {coe}_{1} (b) (Y)) \leftrightarrow (\deg_{1} (R) (b) \leq Y \land {coe}_{1} (c) (X) = {coe}_{1} (b) (Y)))$
58	57	rexbidv	$⊢ a = {coe}_{1} (c) (X) \to (\exists b \in I (\deg_{1} (R) (b) \leq Y \land a = {coe}_{1} (b) (Y)) \leftrightarrow \exists b \in I (\deg_{1} (R) (b) \leq Y \land {coe}_{1} (c) (X) = {coe}_{1} (b) (Y)))$
59	55 58	syl5ibrcom	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to (a = {coe}_{1} (c) (X) \to \exists b \in I (\deg_{1} (R) (b) \leq Y \land a = {coe}_{1} (b) (Y)))$
60	59	expimpd	$⊢ (φ \land c \in I) \to ((\deg_{1} (R) (c) \leq X \land a = {coe}_{1} (c) (X)) \to \exists b \in I (\deg_{1} (R) (b) \leq Y \land a = {coe}_{1} (b) (Y)))$
61	60	rexlimdva	$⊢ φ \to (\exists c \in I (\deg_{1} (R) (c) \leq X \land a = {coe}_{1} (c) (X)) \to \exists b \in I (\deg_{1} (R) (b) \leq Y \land a = {coe}_{1} (b) (Y)))$
62	61	ss2abdv	$⊢ φ \to \{a \| \exists c \in I (\deg_{1} (R) (c) \leq X \land a = {coe}_{1} (c) (X))\} \subseteq \{a \| \exists b \in I (\deg_{1} (R) (b) \leq Y \land a = {coe}_{1} (b) (Y))\}$
63	1 2 3 32	hbtlem1	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to S (I) (X) = \{a \| \exists c \in I (\deg_{1} (R) (c) \leq X \land a = {coe}_{1} (c) (X))\}$
64	4 5 6 63	syl3anc	$⊢ φ \to S (I) (X) = \{a \| \exists c \in I (\deg_{1} (R) (c) \leq X \land a = {coe}_{1} (c) (X))\}$
65	1 2 3 32	hbtlem1	$⊢ (R \in Ring \land I \in U \land Y \in ℕ_{0}) \to S (I) (Y) = \{a \| \exists b \in I (\deg_{1} (R) (b) \leq Y \land a = {coe}_{1} (b) (Y))\}$
66	4 5 7 65	syl3anc	$⊢ φ \to S (I) (Y) = \{a \| \exists b \in I (\deg_{1} (R) (b) \leq Y \land a = {coe}_{1} (b) (Y))\}$
67	62 64 66	3sstr4d	$⊢ φ \to S (I) (X) \subseteq S (I) (Y)$

Metamath Proof Explorer

Theorem hbtlem4

Proof