Theorem ig1pval

Description: Substitutions for the polynomial ideal generator function. (Contributed by Stefan O'Rear, 29-Mar-2015) (Revised by AV, 25-Sep-2020)

	Ref	Expression
Hypotheses	ig1pval.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ig1pval.g	$$⊢G={idlGen}_{\mathrm{1p}}\left(R\right)$$
	ig1pval.z	$$⊢\underset{\dot{}}{0}=0_P$$
	ig1pval.u	$$⊢U=\mathrm{LIdeal}\left(P\right)$$
	ig1pval.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	ig1pval.m	$$⊢M={Monic}_{\mathrm{1p}}\left(R\right)$$
Assertion	ig1pval	$$⊢\left(R\in V\wedge I\in U\right)\to G\left(I\right)=if\left(I=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(I\cap M\right)|D\left(g\right)=inf\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ig1pval.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ig1pval.g	$$⊢G={idlGen}_{\mathrm{1p}}\left(R\right)$$
3		ig1pval.z	$$⊢\underset{\dot{}}{0}=0_P$$
4		ig1pval.u	$$⊢U=\mathrm{LIdeal}\left(P\right)$$
5		ig1pval.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
6		ig1pval.m	$$⊢M={Monic}_{\mathrm{1p}}\left(R\right)$$
7		elex	$$⊢R\in V\to R\in \mathrm{V}$$
8		fveq2	$$⊢r=R\to {\mathrm{Poly}}_1\left(r\right)={\mathrm{Poly}}_1\left(R\right)$$
9	8 1	eqtr4di	$$⊢r=R\to {\mathrm{Poly}}_1\left(r\right)=P$$
10	9	fveq2d	$$⊢r=R\to \mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(r\right)\right)=\mathrm{LIdeal}\left(P\right)$$
11	10 4	eqtr4di	$$⊢r=R\to \mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(r\right)\right)=U$$
12	9	fveq2d	$$⊢r=R\to 0_{{\mathrm{Poly}}_1\left(r\right)}=0_P$$
13	12 3	eqtr4di	$$⊢r=R\to 0_{{\mathrm{Poly}}_1\left(r\right)}=\underset{\dot{}}{0}$$
14	13	sneqd	$$⊢r=R\to \left\{0_{{\mathrm{Poly}}_1\left(r\right)}\right\}=\left\{\underset{\dot{}}{0}\right\}$$
15	14	eqeq2d	$$⊢r=R\to \left(i=\left\{0_{{\mathrm{Poly}}_1\left(r\right)}\right\}\leftrightarrow i=\left\{\underset{\dot{}}{0}\right\}\right)$$
16		fveq2	$$⊢r=R\to {Monic}_{\mathrm{1p}}\left(r\right)={Monic}_{\mathrm{1p}}\left(R\right)$$
17	16 6	eqtr4di	$$⊢r=R\to {Monic}_{\mathrm{1p}}\left(r\right)=M$$
18	17	ineq2d	$$⊢r=R\to i\cap {Monic}_{\mathrm{1p}}\left(r\right)=i\cap M$$
19		fveq2	$$⊢r=R\to {\mathrm{deg}}_1\left(r\right)={\mathrm{deg}}_1\left(R\right)$$
20	19 5	eqtr4di	$$⊢r=R\to {\mathrm{deg}}_1\left(r\right)=D$$
21	20	fveq1d	$$⊢r=R\to {\mathrm{deg}}_1\left(r\right)\left(g\right)=D\left(g\right)$$
22	14	difeq2d	$$⊢r=R\to i\setminus \left\{0_{{\mathrm{Poly}}_1\left(r\right)}\right\}=i\setminus \left\{\underset{\dot{}}{0}\right\}$$
23	20 22	imaeq12d	$$⊢r=R\to {\mathrm{deg}}_1\left(r\right)\left[i\setminus \left\{0_{{\mathrm{Poly}}_1\left(r\right)}\right\}\right]=D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
24	23	infeq1d	$$⊢r=R\to inf\left({\mathrm{deg}}_1\left(r\right)\left[i\setminus \left\{0_{{\mathrm{Poly}}_1\left(r\right)}\right\}\right],ℝ,<\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)$$
25	21 24	eqeq12d	$$⊢r=R\to \left({\mathrm{deg}}_1\left(r\right)\left(g\right)=inf\left({\mathrm{deg}}_1\left(r\right)\left[i\setminus \left\{0_{{\mathrm{Poly}}_1\left(r\right)}\right\}\right],ℝ,<\right)\leftrightarrow D\left(g\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)$$
26	18 25	riotaeqbidv	$$⊢r=R\to \left(\iota g\in \left(i\cap {Monic}_{\mathrm{1p}}\left(r\right)\right)|{\mathrm{deg}}_1\left(r\right)\left(g\right)=inf\left({\mathrm{deg}}_1\left(r\right)\left[i\setminus \left\{0_{{\mathrm{Poly}}_1\left(r\right)}\right\}\right],ℝ,<\right)\right)=\left(\iota g\in \left(i\cap M\right)|D\left(g\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)$$
27	15 13 26	ifbieq12d	$$⊢r=R\to if\left(i=\left\{0_{{\mathrm{Poly}}_1\left(r\right)}\right\},0_{{\mathrm{Poly}}_1\left(r\right)},\left(\iota g\in \left(i\cap {Monic}_{\mathrm{1p}}\left(r\right)\right)|{\mathrm{deg}}_1\left(r\right)\left(g\right)=inf\left({\mathrm{deg}}_1\left(r\right)\left[i\setminus \left\{0_{{\mathrm{Poly}}_1\left(r\right)}\right\}\right],ℝ,<\right)\right)\right)=if\left(i=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(i\cap M\right)|D\left(g\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)$$
28	11 27	mpteq12dv	$$⊢r=R\to \left(i\in \mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(r\right)\right)⟼if\left(i=\left\{0_{{\mathrm{Poly}}_1\left(r\right)}\right\},0_{{\mathrm{Poly}}_1\left(r\right)},\left(\iota g\in \left(i\cap {Monic}_{\mathrm{1p}}\left(r\right)\right)|{\mathrm{deg}}_1\left(r\right)\left(g\right)=inf\left({\mathrm{deg}}_1\left(r\right)\left[i\setminus \left\{0_{{\mathrm{Poly}}_1\left(r\right)}\right\}\right],ℝ,<\right)\right)\right)\right)=\left(i\in U⟼if\left(i=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(i\cap M\right)|D\left(g\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)\right)$$
29		df-ig1p	$$⊢{idlGen}_{\mathrm{1p}}=\left(r\in \mathrm{V}⟼\left(i\in \mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(r\right)\right)⟼if\left(i=\left\{0_{{\mathrm{Poly}}_1\left(r\right)}\right\},0_{{\mathrm{Poly}}_1\left(r\right)},\left(\iota g\in \left(i\cap {Monic}_{\mathrm{1p}}\left(r\right)\right)|{\mathrm{deg}}_1\left(r\right)\left(g\right)=inf\left({\mathrm{deg}}_1\left(r\right)\left[i\setminus \left\{0_{{\mathrm{Poly}}_1\left(r\right)}\right\}\right],ℝ,<\right)\right)\right)\right)\right)$$
30	28 29 4	mptfvmpt	$$⊢R\in \mathrm{V}\to {idlGen}_{\mathrm{1p}}\left(R\right)=\left(i\in U⟼if\left(i=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(i\cap M\right)|D\left(g\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)\right)$$
31	7 30	syl	$$⊢R\in V\to {idlGen}_{\mathrm{1p}}\left(R\right)=\left(i\in U⟼if\left(i=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(i\cap M\right)|D\left(g\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)\right)$$
32	2 31	eqtrid	$$⊢R\in V\to G=\left(i\in U⟼if\left(i=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(i\cap M\right)|D\left(g\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)\right)$$
33	32	fveq1d	$$⊢R\in V\to G\left(I\right)=\left(i\in U⟼if\left(i=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(i\cap M\right)|D\left(g\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)\right)\left(I\right)$$
34		eqeq1	$$⊢i=I\to \left(i=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow I=\left\{\underset{\dot{}}{0}\right\}\right)$$
35		ineq1	$$⊢i=I\to i\cap M=I\cap M$$
36		difeq1	$$⊢i=I\to i\setminus \left\{\underset{\dot{}}{0}\right\}=I\setminus \left\{\underset{\dot{}}{0}\right\}$$
37	36	imaeq2d	$$⊢i=I\to D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right]=D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
38	37	infeq1d	$$⊢i=I\to inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)=inf\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)$$
39	38	eqeq2d	$$⊢i=I\to \left(D\left(g\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\leftrightarrow D\left(g\right)=inf\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)$$
40	35 39	riotaeqbidv	$$⊢i=I\to \left(\iota g\in \left(i\cap M\right)|D\left(g\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)=\left(\iota g\in \left(I\cap M\right)|D\left(g\right)=inf\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)$$
41	34 40	ifbieq2d	$$⊢i=I\to if\left(i=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(i\cap M\right)|D\left(g\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)=if\left(I=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(I\cap M\right)|D\left(g\right)=inf\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)$$
42		eqid	$$⊢\left(i\in U⟼if\left(i=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(i\cap M\right)|D\left(g\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)\right)=\left(i\in U⟼if\left(i=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(i\cap M\right)|D\left(g\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)\right)$$
43	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
44		riotaex	$$⊢\left(\iota g\in \left(I\cap M\right)|D\left(g\right)=inf\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\in \mathrm{V}$$
45	43 44	ifex	$$⊢if\left(I=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(I\cap M\right)|D\left(g\right)=inf\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)\in \mathrm{V}$$
46	41 42 45	fvmpt	$$⊢I\in U\to \left(i\in U⟼if\left(i=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(i\cap M\right)|D\left(g\right)=inf\left(D\left[i\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)\right)\left(I\right)=if\left(I=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(I\cap M\right)|D\left(g\right)=inf\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)$$
47	33 46	sylan9eq	$$⊢\left(R\in V\wedge I\in U\right)\to G\left(I\right)=if\left(I=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(I\cap M\right)|D\left(g\right)=inf\left(D\left[I\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)$$