Theorem 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 = ( Poly1 ` R )
	ig1pval.g	|- G = ( idlGen1p ` R )
	ig1pcl.u	|- U = ( LIdeal ` P )
	ig1prsp.k	|- K = ( RSpan ` P )
Assertion	ig1prsp	|- ( ( R e. DivRing /\ I e. U ) -> I = ( K ` { ( G ` I ) } ) )

Proof

Step	Hyp	Ref	Expression
1		ig1pval.p	|- P = ( Poly1 ` R )
2		ig1pval.g	|- G = ( idlGen1p ` R )
3		ig1pcl.u	|- U = ( LIdeal ` P )
4		ig1prsp.k	|- K = ( RSpan ` P )
5	1 2 3	ig1pcl	|- ( ( R e. DivRing /\ I e. U ) -> ( G ` I ) e. I )
6		eqid	|- ( ||r ` P ) = ( ||r ` P )
7	1 2 3 6	ig1pdvds	|- ( ( R e. DivRing /\ I e. U /\ x e. I ) -> ( G ` I ) ( ||r ` P ) x )
8	7	3expa	|- ( ( ( R e. DivRing /\ I e. U ) /\ x e. I ) -> ( G ` I ) ( ||r ` P ) x )
9	8	ralrimiva	|- ( ( R e. DivRing /\ I e. U ) -> A. x e. I ( G ` I ) ( ||r ` P ) x )
10		drngring	|- ( R e. DivRing -> R e. Ring )
11	1	ply1ring	|- ( R e. Ring -> P e. Ring )
12	10 11	syl	|- ( R e. DivRing -> P e. Ring )
13	12	adantr	|- ( ( R e. DivRing /\ I e. U ) -> P e. Ring )
14		simpr	|- ( ( R e. DivRing /\ I e. U ) -> I e. U )
15		eqid	|- ( Base ` P ) = ( Base ` P )
16	15 3	lidlss	|- ( I e. U -> I C_ ( Base ` P ) )
17	16	adantl	|- ( ( R e. DivRing /\ I e. U ) -> I C_ ( Base ` P ) )
18	17 5	sseldd	|- ( ( R e. DivRing /\ I e. U ) -> ( G ` I ) e. ( Base ` P ) )
19	15 3 4 6	lidldvgen	|- ( ( P e. Ring /\ I e. U /\ ( G ` I ) e. ( Base ` P ) ) -> ( I = ( K ` { ( G ` I ) } ) <-> ( ( G ` I ) e. I /\ A. x e. I ( G ` I ) ( ||r ` P ) x ) ) )
20	13 14 18 19	syl3anc	|- ( ( R e. DivRing /\ I e. U ) -> ( I = ( K ` { ( G ` I ) } ) <-> ( ( G ` I ) e. I /\ A. x e. I ( G ` I ) ( ||r ` P ) x ) ) )
21	5 9 20	mpbir2and	|- ( ( R e. DivRing /\ I e. U ) -> I = ( K ` { ( G ` I ) } ) )