ig1pval3

Description: Characterizing properties of the monic generator of a nonzero ideal of polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015) (Revised by AV, 25-Sep-2020)

	Ref	Expression
Hypotheses	ig1pval.p	$⊢ P = {Poly}_{1} (R)$
	ig1pval.g	$⊢ G = {idlGen}_{1p} (R)$
	ig1pval3.z	$⊢ \underset{˙}{0} = 0_{P}$
	ig1pval3.u	$⊢ U = LIdeal (P)$
	ig1pval3.d	$⊢ D = \deg_{1} (R)$
	ig1pval3.m	$⊢ M = {Monic}_{1p} (R)$
Assertion	ig1pval3	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to (G (I) \in I \land G (I) \in M \land D (G (I)) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$

Proof

Step	Hyp	Ref	Expression
1		ig1pval.p	$⊢ P = {Poly}_{1} (R)$
2		ig1pval.g	$⊢ G = {idlGen}_{1p} (R)$
3		ig1pval3.z	$⊢ \underset{˙}{0} = 0_{P}$
4		ig1pval3.u	$⊢ U = LIdeal (P)$
5		ig1pval3.d	$⊢ D = \deg_{1} (R)$
6		ig1pval3.m	$⊢ M = {Monic}_{1p} (R)$
7	1 2 3 4 5 6	ig1pval	$⊢ (R \in DivRing \land I \in U) \to G (I) = if (I = \{\underset{˙}{0}\}, \underset{˙}{0}, (ι g \in (I \cap M) \| D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)))$
8	7	3adant3	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to G (I) = if (I = \{\underset{˙}{0}\}, \underset{˙}{0}, (ι g \in (I \cap M) \| D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)))$
9		simp3	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to I \neq \{\underset{˙}{0}\}$
10	9	neneqd	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \neg I = \{\underset{˙}{0}\}$
11	10	iffalsed	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to if (I = \{\underset{˙}{0}\}, \underset{˙}{0}, (ι g \in (I \cap M) \| D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))) = (ι g \in (I \cap M) \| D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
12	8 11	eqtrd	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to G (I) = (ι g \in (I \cap M) \| D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
13	1 4 3 6 5	ig1peu	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \exists! g \in (I \cap M) D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)$
14		riotacl2	$⊢ \exists! g \in (I \cap M) D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \to (ι g \in (I \cap M) \| D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)) \in \{g \in (I \cap M) \| D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)\}$
15	13 14	syl	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to (ι g \in (I \cap M) \| D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)) \in \{g \in (I \cap M) \| D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)\}$
16	12 15	eqeltrd	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to G (I) \in \{g \in (I \cap M) \| D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)\}$
17		elin	$⊢ G (I) \in (I \cap M) \leftrightarrow (G (I) \in I \land G (I) \in M)$
18	17	anbi1i	$⊢ (G (I) \in (I \cap M) \land D (G (I)) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)) \leftrightarrow ((G (I) \in I \land G (I) \in M) \land D (G (I)) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
19		fveqeq2	$⊢ g = G (I) \to (D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \leftrightarrow D (G (I)) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
20	19	elrab	$⊢ G (I) \in \{g \in (I \cap M) \| D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)\} \leftrightarrow (G (I) \in (I \cap M) \land D (G (I)) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
21		df-3an	$⊢ (G (I) \in I \land G (I) \in M \land D (G (I)) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)) \leftrightarrow ((G (I) \in I \land G (I) \in M) \land D (G (I)) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
22	18 20 21	3bitr4i	$⊢ G (I) \in \{g \in (I \cap M) \| D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)\} \leftrightarrow (G (I) \in I \land G (I) \in M \land D (G (I)) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
23	16 22	sylib	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to (G (I) \in I \land G (I) \in M \land D (G (I)) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$

Metamath Proof Explorer

Theorem ig1pval3

Proof