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 = {Poly}_{1} (R)$
	ig1pval.g	$⊢ G = {idlGen}_{1p} (R)$
	ig1pval2.z	$⊢ \underset{˙}{0} = 0_{P}$
Assertion	ig1pval2	$⊢ R \in Ring \to G (\{\underset{˙}{0}\}) = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		ig1pval.p	$⊢ P = {Poly}_{1} (R)$
2		ig1pval.g	$⊢ G = {idlGen}_{1p} (R)$
3		ig1pval2.z	$⊢ \underset{˙}{0} = 0_{P}$
4	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
5		eqid	$⊢ LIdeal (P) = LIdeal (P)$
6	5 3	lidl0	$⊢ P \in Ring \to \{\underset{˙}{0}\} \in LIdeal (P)$
7	4 6	syl	$⊢ R \in Ring \to \{\underset{˙}{0}\} \in LIdeal (P)$
8		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
9		eqid	$⊢ {Monic}_{1p} (R) = {Monic}_{1p} (R)$
10	1 2 3 5 8 9	ig1pval	$⊢ (R \in Ring \land \{\underset{˙}{0}\} \in LIdeal (P)) \to G (\{\underset{˙}{0}\}) = if (\{\underset{˙}{0}\} = \{\underset{˙}{0}\}, \underset{˙}{0}, (ι g \in (\{\underset{˙}{0}\} \cap {Monic}_{1p} (R)) \| \deg_{1} (R) (g) = inf (\deg_{1} (R) [\{\underset{˙}{0}\} ∖ \{\underset{˙}{0}\}] ℝ <)))$
11	7 10	mpdan	$⊢ R \in Ring \to G (\{\underset{˙}{0}\}) = if (\{\underset{˙}{0}\} = \{\underset{˙}{0}\}, \underset{˙}{0}, (ι g \in (\{\underset{˙}{0}\} \cap {Monic}_{1p} (R)) \| \deg_{1} (R) (g) = inf (\deg_{1} (R) [\{\underset{˙}{0}\} ∖ \{\underset{˙}{0}\}] ℝ <)))$
12		eqid	$⊢ \{\underset{˙}{0}\} = \{\underset{˙}{0}\}$
13	12	iftruei	$⊢ if (\{\underset{˙}{0}\} = \{\underset{˙}{0}\}, \underset{˙}{0}, (ι g \in (\{\underset{˙}{0}\} \cap {Monic}_{1p} (R)) \| \deg_{1} (R) (g) = inf (\deg_{1} (R) [\{\underset{˙}{0}\} ∖ \{\underset{˙}{0}\}] ℝ <))) = \underset{˙}{0}$
14	11 13	eqtrdi	$⊢ R \in Ring \to G (\{\underset{˙}{0}\}) = \underset{˙}{0}$

Metamath Proof Explorer