hbtlem5

Description: The leading ideal function is strictly monotone. (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)$
	hbtlem3.r	$⊢ φ \to R \in Ring$
	hbtlem3.i	$⊢ φ \to I \in U$
	hbtlem3.j	$⊢ φ \to J \in U$
	hbtlem3.ij	$⊢ φ \to I \subseteq J$
	hbtlem5.e	$⊢ φ \to \forall x \in ℕ_{0} S (J) (x) \subseteq S (I) (x)$
Assertion	hbtlem5	$⊢ φ \to I = J$

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		hbtlem3.r	$⊢ φ \to R \in Ring$
5		hbtlem3.i	$⊢ φ \to I \in U$
6		hbtlem3.j	$⊢ φ \to J \in U$
7		hbtlem3.ij	$⊢ φ \to I \subseteq J$
8		hbtlem5.e	$⊢ φ \to \forall x \in ℕ_{0} S (J) (x) \subseteq S (I) (x)$
9		eqid	$⊢ {Base}_{P} = {Base}_{P}$
10	9 2	lidlss	$⊢ J \in U \to J \subseteq {Base}_{P}$
11	6 10	syl	$⊢ φ \to J \subseteq {Base}_{P}$
12	11	sselda	$⊢ (φ \land a \in J) \to a \in {Base}_{P}$
13		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
14	13 1 9	deg1cl	$⊢ a \in {Base}_{P} \to \deg_{1} (R) (a) \in (ℕ_{0} \cup \{−∞\})$
15	12 14	syl	$⊢ (φ \land a \in J) \to \deg_{1} (R) (a) \in (ℕ_{0} \cup \{−∞\})$
16		elun	$⊢ \deg_{1} (R) (a) \in (ℕ_{0} \cup \{−∞\}) \leftrightarrow (\deg_{1} (R) (a) \in ℕ_{0} \lor \deg_{1} (R) (a) \in \{−∞\})$
17		nnssnn0	$⊢ ℕ \subseteq ℕ_{0}$
18		nn0re	$⊢ \deg_{1} (R) (a) \in ℕ_{0} \to \deg_{1} (R) (a) \in ℝ$
19		arch	$⊢ \deg_{1} (R) (a) \in ℝ \to \exists b \in ℕ \deg_{1} (R) (a) < b$
20	18 19	syl	$⊢ \deg_{1} (R) (a) \in ℕ_{0} \to \exists b \in ℕ \deg_{1} (R) (a) < b$
21		ssrexv	$⊢ ℕ \subseteq ℕ_{0} \to (\exists b \in ℕ \deg_{1} (R) (a) < b \to \exists b \in ℕ_{0} \deg_{1} (R) (a) < b)$
22	17 20 21	mpsyl	$⊢ \deg_{1} (R) (a) \in ℕ_{0} \to \exists b \in ℕ_{0} \deg_{1} (R) (a) < b$
23		elsni	$⊢ \deg_{1} (R) (a) \in \{−∞\} \to \deg_{1} (R) (a) = −∞$
24		0nn0	$⊢ 0 \in ℕ_{0}$
25		mnflt0	$⊢ −∞ < 0$
26		breq2	$⊢ b = 0 \to (−∞ < b \leftrightarrow −∞ < 0)$
27	26	rspcev	$⊢ (0 \in ℕ_{0} \land −∞ < 0) \to \exists b \in ℕ_{0} −∞ < b$
28	24 25 27	mp2an	$⊢ \exists b \in ℕ_{0} −∞ < b$
29		breq1	$⊢ \deg_{1} (R) (a) = −∞ \to (\deg_{1} (R) (a) < b \leftrightarrow −∞ < b)$
30	29	rexbidv	$⊢ \deg_{1} (R) (a) = −∞ \to (\exists b \in ℕ_{0} \deg_{1} (R) (a) < b \leftrightarrow \exists b \in ℕ_{0} −∞ < b)$
31	28 30	mpbiri	$⊢ \deg_{1} (R) (a) = −∞ \to \exists b \in ℕ_{0} \deg_{1} (R) (a) < b$
32	23 31	syl	$⊢ \deg_{1} (R) (a) \in \{−∞\} \to \exists b \in ℕ_{0} \deg_{1} (R) (a) < b$
33	22 32	jaoi	$⊢ (\deg_{1} (R) (a) \in ℕ_{0} \lor \deg_{1} (R) (a) \in \{−∞\}) \to \exists b \in ℕ_{0} \deg_{1} (R) (a) < b$
34	16 33	sylbi	$⊢ \deg_{1} (R) (a) \in (ℕ_{0} \cup \{−∞\}) \to \exists b \in ℕ_{0} \deg_{1} (R) (a) < b$
35	15 34	syl	$⊢ (φ \land a \in J) \to \exists b \in ℕ_{0} \deg_{1} (R) (a) < b$
36		breq2	$⊢ c = 0 \to (\deg_{1} (R) (a) < c \leftrightarrow \deg_{1} (R) (a) < 0)$
37	36	imbi1d	$⊢ c = 0 \to ((\deg_{1} (R) (a) < c \to a \in I) \leftrightarrow (\deg_{1} (R) (a) < 0 \to a \in I))$
38	37	ralbidv	$⊢ c = 0 \to (\forall a \in J (\deg_{1} (R) (a) < c \to a \in I) \leftrightarrow \forall a \in J (\deg_{1} (R) (a) < 0 \to a \in I))$
39	38	imbi2d	$⊢ c = 0 \to ((φ \to \forall a \in J (\deg_{1} (R) (a) < c \to a \in I)) \leftrightarrow (φ \to \forall a \in J (\deg_{1} (R) (a) < 0 \to a \in I)))$
40		breq2	$⊢ c = b \to (\deg_{1} (R) (a) < c \leftrightarrow \deg_{1} (R) (a) < b)$
41	40	imbi1d	$⊢ c = b \to ((\deg_{1} (R) (a) < c \to a \in I) \leftrightarrow (\deg_{1} (R) (a) < b \to a \in I))$
42	41	ralbidv	$⊢ c = b \to (\forall a \in J (\deg_{1} (R) (a) < c \to a \in I) \leftrightarrow \forall a \in J (\deg_{1} (R) (a) < b \to a \in I))$
43	42	imbi2d	$⊢ c = b \to ((φ \to \forall a \in J (\deg_{1} (R) (a) < c \to a \in I)) \leftrightarrow (φ \to \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)))$
44		breq2	$⊢ c = b + 1 \to (\deg_{1} (R) (a) < c \leftrightarrow \deg_{1} (R) (a) < b + 1)$
45	44	imbi1d	$⊢ c = b + 1 \to ((\deg_{1} (R) (a) < c \to a \in I) \leftrightarrow (\deg_{1} (R) (a) < b + 1 \to a \in I))$
46	45	ralbidv	$⊢ c = b + 1 \to (\forall a \in J (\deg_{1} (R) (a) < c \to a \in I) \leftrightarrow \forall a \in J (\deg_{1} (R) (a) < b + 1 \to a \in I))$
47		fveq2	$⊢ a = d \to \deg_{1} (R) (a) = \deg_{1} (R) (d)$
48	47	breq1d	$⊢ a = d \to (\deg_{1} (R) (a) < b + 1 \leftrightarrow \deg_{1} (R) (d) < b + 1)$
49		eleq1	$⊢ a = d \to (a \in I \leftrightarrow d \in I)$
50	48 49	imbi12d	$⊢ a = d \to ((\deg_{1} (R) (a) < b + 1 \to a \in I) \leftrightarrow (\deg_{1} (R) (d) < b + 1 \to d \in I))$
51	50	cbvralvw	$⊢ \forall a \in J (\deg_{1} (R) (a) < b + 1 \to a \in I) \leftrightarrow \forall d \in J (\deg_{1} (R) (d) < b + 1 \to d \in I)$
52	46 51	bitrdi	$⊢ c = b + 1 \to (\forall a \in J (\deg_{1} (R) (a) < c \to a \in I) \leftrightarrow \forall d \in J (\deg_{1} (R) (d) < b + 1 \to d \in I))$
53	52	imbi2d	$⊢ c = b + 1 \to ((φ \to \forall a \in J (\deg_{1} (R) (a) < c \to a \in I)) \leftrightarrow (φ \to \forall d \in J (\deg_{1} (R) (d) < b + 1 \to d \in I)))$
54	4	adantr	$⊢ (φ \land a \in J) \to R \in Ring$
55		eqid	$⊢ 0_{P} = 0_{P}$
56	13 1 55 9	deg1lt0	$⊢ (R \in Ring \land a \in {Base}_{P}) \to (\deg_{1} (R) (a) < 0 \leftrightarrow a = 0_{P})$
57	54 12 56	syl2anc	$⊢ (φ \land a \in J) \to (\deg_{1} (R) (a) < 0 \leftrightarrow a = 0_{P})$
58	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
59	4 58	syl	$⊢ φ \to P \in Ring$
60	2 55	lidl0cl	$⊢ (P \in Ring \land I \in U) \to 0_{P} \in I$
61	59 5 60	syl2anc	$⊢ φ \to 0_{P} \in I$
62		eleq1a	$⊢ 0_{P} \in I \to (a = 0_{P} \to a \in I)$
63	61 62	syl	$⊢ φ \to (a = 0_{P} \to a \in I)$
64	63	adantr	$⊢ (φ \land a \in J) \to (a = 0_{P} \to a \in I)$
65	57 64	sylbid	$⊢ (φ \land a \in J) \to (\deg_{1} (R) (a) < 0 \to a \in I)$
66	65	ralrimiva	$⊢ φ \to \forall a \in J (\deg_{1} (R) (a) < 0 \to a \in I)$
67	11	3ad2ant2	$⊢ (b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \to J \subseteq {Base}_{P}$
68	67	sselda	$⊢ ((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land d \in J) \to d \in {Base}_{P}$
69	13 1 9	deg1cl	$⊢ d \in {Base}_{P} \to \deg_{1} (R) (d) \in (ℕ_{0} \cup \{−∞\})$
70	68 69	syl	$⊢ ((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land d \in J) \to \deg_{1} (R) (d) \in (ℕ_{0} \cup \{−∞\})$
71		simpl1	$⊢ ((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land d \in J) \to b \in ℕ_{0}$
72	71	nn0zd	$⊢ ((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land d \in J) \to b \in ℤ$
73		degltp1le	$⊢ (\deg_{1} (R) (d) \in (ℕ_{0} \cup \{−∞\}) \land b \in ℤ) \to (\deg_{1} (R) (d) < b + 1 \leftrightarrow \deg_{1} (R) (d) \leq b)$
74	70 72 73	syl2anc	$⊢ ((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land d \in J) \to (\deg_{1} (R) (d) < b + 1 \leftrightarrow \deg_{1} (R) (d) \leq b)$
75		fveq2	$⊢ x = b \to S (J) (x) = S (J) (b)$
76		fveq2	$⊢ x = b \to S (I) (x) = S (I) (b)$
77	75 76	sseq12d	$⊢ x = b \to (S (J) (x) \subseteq S (I) (x) \leftrightarrow S (J) (b) \subseteq S (I) (b))$
78	77	rspcva	$⊢ (b \in ℕ_{0} \land \forall x \in ℕ_{0} S (J) (x) \subseteq S (I) (x)) \to S (J) (b) \subseteq S (I) (b)$
79	8 78	sylan2	$⊢ (b \in ℕ_{0} \land φ) \to S (J) (b) \subseteq S (I) (b)$
80	4	adantl	$⊢ (b \in ℕ_{0} \land φ) \to R \in Ring$
81	6	adantl	$⊢ (b \in ℕ_{0} \land φ) \to J \in U$
82		simpl	$⊢ (b \in ℕ_{0} \land φ) \to b \in ℕ_{0}$
83	1 2 3 13	hbtlem1	$⊢ (R \in Ring \land J \in U \land b \in ℕ_{0}) \to S (J) (b) = \{c \| \exists e \in J (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\}$
84	80 81 82 83	syl3anc	$⊢ (b \in ℕ_{0} \land φ) \to S (J) (b) = \{c \| \exists e \in J (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\}$
85	5	adantl	$⊢ (b \in ℕ_{0} \land φ) \to I \in U$
86	1 2 3 13	hbtlem1	$⊢ (R \in Ring \land I \in U \land b \in ℕ_{0}) \to S (I) (b) = \{c \| \exists e \in I (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\}$
87	80 85 82 86	syl3anc	$⊢ (b \in ℕ_{0} \land φ) \to S (I) (b) = \{c \| \exists e \in I (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\}$
88	79 84 87	3sstr3d	$⊢ (b \in ℕ_{0} \land φ) \to \{c \| \exists e \in J (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\} \subseteq \{c \| \exists e \in I (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\}$
89	88	3adant3	$⊢ (b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \to \{c \| \exists e \in J (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\} \subseteq \{c \| \exists e \in I (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\}$
90	89	adantr	$⊢ ((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \to \{c \| \exists e \in J (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\} \subseteq \{c \| \exists e \in I (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\}$
91		simpl	$⊢ (d \in J \land \deg_{1} (R) (d) \leq b) \to d \in J$
92		simpr	$⊢ (d \in J \land \deg_{1} (R) (d) \leq b) \to \deg_{1} (R) (d) \leq b$
93		eqidd	$⊢ (d \in J \land \deg_{1} (R) (d) \leq b) \to {coe}_{1} (d) (b) = {coe}_{1} (d) (b)$
94		fveq2	$⊢ e = d \to \deg_{1} (R) (e) = \deg_{1} (R) (d)$
95	94	breq1d	$⊢ e = d \to (\deg_{1} (R) (e) \leq b \leftrightarrow \deg_{1} (R) (d) \leq b)$
96		fveq2	$⊢ e = d \to {coe}_{1} (e) = {coe}_{1} (d)$
97	96	fveq1d	$⊢ e = d \to {coe}_{1} (e) (b) = {coe}_{1} (d) (b)$
98	97	eqeq2d	$⊢ e = d \to ({coe}_{1} (d) (b) = {coe}_{1} (e) (b) \leftrightarrow {coe}_{1} (d) (b) = {coe}_{1} (d) (b))$
99	95 98	anbi12d	$⊢ e = d \to ((\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)) \leftrightarrow (\deg_{1} (R) (d) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (d) (b)))$
100	99	rspcev	$⊢ (d \in J \land (\deg_{1} (R) (d) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (d) (b))) \to \exists e \in J (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b))$
101	91 92 93 100	syl12anc	$⊢ (d \in J \land \deg_{1} (R) (d) \leq b) \to \exists e \in J (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b))$
102		fvex	$⊢ {coe}_{1} (d) (b) \in V$
103		eqeq1	$⊢ c = {coe}_{1} (d) (b) \to (c = {coe}_{1} (e) (b) \leftrightarrow {coe}_{1} (d) (b) = {coe}_{1} (e) (b))$
104	103	anbi2d	$⊢ c = {coe}_{1} (d) (b) \to ((\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b)) \leftrightarrow (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))$
105	104	rexbidv	$⊢ c = {coe}_{1} (d) (b) \to (\exists e \in J (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b)) \leftrightarrow \exists e \in J (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))$
106	102 105	elab	$⊢ {coe}_{1} (d) (b) \in \{c \| \exists e \in J (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\} \leftrightarrow \exists e \in J (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b))$
107	101 106	sylibr	$⊢ (d \in J \land \deg_{1} (R) (d) \leq b) \to {coe}_{1} (d) (b) \in \{c \| \exists e \in J (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\}$
108	107	adantl	$⊢ ((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \to {coe}_{1} (d) (b) \in \{c \| \exists e \in J (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\}$
109	90 108	sseldd	$⊢ ((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \to {coe}_{1} (d) (b) \in \{c \| \exists e \in I (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\}$
110	104	rexbidv	$⊢ c = {coe}_{1} (d) (b) \to (\exists e \in I (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b)) \leftrightarrow \exists e \in I (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))$
111	102 110	elab	$⊢ {coe}_{1} (d) (b) \in \{c \| \exists e \in I (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\} \leftrightarrow \exists e \in I (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b))$
112		simpll2	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to φ$
113	112 59	syl	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to P \in Ring$
114		ringgrp	$⊢ P \in Ring \to P \in Grp$
115	113 114	syl	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to P \in Grp$
116	112 11	syl	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to J \subseteq {Base}_{P}$
117		simplrl	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to d \in J$
118	116 117	sseldd	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to d \in {Base}_{P}$
119	9 2	lidlss	$⊢ I \in U \to I \subseteq {Base}_{P}$
120	5 119	syl	$⊢ φ \to I \subseteq {Base}_{P}$
121	112 120	syl	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to I \subseteq {Base}_{P}$
122		simprl	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to e \in I$
123	121 122	sseldd	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to e \in {Base}_{P}$
124		eqid	$⊢ +_{P} = +_{P}$
125		eqid	$⊢ -_{P} = -_{P}$
126	9 124 125	grpnpcan	$⊢ (P \in Grp \land d \in {Base}_{P} \land e \in {Base}_{P}) \to (d -_{P} e) +_{P} e = d$
127	115 118 123 126	syl3anc	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to (d -_{P} e) +_{P} e = d$
128	5	3ad2ant2	$⊢ (b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \to I \in U$
129	128	ad2antrr	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to I \in U$
130		simpll1	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to b \in ℕ_{0}$
131	112 4	syl	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to R \in Ring$
132		simplrr	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to \deg_{1} (R) (d) \leq b$
133		simprrl	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to \deg_{1} (R) (e) \leq b$
134		eqid	$⊢ {coe}_{1} (d) = {coe}_{1} (d)$
135		eqid	$⊢ {coe}_{1} (e) = {coe}_{1} (e)$
136		simprrr	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to {coe}_{1} (d) (b) = {coe}_{1} (e) (b)$
137	13 1 9 125 130 131 118 132 123 133 134 135 136	deg1sublt	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to \deg_{1} (R) (d -_{P} e) < b$
138	112 6	syl	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to J \in U$
139	7	3ad2ant2	$⊢ (b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \to I \subseteq J$
140	139	ad2antrr	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to I \subseteq J$
141	140 122	sseldd	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to e \in J$
142	2 125	lidlsubcl	$⊢ ((P \in Ring \land J \in U) \land (d \in J \land e \in J)) \to d -_{P} e \in J$
143	113 138 117 141 142	syl22anc	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to d -_{P} e \in J$
144		simpll3	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)$
145		fveq2	$⊢ a = d -_{P} e \to \deg_{1} (R) (a) = \deg_{1} (R) (d -_{P} e)$
146	145	breq1d	$⊢ a = d -_{P} e \to (\deg_{1} (R) (a) < b \leftrightarrow \deg_{1} (R) (d -_{P} e) < b)$
147		eleq1	$⊢ a = d -_{P} e \to (a \in I \leftrightarrow d -_{P} e \in I)$
148	146 147	imbi12d	$⊢ a = d -_{P} e \to ((\deg_{1} (R) (a) < b \to a \in I) \leftrightarrow (\deg_{1} (R) (d -_{P} e) < b \to d -_{P} e \in I))$
149	148	rspcva	$⊢ (d -_{P} e \in J \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \to (\deg_{1} (R) (d -_{P} e) < b \to d -_{P} e \in I)$
150	143 144 149	syl2anc	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to (\deg_{1} (R) (d -_{P} e) < b \to d -_{P} e \in I)$
151	137 150	mpd	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to d -_{P} e \in I$
152	2 124	lidlacl	$⊢ ((P \in Ring \land I \in U) \land (d -_{P} e \in I \land e \in I)) \to (d -_{P} e) +_{P} e \in I$
153	113 129 151 122 152	syl22anc	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to (d -_{P} e) +_{P} e \in I$
154	127 153	eqeltrrd	$⊢ (((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \land (e \in I \land (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)))) \to d \in I$
155	154	rexlimdvaa	$⊢ ((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \to (\exists e \in I (\deg_{1} (R) (e) \leq b \land {coe}_{1} (d) (b) = {coe}_{1} (e) (b)) \to d \in I)$
156	111 155	biimtrid	$⊢ ((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \to ({coe}_{1} (d) (b) \in \{c \| \exists e \in I (\deg_{1} (R) (e) \leq b \land c = {coe}_{1} (e) (b))\} \to d \in I)$
157	109 156	mpd	$⊢ ((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land (d \in J \land \deg_{1} (R) (d) \leq b)) \to d \in I$
158	157	expr	$⊢ ((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land d \in J) \to (\deg_{1} (R) (d) \leq b \to d \in I)$
159	74 158	sylbid	$⊢ ((b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \land d \in J) \to (\deg_{1} (R) (d) < b + 1 \to d \in I)$
160	159	ralrimiva	$⊢ (b \in ℕ_{0} \land φ \land \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \to \forall d \in J (\deg_{1} (R) (d) < b + 1 \to d \in I)$
161	160	3exp	$⊢ b \in ℕ_{0} \to (φ \to (\forall a \in J (\deg_{1} (R) (a) < b \to a \in I) \to \forall d \in J (\deg_{1} (R) (d) < b + 1 \to d \in I)))$
162	161	a2d	$⊢ b \in ℕ_{0} \to ((φ \to \forall a \in J (\deg_{1} (R) (a) < b \to a \in I)) \to (φ \to \forall d \in J (\deg_{1} (R) (d) < b + 1 \to d \in I)))$
163	39 43 53 43 66 162	nn0ind	$⊢ b \in ℕ_{0} \to (φ \to \forall a \in J (\deg_{1} (R) (a) < b \to a \in I))$
164		rsp	$⊢ \forall a \in J (\deg_{1} (R) (a) < b \to a \in I) \to (a \in J \to (\deg_{1} (R) (a) < b \to a \in I))$
165	163 164	syl6com	$⊢ φ \to (b \in ℕ_{0} \to (a \in J \to (\deg_{1} (R) (a) < b \to a \in I)))$
166	165	com23	$⊢ φ \to (a \in J \to (b \in ℕ_{0} \to (\deg_{1} (R) (a) < b \to a \in I)))$
167	166	imp	$⊢ (φ \land a \in J) \to (b \in ℕ_{0} \to (\deg_{1} (R) (a) < b \to a \in I))$
168	167	rexlimdv	$⊢ (φ \land a \in J) \to (\exists b \in ℕ_{0} \deg_{1} (R) (a) < b \to a \in I)$
169	35 168	mpd	$⊢ (φ \land a \in J) \to a \in I$
170	7 169	eqelssd	$⊢ φ \to I = J$

Metamath Proof Explorer

Theorem hbtlem5

Proof