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 )