drnglpir

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

		Ref	Expression
	Assertion	drnglpir	$⊢ R \in DivRing \to R \in LPIR$

Step	Hyp	Ref	Expression
1		drngring	$⊢ R \in DivRing \to R \in 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 \in DivRing \to LIdeal (R) = \{\{0_{R}\}, {Base}_{R}\}$
6		eqid	$⊢ LPIdeal (R) = LPIdeal (R)$
7	6 3	lpi0	$⊢ R \in Ring \to \{0_{R}\} \in LPIdeal (R)$
8	6 2	lpi1	$⊢ R \in Ring \to {Base}_{R} \in LPIdeal (R)$
9	7 8	prssd	$⊢ R \in Ring \to \{\{0_{R}\}, {Base}_{R}\} \subseteq LPIdeal (R)$
10	1 9	syl	$⊢ R \in DivRing \to \{\{0_{R}\}, {Base}_{R}\} \subseteq LPIdeal (R)$
11	5 10	eqsstrd	$⊢ R \in DivRing \to LIdeal (R) \subseteq LPIdeal (R)$
12	6 4	islpir2	$⊢ R \in LPIR \leftrightarrow (R \in Ring \land LIdeal (R) \subseteq LPIdeal (R))$
13	1 11 12	sylanbrc	$⊢ R \in DivRing \to R \in LPIR$

Metamath Proof Explorer