ig1prsp

Description: Any ideal of polynomials over a division ring is generated by the ideal's canonical generator. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	ig1pval.p	$⊢ P = {Poly}_{1} (R)$
	ig1pval.g	$⊢ G = {idlGen}_{1p} (R)$
	ig1pcl.u	$⊢ U = LIdeal (P)$
	ig1prsp.k	$⊢ K = RSpan (P)$
Assertion	ig1prsp	$⊢ (R \in DivRing \land I \in U) \to I = K (\{G (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		ig1prsp.k	$⊢ K = RSpan (P)$
5	1 2 3	ig1pcl	$⊢ (R \in DivRing \land I \in U) \to G (I) \in I$
6		eqid	$⊢ ∥_{r} (P) = ∥_{r} (P)$
7	1 2 3 6	ig1pdvds	$⊢ (R \in DivRing \land I \in U \land x \in I) \to G (I) ∥_{r} (P) x$
8	7	3expa	$⊢ ((R \in DivRing \land I \in U) \land x \in I) \to G (I) ∥_{r} (P) x$
9	8	ralrimiva	$⊢ (R \in DivRing \land I \in U) \to \forall x \in I G (I) ∥_{r} (P) x$
10		drngring	$⊢ R \in DivRing \to R \in Ring$
11	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
12	10 11	syl	$⊢ R \in DivRing \to P \in Ring$
13	12	adantr	$⊢ (R \in DivRing \land I \in U) \to P \in Ring$
14		simpr	$⊢ (R \in DivRing \land I \in U) \to I \in U$
15		eqid	$⊢ {Base}_{P} = {Base}_{P}$
16	15 3	lidlss	$⊢ I \in U \to I \subseteq {Base}_{P}$
17	16	adantl	$⊢ (R \in DivRing \land I \in U) \to I \subseteq {Base}_{P}$
18	17 5	sseldd	$⊢ (R \in DivRing \land I \in U) \to G (I) \in {Base}_{P}$
19	15 3 4 6	lidldvgen	$⊢ (P \in Ring \land I \in U \land G (I) \in {Base}_{P}) \to (I = K (\{G (I)\}) \leftrightarrow (G (I) \in I \land \forall x \in I G (I) ∥_{r} (P) x))$
20	13 14 18 19	syl3anc	$⊢ (R \in DivRing \land I \in U) \to (I = K (\{G (I)\}) \leftrightarrow (G (I) \in I \land \forall x \in I G (I) ∥_{r} (P) x))$
21	5 9 20	mpbir2and	$⊢ (R \in DivRing \land I \in U) \to I = K (\{G (I)\})$

Metamath Proof Explorer

Theorem ig1prsp

Proof