hbtlem1

Description: Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015)

	Ref	Expression
Hypotheses	hbtlem.p	$⊢ P = {Poly}_{1} (R)$
	hbtlem.u	$⊢ U = LIdeal (P)$
	hbtlem.s	$⊢ S = ldgIdlSeq (R)$
	hbtlem.d	$⊢ D = \deg_{1} (R)$
Assertion	hbtlem1	$⊢ (R \in V \land I \in U \land X \in ℕ_{0}) \to S (I) (X) = \{j \| \exists k \in I (D (k) \leq X \land j = {coe}_{1} (k) (X))\}$

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		hbtlem.d	$⊢ D = \deg_{1} (R)$
5		elex	$⊢ R \in V \to R \in V$
6		fveq2	$⊢ r = R \to {Poly}_{1} (r) = {Poly}_{1} (R)$
7	6 1	eqtr4di	$⊢ r = R \to {Poly}_{1} (r) = P$
8	7	fveq2d	$⊢ r = R \to LIdeal ({Poly}_{1} (r)) = LIdeal (P)$
9	8 2	eqtr4di	$⊢ r = R \to LIdeal ({Poly}_{1} (r)) = U$
10		fveq2	$⊢ r = R \to \deg_{1} (r) = \deg_{1} (R)$
11	10 4	eqtr4di	$⊢ r = R \to \deg_{1} (r) = D$
12	11	fveq1d	$⊢ r = R \to \deg_{1} (r) (k) = D (k)$
13	12	breq1d	$⊢ r = R \to (\deg_{1} (r) (k) \leq x \leftrightarrow D (k) \leq x)$
14	13	anbi1d	$⊢ r = R \to ((\deg_{1} (r) (k) \leq x \land j = {coe}_{1} (k) (x)) \leftrightarrow (D (k) \leq x \land j = {coe}_{1} (k) (x)))$
15	14	rexbidv	$⊢ r = R \to (\exists k \in i (\deg_{1} (r) (k) \leq x \land j = {coe}_{1} (k) (x)) \leftrightarrow \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x)))$
16	15	abbidv	$⊢ r = R \to \{j \| \exists k \in i (\deg_{1} (r) (k) \leq x \land j = {coe}_{1} (k) (x))\} = \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\}$
17	16	mpteq2dv	$⊢ r = R \to (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (\deg_{1} (r) (k) \leq x \land j = {coe}_{1} (k) (x))\}) = (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\})$
18	9 17	mpteq12dv	$⊢ r = R \to (i \in LIdeal ({Poly}_{1} (r)) ⟼ (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (\deg_{1} (r) (k) \leq x \land j = {coe}_{1} (k) (x))\})) = (i \in U ⟼ (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\}))$
19		df-ldgis	$⊢ ldgIdlSeq = (r \in V ⟼ (i \in LIdeal ({Poly}_{1} (r)) ⟼ (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (\deg_{1} (r) (k) \leq x \land j = {coe}_{1} (k) (x))\})))$
20	18 19 2	mptfvmpt	$⊢ R \in V \to ldgIdlSeq (R) = (i \in U ⟼ (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\}))$
21	5 20	syl	$⊢ R \in V \to ldgIdlSeq (R) = (i \in U ⟼ (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\}))$
22	3 21	syl5eq	$⊢ R \in V \to S = (i \in U ⟼ (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\}))$
23	22	fveq1d	$⊢ R \in V \to S (I) = (i \in U ⟼ (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\})) (I)$
24	23	fveq1d	$⊢ R \in V \to S (I) (X) = (i \in U ⟼ (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\})) (I) (X)$
25	24	3ad2ant1	$⊢ (R \in V \land I \in U \land X \in ℕ_{0}) \to S (I) (X) = (i \in U ⟼ (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\})) (I) (X)$
26		rexeq	$⊢ i = I \to (\exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x)) \leftrightarrow \exists k \in I (D (k) \leq x \land j = {coe}_{1} (k) (x)))$
27	26	abbidv	$⊢ i = I \to \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\} = \{j \| \exists k \in I (D (k) \leq x \land j = {coe}_{1} (k) (x))\}$
28	27	mpteq2dv	$⊢ i = I \to (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\}) = (x \in ℕ_{0} ⟼ \{j \| \exists k \in I (D (k) \leq x \land j = {coe}_{1} (k) (x))\})$
29		eqid	$⊢ (i \in U ⟼ (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\})) = (i \in U ⟼ (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\}))$
30		nn0ex	$⊢ ℕ_{0} \in V$
31	30	mptex	$⊢ (x \in ℕ_{0} ⟼ \{j \| \exists k \in I (D (k) \leq x \land j = {coe}_{1} (k) (x))\}) \in V$
32	28 29 31	fvmpt	$⊢ I \in U \to (i \in U ⟼ (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\})) (I) = (x \in ℕ_{0} ⟼ \{j \| \exists k \in I (D (k) \leq x \land j = {coe}_{1} (k) (x))\})$
33	32	fveq1d	$⊢ I \in U \to (i \in U ⟼ (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\})) (I) (X) = (x \in ℕ_{0} ⟼ \{j \| \exists k \in I (D (k) \leq x \land j = {coe}_{1} (k) (x))\}) (X)$
34	33	3ad2ant2	$⊢ (R \in V \land I \in U \land X \in ℕ_{0}) \to (i \in U ⟼ (x \in ℕ_{0} ⟼ \{j \| \exists k \in i (D (k) \leq x \land j = {coe}_{1} (k) (x))\})) (I) (X) = (x \in ℕ_{0} ⟼ \{j \| \exists k \in I (D (k) \leq x \land j = {coe}_{1} (k) (x))\}) (X)$
35		eqid	$⊢ (x \in ℕ_{0} ⟼ \{j \| \exists k \in I (D (k) \leq x \land j = {coe}_{1} (k) (x))\}) = (x \in ℕ_{0} ⟼ \{j \| \exists k \in I (D (k) \leq x \land j = {coe}_{1} (k) (x))\})$
36		breq2	$⊢ x = X \to (D (k) \leq x \leftrightarrow D (k) \leq X)$
37		fveq2	$⊢ x = X \to {coe}_{1} (k) (x) = {coe}_{1} (k) (X)$
38	37	eqeq2d	$⊢ x = X \to (j = {coe}_{1} (k) (x) \leftrightarrow j = {coe}_{1} (k) (X))$
39	36 38	anbi12d	$⊢ x = X \to ((D (k) \leq x \land j = {coe}_{1} (k) (x)) \leftrightarrow (D (k) \leq X \land j = {coe}_{1} (k) (X)))$
40	39	rexbidv	$⊢ x = X \to (\exists k \in I (D (k) \leq x \land j = {coe}_{1} (k) (x)) \leftrightarrow \exists k \in I (D (k) \leq X \land j = {coe}_{1} (k) (X)))$
41	40	abbidv	$⊢ x = X \to \{j \| \exists k \in I (D (k) \leq x \land j = {coe}_{1} (k) (x))\} = \{j \| \exists k \in I (D (k) \leq X \land j = {coe}_{1} (k) (X))\}$
42		simp3	$⊢ (R \in V \land I \in U \land X \in ℕ_{0}) \to X \in ℕ_{0}$
43		simpr	$⊢ (D (k) \leq X \land j = {coe}_{1} (k) (X)) \to j = {coe}_{1} (k) (X)$
44	43	reximi	$⊢ \exists k \in I (D (k) \leq X \land j = {coe}_{1} (k) (X)) \to \exists k \in I j = {coe}_{1} (k) (X)$
45	44	ss2abi	$⊢ \{j \| \exists k \in I (D (k) \leq X \land j = {coe}_{1} (k) (X))\} \subseteq \{j \| \exists k \in I j = {coe}_{1} (k) (X)\}$
46		abrexexg	$⊢ I \in U \to \{j \| \exists k \in I j = {coe}_{1} (k) (X)\} \in V$
47	46	3ad2ant2	$⊢ (R \in V \land I \in U \land X \in ℕ_{0}) \to \{j \| \exists k \in I j = {coe}_{1} (k) (X)\} \in V$
48		ssexg	$⊢ (\{j \| \exists k \in I (D (k) \leq X \land j = {coe}_{1} (k) (X))\} \subseteq \{j \| \exists k \in I j = {coe}_{1} (k) (X)\} \land \{j \| \exists k \in I j = {coe}_{1} (k) (X)\} \in V) \to \{j \| \exists k \in I (D (k) \leq X \land j = {coe}_{1} (k) (X))\} \in V$
49	45 47 48	sylancr	$⊢ (R \in V \land I \in U \land X \in ℕ_{0}) \to \{j \| \exists k \in I (D (k) \leq X \land j = {coe}_{1} (k) (X))\} \in V$
50	35 41 42 49	fvmptd3	$⊢ (R \in V \land I \in U \land X \in ℕ_{0}) \to (x \in ℕ_{0} ⟼ \{j \| \exists k \in I (D (k) \leq x \land j = {coe}_{1} (k) (x))\}) (X) = \{j \| \exists k \in I (D (k) \leq X \land j = {coe}_{1} (k) (X))\}$
51	25 34 50	3eqtrd	$⊢ (R \in V \land I \in U \land X \in ℕ_{0}) \to S (I) (X) = \{j \| \exists k \in I (D (k) \leq X \land j = {coe}_{1} (k) (X))\}$

Metamath Proof Explorer

Theorem hbtlem1

Proof