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 )