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

Metamath Proof Explorer

Definition df-lpir

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)

		Ref	Expression
	Assertion	df-lpir	$⊢ LPIR = \{w \in Ring \| LIdeal (w) = LPIdeal (w)\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clpir	$class LPIR$
1		vw	$setvar w$
2		crg	$class Ring$
3		clidl	$class LIdeal$
4	1	cv	$setvar w$
5	4 3	cfv	$class LIdeal (w)$
6		clpidl	$class LPIdeal$
7	4 6	cfv	$class LPIdeal (w)$
8	5 7	wceq	$wff LIdeal (w) = LPIdeal (w)$
9	8 1 2	crab	$class \{w \in Ring \| LIdeal (w) = LPIdeal (w)\}$
10	0 9	wceq	$wff LPIR = \{w \in Ring \| LIdeal (w) = LPIdeal (w)\}$