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	13	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
15	11 14	syl	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to {mulGrp}_{P} \in Mnd$
16	6	ad2antrr	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to X \in ℕ_{0}$
17	7	ad2antrr	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to Y \in ℕ_{0}$
18	8	ad2antrr	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to X \leq Y$
19		nn0sub2	$⊢ (X \in ℕ_{0} \land Y \in ℕ_{0} \land X \leq Y) \to Y - X \in ℕ_{0}$
20	16 17 18 19	syl3anc	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to Y - X \in ℕ_{0}$
21		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
22		eqid	$⊢ {Base}_{P} = {Base}_{P}$
23	21 1 22	vr1cl	$⊢ R \in Ring \to {var}_{1} (R) \in {Base}_{P}$
24	9 23	syl	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to {var}_{1} (R) \in {Base}_{P}$
25	13 22	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
26		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
27	25 26	mulgnn0cl	$⊢ ({mulGrp}_{P} \in Mnd \land Y - X \in ℕ_{0} \land {var}_{1} (R) \in {Base}_{P}) \to (Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in {Base}_{P}$
28	15 20 24 27	syl3anc	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to (Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in {Base}_{P}$
29		simplr	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to c \in I$
30		eqid	$⊢ \cdot_{P} = \cdot_{P}$
31	2 22 30	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$
32	11 12 28 29 31	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$
33		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
34	22 2	lidlss	$⊢ I \in U \to I \subseteq {Base}_{P}$
35	12 34	syl	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to I \subseteq {Base}_{P}$
36	35 29	sseldd	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to c \in {Base}_{P}$
37	33 1 21 13 26	deg1pwle	$⊢ (R \in Ring \land Y - X \in ℕ_{0}) \to \deg_{1} (R) ((Y - X) \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \leq Y - X$
38	9 20 37	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$
39		simpr	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to \deg_{1} (R) (c) \leq X$
40	1 33 9 22 30 28 36 20 16 38 39	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$
41	17	nn0cnd	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to Y \in ℂ$
42	16	nn0cnd	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to X \in ℂ$
43	41 42	npcand	$⊢ ((φ \land c \in I) \land \deg_{1} (R) (c) \leq X) \to Y - X + X = Y$
44	40 43	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$
45		eqid	$⊢ 0_{R} = 0_{R}$
46	45 1 21 13 26 22 30 9 36 20 16	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)$
47	43	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)$
48	46 47	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)$
49		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)$
50	49	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)$
51		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)$
52	51	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)$
53	52	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))$
54	50 53	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)))$
55	54	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))$
56	32 44 48 55	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))$
57		eqeq1	$⊢ a = {coe}_{1} (c) (X) \to (a = {coe}_{1} (b) (Y) \leftrightarrow {coe}_{1} (c) (X) = {coe}_{1} (b) (Y))$
58	57	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)))$
59	58	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)))$
60	56 59	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)))$
61	60	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)))$
62	61	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)))$
63	62	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))\}$
64	1 2 3 33	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))\}$
65	4 5 6 64	syl3anc	$⊢ φ \to S (I) (X) = \{a \| \exists c \in I (\deg_{1} (R) (c) \leq X \land a = {coe}_{1} (c) (X))\}$
66	1 2 3 33	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))\}$
67	4 5 7 66	syl3anc	$⊢ φ \to S (I) (Y) = \{a \| \exists b \in I (\deg_{1} (R) (b) \leq Y \land a = {coe}_{1} (b) (Y))\}$
68	63 65 67	3sstr4d	$⊢ φ \to S (I) (X) \subseteq S (I) (Y)$

Metamath Proof Explorer

Theorem hbtlem4

Proof