Metamath Proof Explorer

Theorem ply1lpir

Description: The ring of polynomials over a division ring has the principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypothesis ply1lpir.p 
|- P = ( Poly1 ` R )
Assertion ply1lpir 
|- ( R e. DivRing -> P e. LPIR )

Proof

Step Hyp Ref Expression
1 ply1lpir.p 
 |-  P = ( Poly1 ` R )
2 drngring 
 |-  ( R e. DivRing -> R e. Ring )
3 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
4 2 3 syl 
 |-  ( R e. DivRing -> P e. Ring )
5 eqid 
 |-  ( Base ` P ) = ( Base ` P )
6 eqid 
 |-  ( LIdeal ` P ) = ( LIdeal ` P )
7 5 6 lidlss 
 |-  ( i e. ( LIdeal ` P ) -> i C_ ( Base ` P ) )
8 7 adantl 
 |-  ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> i C_ ( Base ` P ) )
9 eqid 
 |-  ( idlGen1p ` R ) = ( idlGen1p ` R )
10 1 9 6 ig1pcl 
 |-  ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> ( ( idlGen1p ` R ) ` i ) e. i )
11 8 10 sseldd 
 |-  ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> ( ( idlGen1p ` R ) ` i ) e. ( Base ` P ) )
12 eqid 
 |-  ( RSpan ` P ) = ( RSpan ` P )
13 1 9 6 12 ig1prsp 
 |-  ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> i = ( ( RSpan ` P ) ` { ( ( idlGen1p ` R ) ` i ) } ) )
14 sneq 
 |-  ( j = ( ( idlGen1p ` R ) ` i ) -> { j } = { ( ( idlGen1p ` R ) ` i ) } )
15 14 fveq2d 
 |-  ( j = ( ( idlGen1p ` R ) ` i ) -> ( ( RSpan ` P ) ` { j } ) = ( ( RSpan ` P ) ` { ( ( idlGen1p ` R ) ` i ) } ) )
16 15 rspceeqv 
 |-  ( ( ( ( idlGen1p ` R ) ` i ) e. ( Base ` P ) /\ i = ( ( RSpan ` P ) ` { ( ( idlGen1p ` R ) ` i ) } ) ) -> E. j e. ( Base ` P ) i = ( ( RSpan ` P ) ` { j } ) )
17 11 13 16 syl2anc 
 |-  ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> E. j e. ( Base ` P ) i = ( ( RSpan ` P ) ` { j } ) )
18 4 adantr 
 |-  ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> P e. Ring )
19 eqid 
 |-  ( LPIdeal ` P ) = ( LPIdeal ` P )
20 19 12 5 islpidl 
 |-  ( P e. Ring -> ( i e. ( LPIdeal ` P ) <-> E. j e. ( Base ` P ) i = ( ( RSpan ` P ) ` { j } ) ) )
21 18 20 syl 
 |-  ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> ( i e. ( LPIdeal ` P ) <-> E. j e. ( Base ` P ) i = ( ( RSpan ` P ) ` { j } ) ) )
22 17 21 mpbird 
 |-  ( ( R e. DivRing /\ i e. ( LIdeal ` P ) ) -> i e. ( LPIdeal ` P ) )
23 22 ex 
 |-  ( R e. DivRing -> ( i e. ( LIdeal ` P ) -> i e. ( LPIdeal ` P ) ) )
24 23 ssrdv 
 |-  ( R e. DivRing -> ( LIdeal ` P ) C_ ( LPIdeal ` P ) )
25 19 6 islpir2 
 |-  ( P e. LPIR <-> ( P e. Ring /\ ( LIdeal ` P ) C_ ( LPIdeal ` P ) ) )
26 4 24 25 sylanbrc 
 |-  ( R e. DivRing -> P e. LPIR )