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

Metamath Proof Explorer

Theorem drnglpir

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

Ref Expression
Assertion drnglpir ( 𝑅 ∈ DivRing → 𝑅 ∈ LPIR )

Proof

Step Hyp Ref Expression
1 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
2 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
4 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
5 2 3 4 drngnidl ⊢ ( 𝑅 ∈ DivRing → ( LIdeal ‘ 𝑅 ) = { { ( 0g ‘ 𝑅 ) } , ( Base ‘ 𝑅 ) } )
6 eqid ⊢ ( LPIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 )
7 6 3 lpi0 ⊢ ( 𝑅 ∈ Ring → { ( 0g ‘ 𝑅 ) } ∈ ( LPIdeal ‘ 𝑅 ) )
8 6 2 lpi1 ⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) ∈ ( LPIdeal ‘ 𝑅 ) )
9 7 8 prssd ⊢ ( 𝑅 ∈ Ring → { { ( 0g ‘ 𝑅 ) } , ( Base ‘ 𝑅 ) } ⊆ ( LPIdeal ‘ 𝑅 ) )
10 1 9 syl ⊢ ( 𝑅 ∈ DivRing → { { ( 0g ‘ 𝑅 ) } , ( Base ‘ 𝑅 ) } ⊆ ( LPIdeal ‘ 𝑅 ) )
11 5 10 eqsstrd ⊢ ( 𝑅 ∈ DivRing → ( LIdeal ‘ 𝑅 ) ⊆ ( LPIdeal ‘ 𝑅 ) )
12 6 4 islpir2 ⊢ ( 𝑅 ∈ LPIR ↔ ( 𝑅 ∈ Ring ∧ ( LIdeal ‘ 𝑅 ) ⊆ ( LPIdeal ‘ 𝑅 ) ) )
13 1 11 12 sylanbrc ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ LPIR )