hbtlem7

Description: Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015)

	Ref	Expression
Hypotheses	hbtlem.p	$⊢ P = {Poly}_{1} (R)$
	hbtlem.u	$⊢ U = LIdeal (P)$
	hbtlem.s	$⊢ S = ldgIdlSeq (R)$
	hbtlem7.t	$⊢ T = LIdeal (R)$
Assertion	hbtlem7	$⊢ (R \in Ring \land I \in U) \to S (I) : ℕ_{0} ⟶ 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		hbtlem7.t	$⊢ T = LIdeal (R)$
5		simpr	$⊢ (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x)) \to y = {coe}_{1} (j) (x)$
6	5	reximi	$⊢ \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x)) \to \exists j \in I y = {coe}_{1} (j) (x)$
7	6	ss2abi	$⊢ \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\} \subseteq \{y \| \exists j \in I y = {coe}_{1} (j) (x)\}$
8		abrexexg	$⊢ I \in U \to \{y \| \exists j \in I y = {coe}_{1} (j) (x)\} \in V$
9		ssexg	$⊢ (\{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\} \subseteq \{y \| \exists j \in I y = {coe}_{1} (j) (x)\} \land \{y \| \exists j \in I y = {coe}_{1} (j) (x)\} \in V) \to \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\} \in V$
10	7 8 9	sylancr	$⊢ I \in U \to \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\} \in V$
11	10	ralrimivw	$⊢ I \in U \to \forall x \in ℕ_{0} \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\} \in V$
12	11	adantl	$⊢ (R \in Ring \land I \in U) \to \forall x \in ℕ_{0} \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\} \in V$
13		eqid	$⊢ (x \in ℕ_{0} ⟼ \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\}) = (x \in ℕ_{0} ⟼ \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\})$
14	13	fnmpt	$⊢ \forall x \in ℕ_{0} \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\} \in V \to (x \in ℕ_{0} ⟼ \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\}) Fn ℕ_{0}$
15	12 14	syl	$⊢ (R \in Ring \land I \in U) \to (x \in ℕ_{0} ⟼ \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\}) Fn ℕ_{0}$
16		elex	$⊢ R \in Ring \to R \in V$
17		fveq2	$⊢ r = R \to {Poly}_{1} (r) = {Poly}_{1} (R)$
18	17 1	eqtr4di	$⊢ r = R \to {Poly}_{1} (r) = P$
19	18	fveq2d	$⊢ r = R \to LIdeal ({Poly}_{1} (r)) = LIdeal (P)$
20	19 2	eqtr4di	$⊢ r = R \to LIdeal ({Poly}_{1} (r)) = U$
21		fveq2	$⊢ r = R \to \deg_{1} (r) = \deg_{1} (R)$
22	21	fveq1d	$⊢ r = R \to \deg_{1} (r) (j) = \deg_{1} (R) (j)$
23	22	breq1d	$⊢ r = R \to (\deg_{1} (r) (j) \leq x \leftrightarrow \deg_{1} (R) (j) \leq x)$
24	23	anbi1d	$⊢ r = R \to ((\deg_{1} (r) (j) \leq x \land y = {coe}_{1} (j) (x)) \leftrightarrow (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x)))$
25	24	rexbidv	$⊢ r = R \to (\exists j \in i (\deg_{1} (r) (j) \leq x \land y = {coe}_{1} (j) (x)) \leftrightarrow \exists j \in i (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x)))$
26	25	abbidv	$⊢ r = R \to \{y \| \exists j \in i (\deg_{1} (r) (j) \leq x \land y = {coe}_{1} (j) (x))\} = \{y \| \exists j \in i (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\}$
27	26	mpteq2dv	$⊢ r = R \to (x \in ℕ_{0} ⟼ \{y \| \exists j \in i (\deg_{1} (r) (j) \leq x \land y = {coe}_{1} (j) (x))\}) = (x \in ℕ_{0} ⟼ \{y \| \exists j \in i (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\})$
28	20 27	mpteq12dv	$⊢ r = R \to (i \in LIdeal ({Poly}_{1} (r)) ⟼ (x \in ℕ_{0} ⟼ \{y \| \exists j \in i (\deg_{1} (r) (j) \leq x \land y = {coe}_{1} (j) (x))\})) = (i \in U ⟼ (x \in ℕ_{0} ⟼ \{y \| \exists j \in i (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\}))$
29		df-ldgis	$⊢ ldgIdlSeq = (r \in V ⟼ (i \in LIdeal ({Poly}_{1} (r)) ⟼ (x \in ℕ_{0} ⟼ \{y \| \exists j \in i (\deg_{1} (r) (j) \leq x \land y = {coe}_{1} (j) (x))\})))$
30	28 29 2	mptfvmpt	$⊢ R \in V \to ldgIdlSeq (R) = (i \in U ⟼ (x \in ℕ_{0} ⟼ \{y \| \exists j \in i (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\}))$
31	16 30	syl	$⊢ R \in Ring \to ldgIdlSeq (R) = (i \in U ⟼ (x \in ℕ_{0} ⟼ \{y \| \exists j \in i (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\}))$
32	3 31	syl5eq	$⊢ R \in Ring \to S = (i \in U ⟼ (x \in ℕ_{0} ⟼ \{y \| \exists j \in i (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\}))$
33	32	fveq1d	$⊢ R \in Ring \to S (I) = (i \in U ⟼ (x \in ℕ_{0} ⟼ \{y \| \exists j \in i (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\})) (I)$
34		rexeq	$⊢ i = I \to (\exists j \in i (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x)) \leftrightarrow \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x)))$
35	34	abbidv	$⊢ i = I \to \{y \| \exists j \in i (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\} = \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\}$
36	35	mpteq2dv	$⊢ i = I \to (x \in ℕ_{0} ⟼ \{y \| \exists j \in i (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\}) = (x \in ℕ_{0} ⟼ \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\})$
37		eqid	$⊢ (i \in U ⟼ (x \in ℕ_{0} ⟼ \{y \| \exists j \in i (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\})) = (i \in U ⟼ (x \in ℕ_{0} ⟼ \{y \| \exists j \in i (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\}))$
38		nn0ex	$⊢ ℕ_{0} \in V$
39	38	mptex	$⊢ (x \in ℕ_{0} ⟼ \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\}) \in V$
40	36 37 39	fvmpt	$⊢ I \in U \to (i \in U ⟼ (x \in ℕ_{0} ⟼ \{y \| \exists j \in i (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\})) (I) = (x \in ℕ_{0} ⟼ \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\})$
41	33 40	sylan9eq	$⊢ (R \in Ring \land I \in U) \to S (I) = (x \in ℕ_{0} ⟼ \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\})$
42	41	fneq1d	$⊢ (R \in Ring \land I \in U) \to (S (I) Fn ℕ_{0} \leftrightarrow (x \in ℕ_{0} ⟼ \{y \| \exists j \in I (\deg_{1} (R) (j) \leq x \land y = {coe}_{1} (j) (x))\}) Fn ℕ_{0})$
43	15 42	mpbird	$⊢ (R \in Ring \land I \in U) \to S (I) Fn ℕ_{0}$
44	1 2 3 4	hbtlem2	$⊢ (R \in Ring \land I \in U \land x \in ℕ_{0}) \to S (I) (x) \in T$
45	44	3expa	$⊢ ((R \in Ring \land I \in U) \land x \in ℕ_{0}) \to S (I) (x) \in T$
46	45	ralrimiva	$⊢ (R \in Ring \land I \in U) \to \forall x \in ℕ_{0} S (I) (x) \in T$
47		ffnfv	$⊢ S (I) : ℕ_{0} ⟶ T \leftrightarrow (S (I) Fn ℕ_{0} \land \forall x \in ℕ_{0} S (I) (x) \in T)$
48	43 46 47	sylanbrc	$⊢ (R \in Ring \land I \in U) \to S (I) : ℕ_{0} ⟶ T$

Metamath Proof Explorer

Theorem hbtlem7

Proof