Metamath Proof Explorer

Theorem drnglpir

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

Ref Expression
Assertion drnglpir ⊢ R ∈ DivRing → R ∈ LPIR

Proof

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