hbtlem2

Description: Leading coefficient ideals are ideals. (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)$
	hbtlem2.t	$⊢ T = LIdeal (R)$
Assertion	hbtlem2	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to S (I) (X) \in T$

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		hbtlem2.t	$⊢ T = LIdeal (R)$
5		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
6	1 2 3 5	hbtlem1	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to S (I) (X) = \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\}$
7		eqid	$⊢ {Base}_{P} = {Base}_{P}$
8	7 2	lidlss	$⊢ I \in U \to I \subseteq {Base}_{P}$
9	8	3ad2ant2	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to I \subseteq {Base}_{P}$
10	9	sselda	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land b \in I) \to b \in {Base}_{P}$
11		eqid	$⊢ {coe}_{1} (b) = {coe}_{1} (b)$
12		eqid	$⊢ {Base}_{R} = {Base}_{R}$
13	11 7 1 12	coe1f	$⊢ b \in {Base}_{P} \to {coe}_{1} (b) : ℕ_{0} ⟶ {Base}_{R}$
14	10 13	syl	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land b \in I) \to {coe}_{1} (b) : ℕ_{0} ⟶ {Base}_{R}$
15		simpl3	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land b \in I) \to X \in ℕ_{0}$
16	14 15	ffvelrnd	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land b \in I) \to {coe}_{1} (b) (X) \in {Base}_{R}$
17		eleq1a	$⊢ {coe}_{1} (b) (X) \in {Base}_{R} \to (a = {coe}_{1} (b) (X) \to a \in {Base}_{R})$
18	16 17	syl	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land b \in I) \to (a = {coe}_{1} (b) (X) \to a \in {Base}_{R})$
19	18	adantld	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land b \in I) \to ((\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)) \to a \in {Base}_{R})$
20	19	rexlimdva	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to (\exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)) \to a \in {Base}_{R})$
21	20	abssdv	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \subseteq {Base}_{R}$
22	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
23	22	3ad2ant1	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to P \in Ring$
24		simp2	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to I \in U$
25		eqid	$⊢ 0_{P} = 0_{P}$
26	2 25	lidl0cl	$⊢ (P \in Ring \land I \in U) \to 0_{P} \in I$
27	23 24 26	syl2anc	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to 0_{P} \in I$
28	5 1 25	deg1z	$⊢ R \in Ring \to \deg_{1} (R) (0_{P}) = −∞$
29	28	3ad2ant1	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to \deg_{1} (R) (0_{P}) = −∞$
30		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
31		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
32	30 31	sstri	$⊢ ℕ_{0} \subseteq ℝ^{*}$
33		simp3	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to X \in ℕ_{0}$
34	32 33	sselid	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to X \in ℝ^{*}$
35		mnfle	$⊢ X \in ℝ^{*} \to −∞ \leq X$
36	34 35	syl	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to −∞ \leq X$
37	29 36	eqbrtrd	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to \deg_{1} (R) (0_{P}) \leq X$
38		eqid	$⊢ 0_{R} = 0_{R}$
39	1 25 38	coe1z	$⊢ R \in Ring \to {coe}_{1} (0_{P}) = ℕ_{0} \times \{0_{R}\}$
40	39	3ad2ant1	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to {coe}_{1} (0_{P}) = ℕ_{0} \times \{0_{R}\}$
41	40	fveq1d	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to {coe}_{1} (0_{P}) (X) = (ℕ_{0} \times \{0_{R}\}) (X)$
42		fvex	$⊢ 0_{R} \in V$
43	42	fvconst2	$⊢ X \in ℕ_{0} \to (ℕ_{0} \times \{0_{R}\}) (X) = 0_{R}$
44	43	3ad2ant3	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to (ℕ_{0} \times \{0_{R}\}) (X) = 0_{R}$
45	41 44	eqtr2d	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to 0_{R} = {coe}_{1} (0_{P}) (X)$
46		fveq2	$⊢ b = 0_{P} \to \deg_{1} (R) (b) = \deg_{1} (R) (0_{P})$
47	46	breq1d	$⊢ b = 0_{P} \to (\deg_{1} (R) (b) \leq X \leftrightarrow \deg_{1} (R) (0_{P}) \leq X)$
48		fveq2	$⊢ b = 0_{P} \to {coe}_{1} (b) = {coe}_{1} (0_{P})$
49	48	fveq1d	$⊢ b = 0_{P} \to {coe}_{1} (b) (X) = {coe}_{1} (0_{P}) (X)$
50	49	eqeq2d	$⊢ b = 0_{P} \to (0_{R} = {coe}_{1} (b) (X) \leftrightarrow 0_{R} = {coe}_{1} (0_{P}) (X))$
51	47 50	anbi12d	$⊢ b = 0_{P} \to ((\deg_{1} (R) (b) \leq X \land 0_{R} = {coe}_{1} (b) (X)) \leftrightarrow (\deg_{1} (R) (0_{P}) \leq X \land 0_{R} = {coe}_{1} (0_{P}) (X)))$
52	51	rspcev	$⊢ (0_{P} \in I \land (\deg_{1} (R) (0_{P}) \leq X \land 0_{R} = {coe}_{1} (0_{P}) (X))) \to \exists b \in I (\deg_{1} (R) (b) \leq X \land 0_{R} = {coe}_{1} (b) (X))$
53	27 37 45 52	syl12anc	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to \exists b \in I (\deg_{1} (R) (b) \leq X \land 0_{R} = {coe}_{1} (b) (X))$
54		eqeq1	$⊢ a = 0_{R} \to (a = {coe}_{1} (b) (X) \leftrightarrow 0_{R} = {coe}_{1} (b) (X))$
55	54	anbi2d	$⊢ a = 0_{R} \to ((\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)) \leftrightarrow (\deg_{1} (R) (b) \leq X \land 0_{R} = {coe}_{1} (b) (X)))$
56	55	rexbidv	$⊢ a = 0_{R} \to (\exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)) \leftrightarrow \exists b \in I (\deg_{1} (R) (b) \leq X \land 0_{R} = {coe}_{1} (b) (X)))$
57	42 56	elab	$⊢ 0_{R} \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \leftrightarrow \exists b \in I (\deg_{1} (R) (b) \leq X \land 0_{R} = {coe}_{1} (b) (X))$
58	53 57	sylibr	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to 0_{R} \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\}$
59	58	ne0d	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \neq \emptyset$
60	23	adantr	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to P \in Ring$
61		simpl2	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to I \in U$
62		eqid	$⊢ algSc (P) = algSc (P)$
63	1 62 12 7	ply1sclf	$⊢ R \in Ring \to algSc (P) : {Base}_{R} ⟶ {Base}_{P}$
64	63	3ad2ant1	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to algSc (P) : {Base}_{R} ⟶ {Base}_{P}$
65	64	adantr	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to algSc (P) : {Base}_{R} ⟶ {Base}_{P}$
66		simprl	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to c \in {Base}_{R}$
67	65 66	ffvelrnd	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to algSc (P) (c) \in {Base}_{P}$
68		simprll	$⊢ (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X))) \to f \in I$
69	68	adantl	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to f \in I$
70		eqid	$⊢ \cdot_{P} = \cdot_{P}$
71	2 7 70	lidlmcl	$⊢ ((P \in Ring \land I \in U) \land (algSc (P) (c) \in {Base}_{P} \land f \in I)) \to algSc (P) (c) \cdot_{P} f \in I$
72	60 61 67 69 71	syl22anc	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to algSc (P) (c) \cdot_{P} f \in I$
73		simprrl	$⊢ (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X))) \to g \in I$
74	73	adantl	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to g \in I$
75		eqid	$⊢ +_{P} = +_{P}$
76	2 75	lidlacl	$⊢ ((P \in Ring \land I \in U) \land (algSc (P) (c) \cdot_{P} f \in I \land g \in I)) \to (algSc (P) (c) \cdot_{P} f) +_{P} g \in I$
77	60 61 72 74 76	syl22anc	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to (algSc (P) (c) \cdot_{P} f) +_{P} g \in I$
78		simpl1	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to R \in Ring$
79	9	adantr	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to I \subseteq {Base}_{P}$
80	79 69	sseldd	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to f \in {Base}_{P}$
81	7 70	ringcl	$⊢ (P \in Ring \land algSc (P) (c) \in {Base}_{P} \land f \in {Base}_{P}) \to algSc (P) (c) \cdot_{P} f \in {Base}_{P}$
82	60 67 80 81	syl3anc	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to algSc (P) (c) \cdot_{P} f \in {Base}_{P}$
83	79 74	sseldd	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to g \in {Base}_{P}$
84		simpl3	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to X \in ℕ_{0}$
85	32 84	sselid	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to X \in ℝ^{*}$
86	5 1 7	deg1xrcl	$⊢ algSc (P) (c) \cdot_{P} f \in {Base}_{P} \to \deg_{1} (R) (algSc (P) (c) \cdot_{P} f) \in ℝ^{*}$
87	82 86	syl	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to \deg_{1} (R) (algSc (P) (c) \cdot_{P} f) \in ℝ^{*}$
88	5 1 7	deg1xrcl	$⊢ f \in {Base}_{P} \to \deg_{1} (R) (f) \in ℝ^{*}$
89	80 88	syl	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to \deg_{1} (R) (f) \in ℝ^{*}$
90	5 1 12 7 70 62	deg1mul3le	$⊢ (R \in Ring \land c \in {Base}_{R} \land f \in {Base}_{P}) \to \deg_{1} (R) (algSc (P) (c) \cdot_{P} f) \leq \deg_{1} (R) (f)$
91	78 66 80 90	syl3anc	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to \deg_{1} (R) (algSc (P) (c) \cdot_{P} f) \leq \deg_{1} (R) (f)$
92		simprlr	$⊢ (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X))) \to \deg_{1} (R) (f) \leq X$
93	92	adantl	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to \deg_{1} (R) (f) \leq X$
94	87 89 85 91 93	xrletrd	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to \deg_{1} (R) (algSc (P) (c) \cdot_{P} f) \leq X$
95		simprrr	$⊢ (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X))) \to \deg_{1} (R) (g) \leq X$
96	95	adantl	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to \deg_{1} (R) (g) \leq X$
97	1 5 78 7 75 82 83 85 94 96	deg1addle2	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to \deg_{1} (R) ((algSc (P) (c) \cdot_{P} f) +_{P} g) \leq X$
98		eqid	$⊢ +_{R} = +_{R}$
99	1 7 75 98	coe1addfv	$⊢ ((R \in Ring \land algSc (P) (c) \cdot_{P} f \in {Base}_{P} \land g \in {Base}_{P}) \land X \in ℕ_{0}) \to {coe}_{1} ((algSc (P) (c) \cdot_{P} f) +_{P} g) (X) = {coe}_{1} (algSc (P) (c) \cdot_{P} f) (X) +_{R} {coe}_{1} (g) (X)$
100	78 82 83 84 99	syl31anc	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to {coe}_{1} ((algSc (P) (c) \cdot_{P} f) +_{P} g) (X) = {coe}_{1} (algSc (P) (c) \cdot_{P} f) (X) +_{R} {coe}_{1} (g) (X)$
101		eqid	$⊢ \cdot_{R} = \cdot_{R}$
102	1 7 12 62 70 101	coe1sclmulfv	$⊢ (R \in Ring \land (c \in {Base}_{R} \land f \in {Base}_{P}) \land X \in ℕ_{0}) \to {coe}_{1} (algSc (P) (c) \cdot_{P} f) (X) = c \cdot_{R} {coe}_{1} (f) (X)$
103	78 66 80 84 102	syl121anc	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to {coe}_{1} (algSc (P) (c) \cdot_{P} f) (X) = c \cdot_{R} {coe}_{1} (f) (X)$
104	103	oveq1d	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to {coe}_{1} (algSc (P) (c) \cdot_{P} f) (X) +_{R} {coe}_{1} (g) (X) = (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X)$
105	100 104	eqtr2d	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) = {coe}_{1} ((algSc (P) (c) \cdot_{P} f) +_{P} g) (X)$
106		fveq2	$⊢ b = (algSc (P) (c) \cdot_{P} f) +_{P} g \to \deg_{1} (R) (b) = \deg_{1} (R) ((algSc (P) (c) \cdot_{P} f) +_{P} g)$
107	106	breq1d	$⊢ b = (algSc (P) (c) \cdot_{P} f) +_{P} g \to (\deg_{1} (R) (b) \leq X \leftrightarrow \deg_{1} (R) ((algSc (P) (c) \cdot_{P} f) +_{P} g) \leq X)$
108		fveq2	$⊢ b = (algSc (P) (c) \cdot_{P} f) +_{P} g \to {coe}_{1} (b) = {coe}_{1} ((algSc (P) (c) \cdot_{P} f) +_{P} g)$
109	108	fveq1d	$⊢ b = (algSc (P) (c) \cdot_{P} f) +_{P} g \to {coe}_{1} (b) (X) = {coe}_{1} ((algSc (P) (c) \cdot_{P} f) +_{P} g) (X)$
110	109	eqeq2d	$⊢ b = (algSc (P) (c) \cdot_{P} f) +_{P} g \to ((c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) = {coe}_{1} (b) (X) \leftrightarrow (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) = {coe}_{1} ((algSc (P) (c) \cdot_{P} f) +_{P} g) (X))$
111	107 110	anbi12d	$⊢ b = (algSc (P) (c) \cdot_{P} f) +_{P} g \to ((\deg_{1} (R) (b) \leq X \land (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) = {coe}_{1} (b) (X)) \leftrightarrow (\deg_{1} (R) ((algSc (P) (c) \cdot_{P} f) +_{P} g) \leq X \land (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) = {coe}_{1} ((algSc (P) (c) \cdot_{P} f) +_{P} g) (X)))$
112	111	rspcev	$⊢ ((algSc (P) (c) \cdot_{P} f) +_{P} g \in I \land (\deg_{1} (R) ((algSc (P) (c) \cdot_{P} f) +_{P} g) \leq X \land (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) = {coe}_{1} ((algSc (P) (c) \cdot_{P} f) +_{P} g) (X))) \to \exists b \in I (\deg_{1} (R) (b) \leq X \land (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) = {coe}_{1} (b) (X))$
113	77 97 105 112	syl12anc	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to \exists b \in I (\deg_{1} (R) (b) \leq X \land (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) = {coe}_{1} (b) (X))$
114		ovex	$⊢ (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) \in V$
115		eqeq1	$⊢ a = (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) \to (a = {coe}_{1} (b) (X) \leftrightarrow (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) = {coe}_{1} (b) (X))$
116	115	anbi2d	$⊢ a = (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) \to ((\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)) \leftrightarrow (\deg_{1} (R) (b) \leq X \land (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) = {coe}_{1} (b) (X)))$
117	116	rexbidv	$⊢ a = (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) \to (\exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)) \leftrightarrow \exists b \in I (\deg_{1} (R) (b) \leq X \land (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) = {coe}_{1} (b) (X)))$
118	114 117	elab	$⊢ (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \leftrightarrow \exists b \in I (\deg_{1} (R) (b) \leq X \land (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) = {coe}_{1} (b) (X))$
119	113 118	sylibr	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land (c \in {Base}_{R} \land ((f \in I \land \deg_{1} (R) (f) \leq X) \land (g \in I \land \deg_{1} (R) (g) \leq X)))) \to (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\}$
120	119	exp45	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to (c \in {Base}_{R} \to ((f \in I \land \deg_{1} (R) (f) \leq X) \to ((g \in I \land \deg_{1} (R) (g) \leq X) \to (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})))$
121	120	imp	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land c \in {Base}_{R}) \to ((f \in I \land \deg_{1} (R) (f) \leq X) \to ((g \in I \land \deg_{1} (R) (g) \leq X) \to (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\}))$
122	121	exp5c	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land c \in {Base}_{R}) \to (f \in I \to (\deg_{1} (R) (f) \leq X \to (g \in I \to (\deg_{1} (R) (g) \leq X \to (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\}))))$
123	122	imp	$⊢ (((R \in Ring \land I \in U \land X \in ℕ_{0}) \land c \in {Base}_{R}) \land f \in I) \to (\deg_{1} (R) (f) \leq X \to (g \in I \to (\deg_{1} (R) (g) \leq X \to (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})))$
124	123	imp41	$⊢ ((((((R \in Ring \land I \in U \land X \in ℕ_{0}) \land c \in {Base}_{R}) \land f \in I) \land \deg_{1} (R) (f) \leq X) \land g \in I) \land \deg_{1} (R) (g) \leq X) \to (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\}$
125		oveq2	$⊢ e = {coe}_{1} (g) (X) \to (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} e = (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X)$
126	125	eleq1d	$⊢ e = {coe}_{1} (g) (X) \to ((c \cdot_{R} {coe}_{1} (f) (X)) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \leftrightarrow (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} {coe}_{1} (g) (X) \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})$
127	124 126	syl5ibrcom	$⊢ ((((((R \in Ring \land I \in U \land X \in ℕ_{0}) \land c \in {Base}_{R}) \land f \in I) \land \deg_{1} (R) (f) \leq X) \land g \in I) \land \deg_{1} (R) (g) \leq X) \to (e = {coe}_{1} (g) (X) \to (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})$
128	127	expimpd	$⊢ (((((R \in Ring \land I \in U \land X \in ℕ_{0}) \land c \in {Base}_{R}) \land f \in I) \land \deg_{1} (R) (f) \leq X) \land g \in I) \to ((\deg_{1} (R) (g) \leq X \land e = {coe}_{1} (g) (X)) \to (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})$
129	128	rexlimdva	$⊢ ((((R \in Ring \land I \in U \land X \in ℕ_{0}) \land c \in {Base}_{R}) \land f \in I) \land \deg_{1} (R) (f) \leq X) \to (\exists g \in I (\deg_{1} (R) (g) \leq X \land e = {coe}_{1} (g) (X)) \to (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})$
130	129	alrimiv	$⊢ ((((R \in Ring \land I \in U \land X \in ℕ_{0}) \land c \in {Base}_{R}) \land f \in I) \land \deg_{1} (R) (f) \leq X) \to \forall e (\exists g \in I (\deg_{1} (R) (g) \leq X \land e = {coe}_{1} (g) (X)) \to (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})$
131		eqeq1	$⊢ a = e \to (a = {coe}_{1} (b) (X) \leftrightarrow e = {coe}_{1} (b) (X))$
132	131	anbi2d	$⊢ a = e \to ((\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)) \leftrightarrow (\deg_{1} (R) (b) \leq X \land e = {coe}_{1} (b) (X)))$
133	132	rexbidv	$⊢ a = e \to (\exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)) \leftrightarrow \exists b \in I (\deg_{1} (R) (b) \leq X \land e = {coe}_{1} (b) (X)))$
134		fveq2	$⊢ b = g \to \deg_{1} (R) (b) = \deg_{1} (R) (g)$
135	134	breq1d	$⊢ b = g \to (\deg_{1} (R) (b) \leq X \leftrightarrow \deg_{1} (R) (g) \leq X)$
136		fveq2	$⊢ b = g \to {coe}_{1} (b) = {coe}_{1} (g)$
137	136	fveq1d	$⊢ b = g \to {coe}_{1} (b) (X) = {coe}_{1} (g) (X)$
138	137	eqeq2d	$⊢ b = g \to (e = {coe}_{1} (b) (X) \leftrightarrow e = {coe}_{1} (g) (X))$
139	135 138	anbi12d	$⊢ b = g \to ((\deg_{1} (R) (b) \leq X \land e = {coe}_{1} (b) (X)) \leftrightarrow (\deg_{1} (R) (g) \leq X \land e = {coe}_{1} (g) (X)))$
140	139	cbvrexvw	$⊢ \exists b \in I (\deg_{1} (R) (b) \leq X \land e = {coe}_{1} (b) (X)) \leftrightarrow \exists g \in I (\deg_{1} (R) (g) \leq X \land e = {coe}_{1} (g) (X))$
141	133 140	bitrdi	$⊢ a = e \to (\exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)) \leftrightarrow \exists g \in I (\deg_{1} (R) (g) \leq X \land e = {coe}_{1} (g) (X)))$
142	141	ralab	$⊢ \forall e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \leftrightarrow \forall e (\exists g \in I (\deg_{1} (R) (g) \leq X \land e = {coe}_{1} (g) (X)) \to (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})$
143	130 142	sylibr	$⊢ ((((R \in Ring \land I \in U \land X \in ℕ_{0}) \land c \in {Base}_{R}) \land f \in I) \land \deg_{1} (R) (f) \leq X) \to \forall e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\}$
144		oveq2	$⊢ d = {coe}_{1} (f) (X) \to c \cdot_{R} d = c \cdot_{R} {coe}_{1} (f) (X)$
145	144	oveq1d	$⊢ d = {coe}_{1} (f) (X) \to (c \cdot_{R} d) +_{R} e = (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} e$
146	145	eleq1d	$⊢ d = {coe}_{1} (f) (X) \to ((c \cdot_{R} d) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \leftrightarrow (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})$
147	146	ralbidv	$⊢ d = {coe}_{1} (f) (X) \to (\forall e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} (c \cdot_{R} d) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \leftrightarrow \forall e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} (c \cdot_{R} {coe}_{1} (f) (X)) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})$
148	143 147	syl5ibrcom	$⊢ ((((R \in Ring \land I \in U \land X \in ℕ_{0}) \land c \in {Base}_{R}) \land f \in I) \land \deg_{1} (R) (f) \leq X) \to (d = {coe}_{1} (f) (X) \to \forall e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} (c \cdot_{R} d) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})$
149	148	expimpd	$⊢ (((R \in Ring \land I \in U \land X \in ℕ_{0}) \land c \in {Base}_{R}) \land f \in I) \to ((\deg_{1} (R) (f) \leq X \land d = {coe}_{1} (f) (X)) \to \forall e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} (c \cdot_{R} d) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})$
150	149	rexlimdva	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land c \in {Base}_{R}) \to (\exists f \in I (\deg_{1} (R) (f) \leq X \land d = {coe}_{1} (f) (X)) \to \forall e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} (c \cdot_{R} d) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})$
151	150	alrimiv	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land c \in {Base}_{R}) \to \forall d (\exists f \in I (\deg_{1} (R) (f) \leq X \land d = {coe}_{1} (f) (X)) \to \forall e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} (c \cdot_{R} d) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})$
152		eqeq1	$⊢ a = d \to (a = {coe}_{1} (b) (X) \leftrightarrow d = {coe}_{1} (b) (X))$
153	152	anbi2d	$⊢ a = d \to ((\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)) \leftrightarrow (\deg_{1} (R) (b) \leq X \land d = {coe}_{1} (b) (X)))$
154	153	rexbidv	$⊢ a = d \to (\exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)) \leftrightarrow \exists b \in I (\deg_{1} (R) (b) \leq X \land d = {coe}_{1} (b) (X)))$
155		fveq2	$⊢ b = f \to \deg_{1} (R) (b) = \deg_{1} (R) (f)$
156	155	breq1d	$⊢ b = f \to (\deg_{1} (R) (b) \leq X \leftrightarrow \deg_{1} (R) (f) \leq X)$
157		fveq2	$⊢ b = f \to {coe}_{1} (b) = {coe}_{1} (f)$
158	157	fveq1d	$⊢ b = f \to {coe}_{1} (b) (X) = {coe}_{1} (f) (X)$
159	158	eqeq2d	$⊢ b = f \to (d = {coe}_{1} (b) (X) \leftrightarrow d = {coe}_{1} (f) (X))$
160	156 159	anbi12d	$⊢ b = f \to ((\deg_{1} (R) (b) \leq X \land d = {coe}_{1} (b) (X)) \leftrightarrow (\deg_{1} (R) (f) \leq X \land d = {coe}_{1} (f) (X)))$
161	160	cbvrexvw	$⊢ \exists b \in I (\deg_{1} (R) (b) \leq X \land d = {coe}_{1} (b) (X)) \leftrightarrow \exists f \in I (\deg_{1} (R) (f) \leq X \land d = {coe}_{1} (f) (X))$
162	154 161	bitrdi	$⊢ a = d \to (\exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)) \leftrightarrow \exists f \in I (\deg_{1} (R) (f) \leq X \land d = {coe}_{1} (f) (X)))$
163	162	ralab	$⊢ \forall d \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \forall e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} (c \cdot_{R} d) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \leftrightarrow \forall d (\exists f \in I (\deg_{1} (R) (f) \leq X \land d = {coe}_{1} (f) (X)) \to \forall e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} (c \cdot_{R} d) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})$
164	151 163	sylibr	$⊢ ((R \in Ring \land I \in U \land X \in ℕ_{0}) \land c \in {Base}_{R}) \to \forall d \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \forall e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} (c \cdot_{R} d) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\}$
165	164	ralrimiva	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to \forall c \in {Base}_{R} \forall d \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \forall e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} (c \cdot_{R} d) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\}$
166	4 12 98 101	islidl	$⊢ \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \in T \leftrightarrow (\{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \subseteq {Base}_{R} \land \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \neq \emptyset \land \forall c \in {Base}_{R} \forall d \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \forall e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} (c \cdot_{R} d) +_{R} e \in \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\})$
167	21 59 165 166	syl3anbrc	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \in T$
168	6 167	eqeltrd	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to S (I) (X) \in T$

Metamath Proof Explorer

Theorem hbtlem2

Proof