Theorem ig1pval2

Description: Generator of the zero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015) (Proof shortened 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)$$
	ig1pval2.z	$$⊢\underset{\dot{}}{0}=0_P$$
Assertion	ig1pval2	$$⊢R\in \mathrm{Ring}\to G\left(\left\{\underset{\dot{}}{0}\right\}\right)=\underset{\dot{}}{0}$$

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		ig1pval2.z	$$⊢\underset{\dot{}}{0}=0_P$$
4	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
5		eqid	$$⊢\mathrm{LIdeal}\left(P\right)=\mathrm{LIdeal}\left(P\right)$$
6	5 3	lidl0	$$⊢P\in \mathrm{Ring}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(P\right)$$
7	4 6	syl	$$⊢R\in \mathrm{Ring}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(P\right)$$
8		eqid	$$⊢{\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(R\right)$$
9		eqid	$$⊢{Monic}_{\mathrm{1p}}\left(R\right)={Monic}_{\mathrm{1p}}\left(R\right)$$
10	1 2 3 5 8 9	ig1pval	$$⊢\left(R\in \mathrm{Ring}\wedge \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(P\right)\right)\to G\left(\left\{\underset{\dot{}}{0}\right\}\right)=if\left(\left\{\underset{\dot{}}{0}\right\}=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(\left\{\underset{\dot{}}{0}\right\}\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[\left\{\underset{\dot{}}{0}\right\}\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)$$
11	7 10	mpdan	$$⊢R\in \mathrm{Ring}\to G\left(\left\{\underset{\dot{}}{0}\right\}\right)=if\left(\left\{\underset{\dot{}}{0}\right\}=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(\left\{\underset{\dot{}}{0}\right\}\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[\left\{\underset{\dot{}}{0}\right\}\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)$$
12		eqid	$$⊢\left\{\underset{\dot{}}{0}\right\}=\left\{\underset{\dot{}}{0}\right\}$$
13	12	iftruei	$$⊢if\left(\left\{\underset{\dot{}}{0}\right\}=\left\{\underset{\dot{}}{0}\right\},\underset{\dot{}}{0},\left(\iota g\in \left(\left\{\underset{\dot{}}{0}\right\}\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[\left\{\underset{\dot{}}{0}\right\}\setminus \left\{\underset{\dot{}}{0}\right\}\right],ℝ,<\right)\right)\right)=\underset{\dot{}}{0}$$
14	11 13	eqtrdi	$$⊢R\in \mathrm{Ring}\to G\left(\left\{\underset{\dot{}}{0}\right\}\right)=\underset{\dot{}}{0}$$