This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) } ) )