Metamath Proof Explorer

Theorem drnglpir

Description: Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Assertion drnglpir 
|- ( R e. DivRing -> R e. LPIR )

Proof

Step Hyp Ref Expression
1 drngring 
 |-  ( R e. DivRing -> R e. Ring )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
4 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
5 2 3 4 drngnidl 
 |-  ( R e. DivRing -> ( LIdeal ` R ) = { { ( 0g ` R ) } , ( Base ` R ) } )
6 eqid 
 |-  ( LPIdeal ` R ) = ( LPIdeal ` R )
7 6 3 lpi0 
 |-  ( R e. Ring -> { ( 0g ` R ) } e. ( LPIdeal ` R ) )
8 6 2 lpi1 
 |-  ( R e. Ring -> ( Base ` R ) e. ( LPIdeal ` R ) )
9 7 8 prssd 
 |-  ( R e. Ring -> { { ( 0g ` R ) } , ( Base ` R ) } C_ ( LPIdeal ` R ) )
10 1 9 syl 
 |-  ( R e. DivRing -> { { ( 0g ` R ) } , ( Base ` R ) } C_ ( LPIdeal ` R ) )
11 5 10 eqsstrd 
 |-  ( R e. DivRing -> ( LIdeal ` R ) C_ ( LPIdeal ` R ) )
12 6 4 islpir2 
 |-  ( R e. LPIR <-> ( R e. Ring /\ ( LIdeal ` R ) C_ ( LPIdeal ` R ) ) )
13 1 11 12 sylanbrc 
 |-  ( R e. DivRing -> R e. LPIR )