ig1pcl

Description: The monic generator of an ideal is always in the 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)$
	ig1pcl.u	$⊢ U = LIdeal (P)$
Assertion	ig1pcl	$⊢ (R \in DivRing \land I \in U) \to G (I) \in I$

Proof

Step	Hyp	Ref	Expression
1		ig1pval.p	$⊢ P = {Poly}_{1} (R)$
2		ig1pval.g	$⊢ G = {idlGen}_{1p} (R)$
3		ig1pcl.u	$⊢ U = LIdeal (P)$
4		fveq2	$⊢ I = \{0_{P}\} \to G (I) = G (\{0_{P}\})$
5		id	$⊢ I = \{0_{P}\} \to I = \{0_{P}\}$
6	4 5	eleq12d	$⊢ I = \{0_{P}\} \to (G (I) \in I \leftrightarrow G (\{0_{P}\}) \in \{0_{P}\})$
7		eqid	$⊢ 0_{P} = 0_{P}$
8		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
9		eqid	$⊢ {Monic}_{1p} (R) = {Monic}_{1p} (R)$
10	1 2 7 3 8 9	ig1pval3	$⊢ (R \in DivRing \land I \in U \land I \neq \{0_{P}\}) \to (G (I) \in I \land G (I) \in {Monic}_{1p} (R) \land \deg_{1} (R) (G (I)) = sup (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <))$
11	10	simp1d	$⊢ (R \in DivRing \land I \in U \land I \neq \{0_{P}\}) \to G (I) \in I$
12	11	3expa	$⊢ ((R \in DivRing \land I \in U) \land I \neq \{0_{P}\}) \to G (I) \in I$
13		drngring	$⊢ R \in DivRing \to R \in Ring$
14	1 2 7	ig1pval2	$⊢ R \in Ring \to G (\{0_{P}\}) = 0_{P}$
15	13 14	syl	$⊢ R \in DivRing \to G (\{0_{P}\}) = 0_{P}$
16		fvex	$⊢ G (\{0_{P}\}) \in V$
17	16	elsn	$⊢ G (\{0_{P}\}) \in \{0_{P}\} \leftrightarrow G (\{0_{P}\}) = 0_{P}$
18	15 17	sylibr	$⊢ R \in DivRing \to G (\{0_{P}\}) \in \{0_{P}\}$
19	18	adantr	$⊢ (R \in DivRing \land I \in U) \to G (\{0_{P}\}) \in \{0_{P}\}$
20	6 12 19	pm2.61ne	$⊢ (R \in DivRing \land I \in U) \to G (I) \in I$

Metamath Proof Explorer

Theorem ig1pcl

Proof