Definition df-lpir 20496

Description: Define the class of left principal ideal rings, rings where every left ideal has a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015.)

Assertion

Ref	Expression
df-lpir	⊢ LPIR = {𝑤 ∈ Ring ∣ (LIdeal‘𝑤) = (LPIdeal‘𝑤)}

Detailed syntax breakdown of Definition df-lpir

Step	Hyp	Ref	Expression
1		clpir 20494	. 2 class LPIR
2		vw	. . . . . 6 setvar 𝑤
3	2	cv 1540	. . . . 5 class 𝑤
4		clidl 20413	. . . . 5 class LIdeal
5	3, 4	cfv 6430	. . . 4 class (LIdeal‘𝑤)
6		clpidl 20493	. . . . 5 class LPIdeal
7	3, 6	cfv 6430	. . . 4 class (LPIdeal‘𝑤)
8	5, 7	wceq 1541	. . 3 wff (LIdeal‘𝑤) = (LPIdeal‘𝑤)
9		crg 19764	. . 3 class Ring
10	8, 2, 9	crab 3069	. 2 class {𝑤 ∈ Ring ∣ (LIdeal‘𝑤) = (LPIdeal‘𝑤)}
11	1, 10	wceq 1541	1 wff LPIR = {𝑤 ∈ Ring ∣ (LIdeal‘𝑤) = (LPIdeal‘𝑤)}

This definition is referenced by:  islpir  20501